Ich verstehe nicht ganz, warum fast alle SAT-Löser CNF anstelle von DNF verwenden. Es scheint mir, dass die Lösung von SAT mit DNF einfacher ist. Schließlich müssen Sie nur den Satz von Implantaten durchsuchen und prüfen, ob einer von ihnen nicht sowohl eine Variable als auch deren Negation enthält. Für CNF gibt es kein einfaches Verfahren wie dieses.
ds.algorithms
sat
Kaveh
quelle
quelle
Antworten:
Die Lehrbuchreduktion von SAT auf 3SAT aufgrund von Karp transformiert eine beliebige Boolesche Formel in eine „äquivalente“ CNF-Boolesche FormelΦ einer Polynomgröße, so dass Φ genau dann erfüllt werden kann, wenn Φ ' erfüllt werden kann. (Genau genommen sind diese beiden Formeln nicht äquivalent, da Φ ' zusätzliche Variablen enthält, der Wert von Φ ' jedoch nicht von diesen neuen Variablen abhängt.)Φ′ Φ Φ′ Φ′ Φ′
Eine ähnliche Reduktion von beliebigen Booleschen Formeln auf DNF-Formeln ist nicht bekannt. Alle bekannten Transformationen vergrößern die Formel exponentiell. Außerdem ist eine solche Reduktion nur möglich, wenn P = NP!
quelle
Die meisten wichtigen Dinge wurden gesagt, aber ich möchte ein paar Punkte hervorheben.
Daher verwenden SAT-Löser CNF, weil sie auf die Erfüllbarkeit abzielen und jede Formel in einen CNF übersetzt werden kann, während die Erfüllbarkeit in linearer Zeit erhalten bleibt.
quelle
SAT-Löser "verwenden" kein CNF - sie erhalten (oft) CNF als Eingabe und geben ihr Bestes, um das ihnen gegebene CNF zu lösen. Wie Ihre Frage zeigt, ist Repräsentation alles - es ist viel einfacher festzustellen, ob eine DNF zufriedenstellend ist als eine CNF derselben Größe.
Dies führt zu der Frage, warum SAT-Löser nicht einfach ihren gegebenen CNF in einen DNF umwandeln und den resultierenden DNF lösen können. Dies zu versuchen, ist eine gute Übung, um Fragen der Repräsentation zu verstehen.
quelle
7 th September 2013: Weitere Antwort hinzugefügt, Scheck unten auf der Seite
Grundsätzlich ist eine DNF-Formel eine Disjunktion von Klauseln , wobei jede Klausel c i = l i , 1 ∧ ist . . . ∧ l i , k ist eine Konjunktion von Literalen. Nennen wir eine Klausel c i widersprüchlich, wenn sie sowohl ein Literal l als auch dessen Negation ¬ l enthält . Es ist leicht zu erkennen, dass jede nicht widersprüchliche Klausel nur 2 n - k codiertc1∨...∨cm ci=li,1∧...∧li,k ci l ¬l 2n−k Lösungen der Formel. Die gesamte DNF ist also nur eine Aufzählung von Lösungen. Eine Formel kann exponentiell viele Lösungen haben, so dass die entsprechende DNF-Formel exponentiell viele Klauseln haben kann. Versuchen Sie, diese CNF-Formel zu konvertieren:
zu seiner entsprechenden DNF-Formel: Sie werden zu viele Klauseln erhalten. Mit einem Wort: CNF ist kompakt, DNF nicht. CNF ist implizit, während DNF explizit ist.
Das folgende Problem ist NP-vollständig: Gibt es bei einer DNF-Instanz eine Zuweisung von Variablen, die alle Klauseln verfälscht?
quelle
Ich habe nur noch eine Sache bemerkt, die hoffentlich eine separate Antwort verdient. Die Vermutung der Frage ist nicht ganz richtig. Ein binäres Entscheidungsdiagramm (BDD) könnte als kompakte / verfeinerte Darstellung von DNF angesehen werden. Es gibt einige SAT-Löser, die BDDs verwenden, aber ich glaube, sie werden nicht mehr angezeigt.
Es gibt eine schöne Arbeit von Darwiche und Marquis , die verschiedene Eigenschaften verschiedener Darstellungen von Booleschen Funktionen untersucht.
quelle
Diese weitere Antwort ist als Feedback auf den Kommentar von dividebyzero zu meiner vorherigen Antwort gedacht.
Wie dividebyzero sagt, sind CNF und DNF zweifellos zwei Seiten einer Medaille.
Wenn Sie eine befriedigende Aufgabe finden müssen, ist DNF explizit, da es Ihnen offenbar die befriedigenden Aufgaben zeigt (DNF-Zufriedenheit gehört zu ), wohingegen CNF implizit ist, wenn es seine befriedigenden Aufgaben vor Ihren Augen verbirgt (CNF-Zufriedenheit ist N) P - c o m p l e t e ). Wir kennen kein Verfahren, das in der Lage ist, eine CNF-Formel in eine zufriedenstellende DNF-Formel mit nicht exponentieller Größe einzuwickeln und abzuwickeln. Dies war der Punkt meiner vorherigen Antwort (deren Beispiel das exponentielle Aufblähen zeigen sollte, obwohl zugegebenermaßen ein solches Beispiel nicht die bestmögliche Wahl war).P NP−complete
An einem Ende gibt es Widersprüche, dh nicht erfüllbare Formeln. Am anderen Ende haben wir Tautologien, dh nicht fälschbare Formeln. In der Mitte haben wir Formeln, die sowohl erfüllbar als auch verfälschbar sind.
In jeder CNF-Formel mit Variablen codiert jeder Satz der Länge k offenbar 2 n - kn k 2n−k fälschende Zuweisungen.
In jeder DNF-Formel mit Variablen codiert jeder Ausdruck der Länge k offenbar 2 n - kn k 2n−k die die Zuweisungen erfüllen.
Eine CNF-Formel ohne Klauseln ist eine Tautologie, da sie keine fälschende Zuordnung hat. Eine CNF-Formel, die die leere Klausel enthält (die alle anderen Klauseln subsumiert), ist ein Widerspruch, da die leere Klausel (diek=0 2n NP−complete zu unterscheiden zwischen diesen 2 Fälle).
Eine DNF-Formel ohne Terme ist ein Widerspruch, weil sie keine zufriedenstellende Zuordnung hat. Eine DNF-Formel, die den leeren Term enthält (der jeden anderen Term subsumiert), ist eine Tautologie, weil der leere Term (der ) anzeigt, dass alle 2 n Zuweisungen erfüllt sind. Jede andere DNF Formel ist entweder ein Tautology odereiner dieser Formeln in der Mitte (und es ist N P - C o m p l e t e zu unterscheiden zwischen diesen 2 Fällen).k=0 2n NP−complete
Bei einer CNF-Formel bedeutet die Unterscheidung zwischen den beiden oben genannten Fällen, dass festgestellt werden kann, ob sich alle fälschenden Zuweisungen, die durch das Vorhandensein von Klauseln kollektiv erzeugt werden, so überlappen, dass alle abgedeckt werden2n Zuweisungen (in diesem Fall ist die Formel ein Widerspruch, ansonsten ist es befriedigend).
In diesem Licht wird klarer, warum CNF-Zufriedenheit und DNF-Fälschbarkeit in Bezug auf die Rechenhärte gleichwertig sind. Weil es sich tatsächlich um dasselbe Problem handelt, da die zugrunde liegende Aufgabe genau dieselbe ist: festzustellen, ob die Vereinigung mehrerer Mengen dem Raum aller Möglichkeiten entspricht . Eine solche Aufgabe führt uns in den weiteren Bereich des Zählens, der meiner Meinung nach einer der Wege ist, die inbrünstig erkundet werden müssen, um hoffentlich einige nicht zu vernachlässigende Fortschritte bei diesen Problemen zu erzielen (ich bezweifle, dass weitere Untersuchungen zu lösungsbasierten Lösungen durchgeführt werden) kann schließlich bahnbrechende theoretische Fortschritte bringen, während es sicherlich weiterhin überraschende praktische Fortschritte bringt).
Die Schwierigkeit einer solchen Aufgabe besteht darin, dass sich diese Mengen in einer Einschluss - Ausschluss - Weise wild überlappen.
Das Vorhandensein einer solchen Überlappung ist genau dort, wo die Härte des Zählens liegt. Darüber hinaus ist die Tatsache, dass wir diese Mengen überlappen lassen, genau der Grund, warum wir kompakte Formeln haben können, deren Lösungsraum dennoch exponentiell groß ist.
quelle
Ich habe beschlossen, alle diese Antworten in diesem Thread (insbesondere Giorgio Cameranis Antwort) in eine schöne Tabelle zu verwandeln, damit die Dualität auf einen Blick sichtbar wird:
Kürzeste Antwort auf die Frage: Das Anzeigen der Erfüllbarkeit (Lösen von SAT) über DNF ist gemäß der obigen Tabelle nur in exponentieller Zeit möglich.
quelle