Messung der Schwierigkeit der SAT -Instanzen

Question

Angesichts einer Instanz von SAT möchte ich schätzen können, wie schwierig es sein wird, die Instanz zu lösen.

Eine Möglichkeit besteht darin, vorhandene Löser auszuführen, aber diese Art von Niederlagen des Zwecks der Schätzung der Schwierigkeit. Ein zweiter Weg könnte ein Verhältnis von Klauseln zu Variablen suchen, wie es für Phasenübergänge in Zufalls-SAT getan wird, aber ich bin sicher, dass es bessere Methoden gibt.

Gibt es angesichts einer Instanz von SAT einige schnelle Heuristiken, um die Schwierigkeit zu messen? Die einzige Bedingung ist, dass diese Heuristiken schneller sind als tatsächlich vorhandene SAT -Solvers auf der Instanz.

---

Verwandte Frage

Welche SAT -Probleme sind einfach? auf csthory.se. Diese Fragen stellt nach vorstellbaren Instanzen. Dies ist eine ähnliche Frage, aber nicht genau gleich. Ich interessiere mich sehr für eine Heuristik, die angesichts einer einzigen Instanz eine Art halbtelligentes Vermutung macht, wenn die Instanz schwer zu lösen ist.

Answer 1

Im Allgemeinen ist dies eine sehr relevante und interessante Forschungsfrage. "Eine Möglichkeit ist, vorhandene Löser auszuführen ..." und was würde uns das überhaupt genau sagen? Wir konnten empirisch erkennen, dass eine Instanz für einen bestimmten Löser oder einen bestimmten Algorithmus/Heuristik schwierig erscheint, aber was sagt es wirklich über die Härte der Instanz?

Ein Weg, der verfolgt wurde, ist die Identifizierung verschiedener struktureller Eigenschaften von Instanzen, die zu effizienten Algorithmen führen. Es wird in der Tat vorgezogen, diese Eigenschaften "leicht" identifizierbar zu sein. Ein Beispiel ist die Topologie des zugrunde liegenden Einschränkungsdiagramms, gemessen mit verschiedenen Parametern der Graphenbreite. Zum Beispiel ist bekannt, dass eine Instanz in der Polynomzeit lösbar ist, wenn die Baumbreite des zugrunde liegenden Einschränkungsdiagramms durch eine Konstante begrenzt wird.

Ein anderer Ansatz hat sich auf die Rolle von konzentriert Versteckte Struktur von Instanzen. Ein Beispiel ist das Hintertür -Set, Das verbleibende Problem vereinfacht das verbleibende Problem zu einer übersetzbaren Klasse. Zum Beispiel, Williams et al., 2003 1] Zeigen Sie, dass selbst bei Berücksichtigung der Kosten für die Suche nach Backdoor -Variablen auch bei der Konzentration auf ein Hintertür -Set ein Gesamtvorteil erhalten wird, sofern das Set ausreichend gering ist. Außerdem, Dilkina et al., 2007 2] Beachten Sie, dass ein Löser rief Satz-rand ist bemerkenswert gut darin, kleine starke Hintertüren in einer Reihe von experimentellen Domänen zu finden.

In jüngerer Zeit, Ansotegui et al., 2008 3] schlagen die Verwendung der baumartigen Raumkomplexität als Maß für DPLL-basierte Löser vor. Sie beweisen, dass auch ein konstantem Raum die Existenz eines Polynomzeitentscheidungsalgorithmus impliziert, wobei der Raum der Grad des Polynoms ist (Satz 6 in der Arbeit). Darüber hinaus zeigen sie, dass der Raum ist kleiner als die Größe der Zyklusschnitte. Tatsächlich ist der Raum unter bestimmten Annahmen auch kleiner als die Größe der Hintertüren.

Sie formalisieren auch, wonach Sie denken, dass Sie suchen, das heißt:

Finden Sie eine Maßnahme $ psi $ und einen Algorithmus, der eine Formel $ gamma $ befriedigt, die die Zufriedenheit in der Zeit $ o (n^{ psi ( gamma)}) $ entscheidet. Je kleiner die Maßnahme ist, desto besser charakterisiert es das Härte einer Formel.

---

1] Williams, Ryan, Carla P. Gomes und Bart Selman. "Hintertüren zur typischen Fallkomplexität." Internationale gemeinsame Konferenz über künstliche Intelligenz. Vol. 18, 2003.

2] Dilkina, Bistra, Carla Gomes und Ashish Sabharwal. "Kompromisse bei der Komplexität der Erkennung von Hintertüren." Prinzipien und Praxis der Einschränkungsprogrammierung (CP 2007), S. 256-270, 2007.

3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy und Felip Manya. "Messung der Härte von SAT -Instanzen." In Proceedings der 23. Nationalen Konferenz über künstliche Intelligenz (AAAI'08), S. 222-228, 2008.

Answer 2

Da Sie den Phasenübergang kennen, können Sie mir einige andere einfache Überprüfungen erwähnen, die mir bekannt sind (die wahrscheinlich durch die Einschränkungsgraphenanalyse subsumiert werden):

• Einige frühe zufällige SAT -Generatoren erzeugten versehentlich meist einfache Formeln, da sie "konstante Dichte" verwendeten, was einen ungefähr gleichen Anteil aller Klausellängen bedeutet. Diese waren größtenteils einfach, da 2-Klauseln und Einheiten das Problem erheblich vereinfachen, wie man es erwarten sollte, und wirklich lange Klauseln entweder viel Verzweigung hinzufügen oder die Hyperauflösung noch besser erleichtern. Es erscheint also besser, sich an Klauseln mit fester Länge zu halten und andere Parameter zu variieren.
• In ähnlicher Weise ist eine starke Vereinfachungsregel eine reine wörtliche Eliminierung. Offensichtlich ist eine Formel wirklich nur so schwer wie die Anzahl der unreinen Literalen, die sie hat. Weil die Auflösung neue Klauseln nummeriert $ | x |*| lnot x | $ (Bedeutung, das Produkt von Vorkommen von $ x $ und seine Negation), die Anzahl der Resolventionen wird maximiert, wenn für jede Variable eine gleiche Anzahl von positiven und negativen Literalen vorliegt. Daher ausgeglichene SAT -Generatoren.
• Es gibt auch eine Technik namens "No Dreieck SAT", die ziemlich frisch zu sein scheint [1], was eine Art Hard-Instance-Generator ist, der "Dreiecke" verbietet. Ein Dreieck ist eine Reihe von Klauseln mit 3 Variablen $ v_1, v_2, v_3 $ die in allen Kombinationen in einigen Klauseln paarweise auftreten (dh,, $ {v_1, v_2, ... }, {v_2, v_3, ... }, {v_1, v_3, ... } $). Offensichtlich machen Dreiecke für bekannte Löser eine Formel leichter.

[1] https://arxiv.org/pdf/1903.03592.pdf

Answer 3

Zusätzlich zu JUHOs hervorragender Antwort finden Sie einen weiteren Ansatz:

Ercsey-Ravasz & Toroczkai, Optimierungshärte als vorübergehendes Chaos in einem analogen Ansatz zur Beschränkung der Zufriedenheit, Nature Physics Band 7, Seiten 966–970 (2011).

Dieser Ansatz soll das SAT -Problem in ein dynamisches System umschreiben, wo jeder Attraktor des Systems ist eine Lösung für das SAT -Problem. Die Anziehungsbecken des Systems sind fraktaler, da das Problem schwieriger wird, und daher kann die "Schwierigkeit" der SAT -Instanz gemessen werden, indem untersucht wird, wie chaotisch die Transienten sind, bevor das System konvergiert.

In der Praxis bedeutet dies, ein paar Löser aus verschiedenen Anfangspositionen zu beginnen und die Rate zu untersuchen, mit der Löser den chaotischen Transienten entkommen, bevor sie zu einem Attraktor gelangen.

Es ist nicht schwer, ein dynamisches System zu entwickeln, für das die "Lösungen" Lösungen für ein bestimmtes SAT -Problem sind, aber es ist etwas schwieriger, sicherzustellen, dass die Lösungen alle Attraktoren und keine Repeller sind. Ihre Lösung besteht darin, Energievariablen (ähnlich wie LaGrange -Multiplikatoren) einzuführen, um darzustellen, wie stark eine Einschränkung verletzt wird, und zu versuchen, das System zu erhalten, um die Energie des Systems zu minimieren.

Interessanterweise können Sie mit ihrem dynamischen System SAT -Probleme in der Polynomzeit auf einem analogen Computer lösen, was an sich ein bemerkenswertes Ergebnis ist. Es gibt einen Haken; Möglicherweise erfordern es exponentiell große Spannungen, um die Energievariablen darzustellen, sodass Sie dies leider auf physischer Hardware nicht realisieren können.