Warum wird CNF für SAT und nicht für DNF verwendet?

22

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.

Kaveh
quelle
5
Nicht alle Bedingungslöser verwenden CNF als Eingabe. Einige bevorzugen dies nicht, da die Struktur des ursprünglichen Einschränkungssatzes beibehalten wird.
Dave Clarke
1
Diese Frage hat eine falsche Prämisse und verdient keine so hohe Bewertung, wie sie derzeit formuliert wird. SAT ist definiert als die Lösung von CNF-Formeln. Es gibt ein Problem beim Lösen von DNFs (Sie können es sogar als das Finden zufriedenstellender Zuordnungen bezeichnen), aber in CS heißt es nicht / SAT mit einem Spitznamen. & imho sollte dies nach cs.se migriert werden ... eine weitere Anmerkung - die Konvertierung von CNF in DNF und umgekehrt ist tatsächlich einem Komprimierungsalgorithmus sehr ähnlich oder kann als solcher angesehen werden, der in bestimmten Fällen schlecht ausfällt (was zu einer exponentiellen Explosion führt) in der Größe)
vzn
10
@vzn: Tatsächlich wird "SAT" manchmal verwendet, um auf das Problem hinzuweisen, eine befriedigende Zuweisung für eine beliebige Boolesche Formel zu finden. CNF-SAT ist nur der interessanteste Spezialfall, so dass wir mit "SAT" vor allem CNF-SAT als eine Art Synechdoche bezeichnen. DNF-SAT ist natürlich genauso effizient lösbar wie CNF-TAUTOLOGY. Die Frage scheint davon auszugehen, dass dies nicht erkannt wird.
Niel de Beaudrap

Antworten:

56

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!

Jeffε
quelle
afaik die Umwandlung von DNF in CNF und umgekehrt ist nicht genau das gleiche wie P vs NP, obwohl es wahrscheinlich einige wichtige Trennungen von Komplexitätsklassen betrifft (anscheinend für Klassen "größer" als NP) ... das Problem ist, dass es dazu führen kann eine exponentielle Vergrößerung ... und in jedem Fall ist die Konvertierung zwischen CNF und DNF kein Entscheidungsproblem ... Es gibt mehrere Möglichkeiten, daraus ein Entscheidungsproblem zu machen ...
vzn 22.10.12
10
Ich denke, JeffE meinte, dass DNF-SAT in P ist, es kann also nicht NP-vollständig sein, es sei denn, P = NP.
Luke Mathieson
2
"Alle bekannten Transformationen" sind nach heutigem Kenntnisstand nicht korrekt, da es DNF <=> CNF-Formeln / -Konvertierungen gibt, die unabhängig vom Algorithmus nachweislich einen exponentiellen Speicherplatzverlust erfordern auf diese Frage & diese Antwort hinweisen ... wird die Abkürzung "DNF-SAT" irgendwo in der Literatur verwendet? Ich kann mich nicht erinnern, es selbst gesehen zu haben ... es scheint mir von Natur aus verwirrend ... DNF-befriedigend ist ein Entscheidungsproblem, DNF <-> CNF-Konvertierung ist ein Funktionsproblem & die Antwort macht diese Unterscheidung nicht zu klar; eine tolle antwort wäre ...
vzn
@ Jɛ ɛ E: Stört es Sie zu klären, was Sie hier mit "willkürlicher Boolescher Formel" gemeint haben? In der Arbeit von Karp auf Seite 92 wird die ZUFRIEDENHEITSBESTIMMUNG anhand von CNF-Formeln definiert. Dies hat keinen Einfluss auf Ihre Antwort auf die Frage des OP, aber ich versuche sicherzustellen, dass es keine allgemeineren Ergebnisse für beliebige boolesche Formeln gibt (dh Formeln, die nicht unbedingt in CNF enthalten sind). Thanks
lyes
22

Die meisten wichtigen Dinge wurden gesagt, aber ich möchte ein paar Punkte hervorheben.

  1. Erfüllbarkeit einer DNF-Formel ist P
  2. Die Erfüllbarkeit einer CNF-Formel ist NP
  3. Testen, ob eine CNF-Formel eine Tautologie ist, ist P
  4. Testen, ob eine DNF-Formel eine Tautologie ist, ist coNP
  5. Das Negieren von DNF ergibt CNF und umgekehrt

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.

Mikolas
quelle
1
@TayfunPay tun sie. Zum Beispiel . Wenn Sie Klauseln, die dieselbe Variable zweimal enthalten, nicht erlauben, gibt es eine einzige Darstellung einer Tautologie, bei der es sich um die leere Menge von Klauseln handelt. {{¬xx}}
Mikolas
3
@Tayfun Obwohl ich damit einverstanden bin, dass Definitionen das Wiederholen von Variablen in Klauseln normalerweise nicht zulassen, glaube ich nicht, dass ich jemals eine Definition gesehen habe, die den leeren Satz von Klauseln nicht zulässt. (Und es ist mir nicht klar, warum Sie das tun möchten)
Mikolas
2
@Tayfun 1) Könnten Sie mich auf eine Veröffentlichung hinweisen, die besagt, dass es in CNF keine Tautologien gibt oder dass der leere Satz von Klauseln nicht CNF ist? 2) Wenn Sie die leere Menge von Klauseln nicht zulassen, sollten Sie auch die leere Klausel nicht zulassen und können auch nicht falsch darstellen. 3) Wenn Sie in CNF nicht wahr und / oder falsch zulassen, verlieren Sie die Eigenschaft, darstellen zu können alle Booleschen Funktionen, warum möchten Sie das tun?
Mikolas
1
"Es sollte keine Wiederholung von Variablen oder Literalen in einer bestimmten Klausel geben." --- das verbietet keine leeren Formeln oder Klauseln. Übrigens: Wenn Sie die leere Klausel nicht zulassen, können Sie keine Auflösungs-Widerlegungs-Beweise mehr durchführen, die einen ziemlich wichtigen Teil des automatisierten Denkens darstellen.
Mikolas
18

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.

Lev Reyzin
quelle
11

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...cmci=li,1...li,kcil¬l2nkLö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:

l1l2l3l4

l5l6l7l8

l9l10l11l12

l13l14l15l16

l17l18l19l20

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?

Giorgio Camerani
quelle
4
Ersetzen Sie \ und \ oder \ land und \ lor (oder \ wedge und \ vee), um die richtige LaTeX-Formatierung zu erhalten.
Jeffs
2
Eine Transformation zum regulären CNF ist von Natur aus nicht kompakter. Der eigentliche Schlüssel zur OP-Frage ist die Tatsache, dass Sie diese "gleichwertigen" CNF-Funktionen mit Hilfsvariablen erstellen können. Es gibt wahrscheinlich eine ähnliche Annäherung, die Sie mit der DNF anstellen können, um ein anderes Problem zu lösen, anstatt die Erfüllbarkeit zu testen. (Equi-Unzufriedenheit Funktionen? ...)
Dividebyzero
1
Diese Einsicht von Giorgio Camerani ist nicht gut. Die gleiche exponentielle Zunahme der Anzahl von Klauseln kann auftreten, wenn Sie etwas in CNF konvertieren. Wählen Sie dasselbe Beispiel aus und ersetzen Sie "und" durch "oder". Die Konvertierung von diesem kleinen DNF-Ausdruck in den CNF wird trotzdem enorm sein. Sie haben ein bisschen eine Ying-and-Yang-Beziehung zu ihnen.
Dividebyzero
@dividebyzero: Ich habe eine separate Antwort gewidmet, um auf Ihre Kommentare einzugehen.
Giorgio Camerani
6

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.

Mikolas
quelle
4

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).PNPcomplete

PNPcomplete ). Wir kennen kein Verfahren, das in der Lage ist, eine DNF-Formel in eine nicht exponentiell dimensionierte, gleichwertige CNF-Formel einzuwickeln und abzuwickeln.

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 - knk2nk fälschende Zuweisungen.

In jeder DNF-Formel mit Variablen codiert jeder Ausdruck der Länge k offenbar 2 n - knk2nk 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 (die k=02nNPcomplete 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=02nNPcomplete

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).

2n

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.

Giorgio Camerani
quelle
4

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:

DNFCNFtautology/unfalsifiabilitycoNP-completeP(each clause has a pair of P and ¬P)satisfiabilityP(sat. assignments are explicit)NP-completefalsifiabilityNP-completeP(fals. assignments are explicit)unsatisfiabilityP(each clause has a pair of P and ¬P)coNP-completeconversion to normal form, retaining equivalence()()conversion to normal form, retaining satisfiability()FPconversion to normal form, retaining falsiabilityFP()

()

()()FPNP[1]

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.

mcb
quelle
1
Was ist eine "PL-Formel" und was bedeutet "NF"?
Joshua Grochow
4
Hier gibt es einige Probleme. (1) Unter "Unverfälschbarkeit" verstehe ich "Tautologie". (2) KNF sollte CNF sein.
Huck Bennett
2
A(φ)φφA(φ)φA(φ)
1
(1) "Prädikatenlogik" sollte "Aussagenlogik" sein. (2) Die Konvertierungen in Normalformen sind keine Entscheidungsprobleme, sondern Funktionsprobleme (bzw. Suchprobleme, da die "Normalformen" nicht eindeutig sind). Die in der Tabelle angegebenen Entscheidungsklassen sind daher unangemessen.
Emil Jeřábek unterstützt Monica am
1
Δ3P