DNF vs KNF
-
knivil schrieb:
SAT trivial?
Aber ja doch. Selbst das Argument dafür ist trivial, da denkst du besser nochmal kurz drüber nach.
-
Und wie komme ich zu meinem ersten Term? Wenn ich die Loesung kenne, ja, dann ist die Loesung trivial.
-
knivil: Für SAT in DNF reicht es, sich die Monome einzeln anzuschauen, denn wenn eines erfüllbar ist, ist der Gesamtausdruck erfüllbar. Jetzt schaust du dir die Literale eines Monoms der Reihe nach an und gibst deinen Variablen genau die Belegung, die nötig ist, um das Monom zu erfüllen. Kommt es dabei zu Widersprüchen, gehst du zum nächsten Monom.
-
Entsprechend arbeiten SAT-solver auch eher mit KNF Formeln, da man jede beliebige Formel in polynomieller Zeit in eine erfüllbarkeitsäquivalente KNF Formel umwandeln kann (im Gegensatz zu DNF).
-
knivil, kann es sein, dass du den Aufwand zur Aufstellung der DNF mitrechnest? Die Behauptung war nur: Wenn man die DNF hat, ist das Erfüllbarkeitsproblem trivial. Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.
-
Bashar schrieb:
Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.
"(a \land \neg a) \lor (b \land \neg b)" ist auch nicht erfüllbar und in DNF.
Natürlich ist jede nicht erfüllbare DNF Formel äquivalent zu "false", aber das gilt (per Definition) auch für jede andere nicht erfüllbare Formel.
-
life schrieb:
Bashar schrieb:
Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.
"(a \land \neg a) \vee (b \land \neg b)" ist auch nicht erfüllbar und in DNF.
Natürlich ist jede nicht erfüllbare DNF Formel äquivalent zu "false", aber das gilt (per Definition) auch für jede andere nicht erfüllbare Formel.
Je nach Definition... Wenn man sagt, dass eine Variable in einer Klausel nur einmal vorkommen darf geht das nicht mehr.
-
Ausschnitt aus wikipedia
... A DNF formula is in full disjunctive normal form if each of its variables appears exactly once in every clause. ...
-
full disjunctive normal form != disjunctive normal form
-
SG1 schrieb:
full disjunctive normal form != disjunctive normal form
Wohl war... Aber trotzdem witzlos bei der DNF zwei Literale in einer Klausel zuzulassen.
-
zwei gleiche meine ich.
-
Seh ich genauso. Jede Variable höchstens einmal pro Konjunktionsterm, sonst ist es keine DNF.
-
Eine solche Definition von DNF war mir nicht bekannt. Mit dieser Definition macht Bashars Aussage dann natürlich wesentlich mehr Sinn ;).
-
life schrieb:
Eine solche Definition von DNF war mir nicht bekannt. Mit dieser Definition macht Bashars Aussage dann natürlich wesentlich mehr Sinn ;).
Sonst könnte man eine DNF beliebig aufblähen und keine obere Schranke für die Länge für Formeln in DNF angeben. Egal. Es gibt Formeln, deren kleinste DNF nach obiger Definition die Länge O(2^n) haben. Checken ist also linear, aber die Konstruktion dieser DNF braucht natürlich im Worst-Case O(2^n).
-
Eine DNF ist es ja immer noch, egal wie oft die Literale in einem Monom vorkommen. Wenn man das exakt einmalige Vorkommen jedes Literals fordert heißt das ganze kanonische DNF
