Was ist ein Beispiel für eine unbefriedigende 3-CNF-Formel?

15

Ich versuche, meinen Kopf um einen NP-Vollständigkeitsnachweis zu wickeln, der sich anscheinend um SAT / 3CNF-SAT dreht.

Vielleicht ist es die späte Stunde, aber ich fürchte, ich kann mir keine 3CNF-Formel vorstellen, die nicht befriedigt werden kann (ich vermisse wahrscheinlich etwas Offensichtliches).

Können Sie mir ein Beispiel für eine solche Formel geben?

user11171
quelle

Antworten:

29

Technisch gesehen können Sie in 3-CNF als ( x x x ) ( ¬ x ¬ x ¬ x ) schreiben , aber Sie möchten wahrscheinlich ein "echtes" Beispiel.x¬x(xxx)(¬x¬x¬x)

In diesem Fall benötigt eine 3CNF-Formel mindestens 3 Variablen. Da jede Klausel genau eine Zuweisung ausschließt, benötigen Sie mindestens Klauseln, um eine nicht erfüllbare Formel zu erhalten. In der Tat ist die einfachste:23=8

Es ist nicht schwer zu erkennen, dass diese Formel nicht zu vereinbaren ist.

(xyz)(xy¬z)(x¬yz)(x¬y¬z)(¬xyz)(¬xy¬z)(¬x¬yz)(¬x¬y¬z)
Shaull
quelle
Vielleicht bin ich hier eher naiv, aber warum können Sie nicht eine Reihe von Vergleichen durchführen, um festzustellen, ob es Sätze nicht äquivalenter Ausdrücke gibt? - v ist die Anzahl der eindeutigen Variablen. Wenn ich richtig gezählt habe, gibt es nur n ( n - 1 )2vvn(n-1)2
@ BenCrossley - nicht sicher, was du meinst. Kannst du ein Beispiel geben?
Shaull
8

Wenn Sie komplexere Beispiele für solche Formeln wünschen, werfen Sie einen Blick auf einige Benchmark-Probleme von SATLIB . ToughSAT ist auch ein nützliches Tool zum Erstellen von 3-SAT-Instanzen. Es ist einfach, befriedigende und unbefriedigende Instanzen zu erstellen.

Juho
quelle