Welche SAT-Probleme sind einfach?

Was sind "einfache Regionen" für die Erfüllbarkeit? Mit anderen Worten, ausreichende Bedingungen, damit ein SAT-Löser eine zufriedenstellende Zuordnung finden kann, sofern diese vorliegt.

Ein Beispiel ist, wenn jede Klausel Variablen mit wenigen anderen Klauseln teilt, aufgrund des konstruktiven Nachweises von LLL, irgendwelche anderen Ergebnisse in dieser Richtung?

Es gibt umfangreiche Literatur zu einfachen Regionen für die Glaubensvermehrung.

Ich vermute, Sie kennen das klassische Ergebnis von Schaefer von STOC'78, aber nur für den Fall.

10.1145 / 800133.804350

Schaefer hat bewiesen, dass, wenn SAT durch eine Reihe von Beziehungen parametrisiert wird, die in jedem Fall zulässig sind, es nur 6 nachvollziehbare Fälle gibt: 2-SAT (dh jede Klausel ist binär), Horn-SAT, Dual-Horn-SAT, Affin-SAT ( Lösungen für lineare Gleichungen in GF (2)), 0-gültig (Relationen, die durch die All-0-Zuweisung erfüllt werden) und 1-gültig (Relationen, die durch die All-1-Zuweisung erfüllt werden).

Ich bin mir nicht sicher, ob Sie danach suchen, aber es gibt eine umfangreiche Literatur zum 3-SAT-Phasenübergang.

Monasson, Zecchina, Kirkpatrcik, Selman und Troyansky hatten eine Arbeit in der Natur, die über den Phasenübergang von zufälligem k-SAT spricht. Sie verwendeten eine Parametrisierung des Verhältnisses von Klauseln zu Variablen. Für zufälliges 3-SAT stellten sie numerisch fest, dass der Übergangspunkt bei 4,3 liegt. Oberhalb dieses Punktes sind zufällige 3-SAT-Instanzen überbeschränkt und mit ziemlicher Sicherheit nicht mehr zu vereinbaren, und unterhalb dieses Punktes sind Probleme unterbeschränkt und mit hoher Wahrscheinlichkeit zu erfüllen. Mertens, Mezard und Zecchina verwenden Verfahren nach der Hohlraummethode, um den Phasenübergangspunkt mit einem höheren Genauigkeitsgrad abzuschätzen.

Weit weg vom kritischen Punkt funktionieren "dumme" Algorithmen gut für befriedigende Instanzen (Walk Sat, etc.). Soweit ich weiß, wachsen die Laufzeiten deterministischer Löser exponentiell an oder nahe dem Phasenübergang (siehe hier für eine ausführlichere Diskussion?).

Braunstein, Mezard und Zecchina, ein enger Verwandter der Glaubensvermehrung, haben eine Vermessungsvermehrung eingeführt , die befriedigende 3-SAT-Instanzen in Millionen von Variablen lösen soll, sogar in extremer Nähe des Phasenübergangs. MEZARD hat einen Vortrag hier auf Spingläser (die Theorie , von denen er bei der Analyse von zufälligen NP-Complete Phasenübergänge verwendet hat) und Maneva hat einen Vortrag hier auf Umfrage Ausbreitung.

Aus der anderen Richtung sieht es immer noch so aus, als würden unsere besten Löser exponentiell viel Zeit in Anspruch nehmen, um ihre Unzufriedenheit zu beweisen. Sehen Sie hier , hier und hier für Proofs / Diskussion der exponentiellen Natur einiger gängiger Methoden der Nachweis der Unerfüllbarkeit (Davis-Putnam Verfahren und Lösungsmethoden).

Bei zufälligen NP-Complete-Problemen muss man sehr vorsichtig mit Behauptungen von "Leichtigkeit" oder "Härte" sein. Wenn bei einem NP-Complete-Problem ein Phasenübergang angezeigt wird, kann nicht garantiert werden, wo die schwerwiegenden Probleme liegen oder ob es überhaupt Probleme gibt. Zum Beispiel ist das Hamiltoniain-Zyklus-Problem in Erdos-Renyi-Zufallsgraphen auch am oder nahe dem kritischen Übergangspunkt nachweislich einfach. Das Zahlenpartitionsproblem scheint keine Algorithmen zu haben, die es gut im Bereich von Wahrscheinlichkeit 1 oder 0 lösen, geschweige denn in der Nähe des kritischen Schwellenwerts. Soweit ich weiß, weisen zufällige 3-SAT-Probleme Algorithmen auf, die für befriedigende Fälle nahe oder unterhalb des kritischen Schwellenwerts (Erhebungsausbreitung, gesessenes Gehen usw.) gut funktionieren, aber keine effizienten Algorithmen oberhalb des kritischen Schwellenwerts, um die Unzufriedenheit zu beweisen.

Es gibt viele ausreichende Bedingungen. In gewissem Sinne wurde ein Großteil der theoretischen CS für die Erfassung dieser Bedingungen verwendet - Traktierbarkeit mit festen Parametern, 2-SAT, zufälliges 3-SAT mit verschiedenen Dichten usw.

Bisher ist dieses Konzept in der Literatur nicht allgemein anerkannt , aber der Klauselgraph des SAT-Problems (der Graph mit einem Knoten pro Klausel und Knoten, die verbunden sind, wenn Klauseln Variablen gemeinsam haben) sowie andere verwandte Graphen der SAT-Darstellung scheint viele grundlegende Hinweise zu haben, wie schwer die Instanz im Durchschnitt sein wird.

Der Klauselgraph kann über alle Arten von graphentheoretischen Algorithmen analysiert werden, ist ein anscheinend natürliches Maß für "Struktur" und mit starken Verbindungen zur Messung / Schätzung der Härte verbunden, und es scheint, dass die Erforschung dieser Struktur und ihrer Implikationen noch sehr früh ist Stufen. Es ist nicht unvorstellbar, dass die Übergangspunktforschung, eine traditionelle und gut untersuchte Methode, um sich dieser Frage zu nähern, irgendwann in diese Klauselgraphenstruktur eingebunden wird (bis zu einem gewissen Grad bereits). mit anderen Worten, der Übergangspunkt in SAT kann "aufgrund" der Struktur des Klauselgraphen als vorhanden angesehen werden.

Hier ist eine hervorragende Referenz in dieser Richtung, eine Doktorarbeit von Herwig, es gibt viele andere.

[1] Zerlegen von Erfüllbarkeitsproblemen oder Verwenden von Diagrammen, um einen besseren Einblick in Erfüllbarkeitsprobleme zu erhalten , Herwig 2006 (83 Seiten).

Es ist einfach, alle Instanzen in der Nähe des "Übergangspunkts" so weit vom "Übergangspunkt" zu verschieben, wie es gewünscht wird. Die Bewegung beinhaltet ein Polynom Zeit / Raum Aufwand.

Wenn Instanzen, die weit vom "Übergangspunkt" entfernt sind, leichter zu lösen sind, müssen die Instanzen in der Nähe des Übergangspunkts ebenso einfach zu lösen sein. (Polynomtransformationen und alle.)

Diese wichtige Arbeit [1] von Toby Walsh bezieht sich auf den SAT-Übergang, gemessen im Verhältnis von Klausel zu Variable. Es geht jedoch noch weiter bei der Messung einer Eigenschaft namens Constrainedness , . Es ist ein raues oder möglicherweise natürliches Maß für die Härte, sodass über- oder unterbeschränkte Probleme an einem kritischen Zwischenpunkt einfacher sind als Einschränkungen.$\kappa$

Es findet eine scheinbare fraktale Selbstähnlichkeitsstruktur von Hard Instances in Bezug auf den Constrainedess-Parameter, sodass ein DP (LL) -Löser während der Suche dazu neigt, Unterprobleme mit derselben kritischen Constrainedness zu finden, unabhängig davon, welche Variable als nächstes für den Zweig ausgewählt wird. Es gibt einige weitere Analysen der fraktalen Struktur in SAT-Instanzen (wie die Hausdorff-Dimension von SAT-Formeln und die Verbindung zur Härte) in zB [2,3].

Eine andere, etwas verwandte Fragestellung ist die Beziehung von kleinen Weltgraphen zu (harten) SAT-Strukturen, zB [4,5].

Natürlich gilt in diesem Bereich die Regel, dass eine sehr eindeutige Antwort auf diese Frage inhärent nahe an einem P NP-$\stackrel{?}{=}$ Beweis liegt oder dass ein solcher Beweis der beste / nahe wäre (wird?) -Finale Antwort auf die Frage.

[1] The Constrainedness Knife von Toby Walsh 1998

[2] SELBSTÄHNLICHKEIT ZUFRIEDENSTELLENDER BOOLEAN-AUSDRÜCKE, DIE VON Ni und Wen NACH GRAPH DIRECTED ITERATED FUNCTION SYSTEMS FESTGELEGT SIND

[3] Visualisierung der internen Struktur von SAT-Instanzen (Vorbericht) Sinz

[4] Suche in einer kleinen Welt von Walsh 1999

[5] Modellierung realistischerer SAT-Probleme von Slater 2002