Direkte SAT- bis 3-SAT-Reduzierung

Hier besteht das Ziel darin, ein beliebiges SAT-Problem in Polynomzeit unter Verwendung der geringsten Anzahl von Klauseln und Variablen auf 3-SAT zu reduzieren. Meine Frage ist von Neugierde motiviert. Weniger formal möchte ich wissen: "Was ist die 'natürlichste' Reduzierung von SAT auf 3-SAT?"

Die Reduktion, die ich in Lehrbüchern immer gesehen habe, sieht ungefähr so ​​aus:

1. Nehmen Sie zuerst Ihre SAT-Instanz und wenden Sie den Cook-Levin-Satz an, um ihn auf die SAT-Schaltung zu reduzieren.

2. Anschließend beenden Sie den Job durch die Standardreduzierung des Schaltkreises SAT auf 3-SAT, indem Sie die Gatter durch Klauseln ersetzen.

Während dies funktioniert, sehen die resultierenden 3-SAT-Klauseln aufgrund der anfänglichen Anwendung des Cook-Levin-Theorems fast nicht so aus wie die SAT-Klauseln, mit denen Sie begonnen haben.

Kann jemand sehen, wie man die Reduzierung direkter vornimmt, den Zwischenkreis überspringt und direkt zu 3-SAT übergeht? Ich würde mich sogar über eine direkte Reduzierung des Sonderfalls von n-SAT freuen.

(Ich würde vermuten, dass es einige Kompromisse zwischen der Rechenzeit und der Größe der Ausgabe gibt. Es ist klar, dass eine entartete - wenn auch glücklicherweise unzulässige - Lösung darin besteht, nur das SAT-Problem zu lösen und dann eine triviale 3 auszugeben -SAT-Instanz ...)

EDIT: Basierend auf der Antwort von ratchet ist es jetzt klar, dass die Reduzierung auf n-SAT etwas trivial ist (und dass ich mir das vor dem Posten wirklich etwas genauer hätte überlegen sollen). Ich lasse diese Frage für den Fall offen, dass jemand die Antwort auf die allgemeinere Situation kennt, sonst akzeptiere ich einfach die Antwort der Ratsche.

Jede SAT-Klausel enthält 1, 2, 3 oder mehr Variablen. Die 3-Variablen-Klausel kann problemlos kopiert werden

Die 1 und 2 variable Klauseln {a1}und {a1,a2}kann erweitert werden , {a1,a1,a1}und{a1,a2,a1} jeweils.

Die Klausel mit mehr als 3 Variablen {a1,a2,a3,a4,a5}kann {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}mit s1und s2neuen Variablen erweitert werden, deren Wert davon abhängt, welche Variable in der ursprünglichen Klausel wahr ist

$n'$$n$

Wenn Sie eine Reduzierung von k-SAT auf 3-SAT benötigen, funktioniert die Antwort der Ratsche einwandfrei.

Wenn Sie eine direkte Reduktion von der allgemeinen Satzformel auf CNF (und auf 3-SAT) wünschen, dann denke ich, dass die Antwort auf Ihre Frage Was ist die "natürlichste" Reduktion ... ? ist: Es gibt keine "natürliche" Reduktion !

Aus den Schlussfolgerungen von Kapitel 2 - "CNF-Codierungen" des (sehr guten) Buches: Handbuch der Zufriedenheit :

...
Es gibt normalerweise viele Möglichkeiten, ein bestimmtes Problem in CNF zu modellieren, und es sind nur wenige Richtlinien für die Auswahl bekannt. Es gibt oft eine Auswahl von Problemmerkmalen, die als Variablen modelliert werden können, und einige müssen möglicherweise gründlich überlegt werden, um sie zu ermitteln. Tseitin-Codierungen sind kompakt und mechanisierbar, führen jedoch in der Praxis nicht immer zum besten Modell, und einige Teilformeln könnten besser erweitert werden. Einige Klauseln können aus Gründen der Polarität weggelassen werden, und implizite, symmetrische oder blockierte Klauseln können hinzugefügt werden. Unterschiedliche Kodierungen können unterschiedliche Vor- und Nachteile haben, wie z. B. Größe oder Lösungsdichte. Was für einen SAT-Solver von Vorteil ist, kann für einen anderen von Nachteil sein. Kurz gesagt, CNF-Modellierung ist eine Kunst, und wir müssen oft durch Intuition und Experimente vorgehen.
...

Der bekannteste Algorithmus ist der Tseitin-Algorithmus (G. Tseitin. Zur Komplexität der Herleitung in der Aussagenrechnung. Automation of Reasoning: Classical Papers in Computational Logic, 2: 466–483, 1983. Springer-Verlag.)

Für eine gute Einführung in die CNF-Codierung lesen Sie das vorgeschlagene Buch „ Handbuch zur Zufriedenheit“ . Sie können auch einige neuere Werke lesen und sich die Referenzen ansehen. beispielsweise:

• P. Jackson und D. Sheridan. Klauselformkonvertierungen für Boolesche Schaltungen. In HH Hoos und DG Mitchell, Redakteure, Theorie und Anwendungen von Erfüllbarkeitstests, 7. Internationale Konferenz, SAT 2004 , Band 3542 des LNCS, Seiten 183–198. Springer, 2004. (mit dem Ziel, die Anzahl der Klauseln zu reduzieren)
• P. Manolios, D. Vroon, Effiziente Schaltung zur CNF-Umwandlung. In Theorie und Anwendung von Erfüllbarkeitstests - SAT 2007 (2007), S. 4-9

Lassen Sie mich bitte eine andere Lösung posten, die der von Ratchel ähnelt, jedoch etwas anders ist. Dies ist direkt aus Kapitel 9 der 2. Ausgabe des "The Algorithm Design Manual" von Steven Skiena entnommen

• Wenn die Klausel nur ein Literal C = {z1} enthält, erstellen Sie zwei neue Variablen v1 und v2 und vier neue Klauseln mit drei Literalen: {v1, v2, z1}, {! V1, v2, z1}, {v1,! v2, z1} und {! v1,! v2, z1}. Beachten Sie, dass alle vier dieser Klauseln nur dann gleichzeitig erfüllt werden können, wenn z1 = T ist. Dies bedeutet auch, dass das ursprüngliche C erfüllt wird
• Wenn die Klausel zwei Literale enthält, C = {z1, z2}, erstellen Sie eine neue Variable v1 und zwei neue Klauseln: {v1, z1, z2} und {! V1, z1, z2}. Wiederum besteht die einzige Möglichkeit, diese beiden Klauseln zu erfüllen, darin, dass mindestens einer von z1 und z2 wahr ist und somit C erfüllt
• Wenn die Klausel drei Literale enthält, C = {z1, z2, z3}, kopieren Sie einfach C unverändert in die 3-SAT-Instanz
• Wenn die Klausel mehr als 3 Literale C = {z1, z2, ..., zn} enthält, erstellen Sie n-3 neue Variablen und n-2 neue Klauseln in einer Kette, wobei für 2 <= j <= n-2 gilt , Cij = {v1, j-1, zj + 1,! Vi, j}, Ci1 = {z1, z2,! Vi, 1} und Ci, n-2 = {vi, n-3, zn-1, zn}