Theoretische Erklärungen für den praktischen Erfolg von SAT-Lösern?

Welche theoretischen Erklärungen gibt es für den praktischen Erfolg von SAT-Lösern, und kann jemand einen Überblick im "Wikipedia-Stil" geben und sie alle zusammenfassen?

Analog dazu liefert die geglättete Analyse ( arXiv-Version ) für den Simplex-Algorithmus eine hervorragende Erklärung dafür, warum sie in der Praxis so gut funktioniert, obwohl sie im schlimmsten Fall exponentielle Zeit in Anspruch nimmt und NP-mächtig ist ( arXiv-Version ).

Ich habe ein bisschen über Dinge wie Hintertüren, Struktur des Klauselgraphen und Phasenübergänge gehört, aber (1) ich sehe nicht, wie diese alle zusammenpassen, um das größere Bild zu ergeben (wenn sie das tun), und (2) Ich weiß nicht, ob dies wirklich erklärt, warum SAT-Löser beispielsweise auf industriellen Instanzen so gut funktionieren. Auch wenn es um Dinge wie die Struktur des Klauselgraphen geht: Warum können aktuelle Löser bestimmte Klauselgraphenstrukturen nutzen?

Die Ergebnisse zu Phasenübergängen finde ich diesbezüglich zumindest nach meinem derzeit eingeschränkten Verständnis nur teilweise befriedigend. Der Phasenübergang Literatur ist über Fälle von zufälligen k-SAT, aber ist das wirklich etwas über reale Fälle erklären? Ich erwarte nicht, dass reale SAT-Instanzen wie zufällige Instanzen aussehen. sollte ich? Gibt es einen Grund zu der Annahme, dass Phasenübergänge auch intuitiv etwas über reale Instanzen aussagen, selbst wenn sie nicht wie zufällige Instanzen aussehen?

Verwandte Fragen, die helfen, aber meine Frage nicht vollständig beantworten, insbesondere die Frage, ob Dinge zu einem zusammenhängenden Bild zusammengefügt werden sollen:

• Warum gibt es einen enormen Unterschied zwischen SAT-Lösern?

• Welche SAT-Probleme sind einfach?

• Was ist die Korrelation zwischen Baumbreite und Instanzhärte aus zufälligen 3SAT?

Ich gehe davon aus, dass Sie sich bei Benchmark-Datensätzen, wie sie im SAT-Wettbewerb verwendet werden, auf CDCL-SAT-Löser beziehen . Diese Programme basieren auf vielen Heuristiken und vielen Optimierungen. Im Workshop Theoretische Grundlagen des angewandten SAT-Lösens in Banff im Jahr 2014 wurden einige sehr gute Einführungen in ihre Arbeitsweise gegeben ( Videos ).

Diese Algorithmen basieren auf dem DPLL-Backtracking-Algorithmus, der versucht, eine zufriedenstellende Zuordnung zu finden, indem Werte für Variablen und Backtracks festgelegt werden, wenn ein Konflikt festgestellt wird. Die Leute haben sich angesehen, welchen Einfluss diese Heuristiken haben. ZB sehen

• Hadi Katebi, Karem A. Sakallah und Joao P. Marques-Silva, " Empirische Untersuchung der Anatomie moderner Sat-Löser ", 2011

Es scheint, dass die Effizienz dieser SAT-Löser in Bezug auf die Benchmarks hauptsächlich von zwei Heuristiken (und ihren Varianten) herrührt:

1. VSIDS-Heuristik zur Auswahl der Variablen, auf die als Nächstes verzweigt werden soll.
2. CDCL: Konfliktgetriebene Klausellernheuristik, die eine neue Klausel aus einem Konflikt lernt.

Es ist bekannt, dass DPLL-Beweise Beweisen in der Auflösung entsprechen. Ohne CDCL sind die einzigen Auflösungsnachweise, die wir erhalten können, Baumauflösungsnachweise, die viel schwächer sind als allgemeine Auflösungsnachweise.

Es gibt Ergebnisse, die zeigen, dass wir mit CDCL einen allgemeinen Auflösungsnachweis erhalten können. Es gibt jedoch Vorbehalte, sie erfordern viele künstliche Neustarts, künstliche Verzweigungen und / oder eine bestimmte Vorverarbeitung, so dass nicht klar ist, inwieweit diese dem entsprechen, was diese Programme in der Praxis tun. Siehe zB das folgende Papier für mehr Details:

• Paul Beame und Ashish Sabharwal, " Nicht neu startende SAT-Solver mit einfacher Vorverarbeitung können die Auflösung effizient simulieren ", 2014

CDCL schneidet im Wesentlichen Zweige aus dem Suchraum. Es gibt verschiedene Möglichkeiten, eine neu erlernte Klausel aus einem Konflikt abzuleiten. Im Idealfall fügen wir eine Reihe von Minimalklauseln hinzu, die den Konflikt implizieren. In der Praxis kann dies jedoch umfangreich und teuer in der Berechnung sein. Top-SAT-Löser löschen häufig gelernte Klauseln regelmäßig, was in der Praxis hilfreich ist.

$\alpha$$F(v,i)$$i$$0<\alpha<1$$v$$n$

Intuitiv kann man sagen, dass damit versucht wird, Variablen hervorzuheben, die konsequent in aktuelle Konflikte verwickelt waren. Sie können sich das auch als eine vereinfachte, aber äußerst kostengünstige Methode vorstellen, um vorherzusagen, welche Variablen in den nächsten Konflikt verwickelt sein werden. VSIDS verzweigt sich also zuerst zu diesen Variablen. Man kann behaupten, dass der Algorithmus im Wesentlichen ein Fail-Fast-Algorithmus ist, Konflikte finden sich schnell. Fast bezieht sich auf eine geringere Anzahl festgelegter Variablen, was bedeutet, dass große Teilbäume des Suchbaums blockiert werden. Aber dies ist meistens eine Intuition, afaik niemand hat es sehr sorgfältig formalisiert, um es an SAT-Datensätzen zu testen. Das Ausführen eines SAT-Lösers für einen dieser Datensätze ist nicht billig, geschweige denn der Vergleich mit den optimalen Entscheidungen (kleinste Erweiterung der aktuellen Zuordnung zu Variablen, die eine der Klauseln verletzen würden). VSIDS hängt auch davon ab, auf welche Variablen wir bei jedem Konflikt stoßen. Es gibt verschiedene Möglichkeiten, zu definieren, wann eine Variable in einen Konflikt verwickelt ist.

Es gibt Ergebnisse, die zeigen, dass eine bestimmte Implementierung dieser Ideen einer zeitgewichteten Zentralität von Eckpunkten in dynamischen Graphen entspricht.

Es gibt auch Vorschläge, nach denen der Rest der Instanzen, die auf NP-harten Problemen und Krypto-Primitiven sowie auf zufälligen Instanzen basieren (in denen CDCL-SAT-Löser nicht gut sind), von sehr gut strukturierten Dingen wie Software- und Hardwareverifizierung und auf irgendeine Weise von diesen ausgeht Strukturen werden von CDCL-SAT-Solvern ausgenutzt (viele Ideen wurden erwähnt, z. B. Hintertüren, eingefrorene Variablen usw.), aber es handelt sich meistens um Ideen, für deren Sicherung keine soliden theoretischen oder experimentellen Beweise vorliegen. Ich denke, man müsste das genau definieren und zeigen, dass die Instanzen, auf denen diese Algorithmen gut funktionieren, die Eigenschaft haben und dann zeigen, dass diese Algorithmen diese Eigenschaften ausnutzen.

Einige Leute bestehen darauf, dass das Klauselverhältnis und die Schwellenwerte das einzige Spiel in der Stadt sind. Das ist definitiv falsch, wie jeder, der ein wenig mit der Funktionsweise industrieller SAT-Löser vertraut ist oder Kenntnisse über die Komplexität von Beweisen besitzt, wissen würde. Es gibt viele Dinge, die einen SAT-Solver in der Praxis gut oder schlecht funktionieren lassen, und die Klauselquote ist nur eines der Dinge, die möglicherweise eine Rolle spielen. Ich denke, die folgende Umfrage ist ein guter Ausgangspunkt, um die Zusammenhänge zwischen Beweiskomplexität und SAT-Lösern und -Perspektiven zu untersuchen:

• Jakob Nordstrom, " Über das Zusammenspiel von Beweiskomplexität und SAT-Lösung ", 2015

Interessanterweise ist sogar das Schwellenphänomen komplizierter als die meisten Leute denken. Moshe Vardi erklärte in seinem Vortrag " Phasenübergänge und rechnerische Komplexität ", dass die mittlere Laufzeit von GRASP für zufällige 3SAT-Formeln nach der Schwelle exponentiell bleibt, der Exponent jedoch abnimmt (afaik, es ist nicht klar, wie schnell es abnimmt).

Warum studieren wir SAT-Löser (als Komplexitätstheoretiker)? Ich denke, die Antwort ist dieselbe wie für andere Algorithmen: 1. Vergleichen Sie sie, 2. Finden Sie ihre Grenzen, 3. Entwerfen Sie bessere, 4. Beantworten Sie grundlegende Fragen der Komplexitätstheorie.

Bei der Modellierung einer Heuristik ersetzen wir die Heuristik häufig durch Nichtdeterminismus. Die Frage wird dann, ob es ein "fairer" Ersatz ist. Und hiermit meine ich fairerweise, wie nah das Modell daran ist, uns bei der Beantwortung der obigen Frage zu helfen.

Wenn wir einen SAT-Löser als Beweissystem modellieren, zeigen wir teilweise seine Einschränkung, da der Algorithmus für Anweisungen mit niedrigeren Grenzen im Beweissystem ineffizient ist. Es besteht jedoch immer noch eine Lücke zwischen dem, was der Algorithmus tatsächlich findet, und dem optimalen Beweis im Beweissystem. Wir müssen also zeigen, dass auch das Gegenteil der Fall ist, dh der Algorithmus kann Beweise finden, die so gut sind wie die im Beweissystem. Wir sind nicht nah dran, diese Frage zu beantworten, aber die Menge an Heuristik, die durch Nichtdeterminismus ersetzt wird, definiert, wie nah das Modell dem Beweissystem ist. Ich erwarte nicht, dass wir die Ersetzung der Heuristik durch Nichtdeterminismus vollständig einstellen, da wir sonst Automatisierbarkeitsergebnisse erhalten, die Konsequenzen für offene Probleme in der Krypto usw. haben.

Bei der Betrachtung eines Modells stellt sich also die Frage: Inwiefern helfen die Modelle zu erklären, warum der SAT-Löser A besser ist als der SAT-Löser B? Wie hilfreich sind sie bei der Entwicklung besserer SAT-Löser? Findet der SAT-Löser in der Praxis Beweise, die nahe an den optimalen Beweisen im Modell liegen? ... Wir müssen auch die praktischen Beispiele modellieren.

In Bezug auf die Intuition, dass CDCL-SAT-Löser "die Struktur praktischer Instanzen ausnutzen" (was auch immer diese Struktur ist), ist die Intuition meines Erachtens allgemein akzeptiert. Die eigentliche Frage ist, eine überzeugende Erklärung zu geben, was das bedeutet, und zu zeigen, dass es tatsächlich wahr ist.

Siehe auch Jakob Nordstroms eigene Antwort für neuere Entwicklungen.

Ich schreibe das ziemlich schnell, weil die Zeit sehr knapp ist (und ich habe aus demselben Grund nicht einmal früher geantwortet), aber ich dachte, ich würde versuchen, wenigstens mit meinen zwei Cent mitzumachen.

Ich halte dies für eine wirklich gute Frage und habe in den letzten Jahren nicht unwesentlich Zeit darauf verwendet, dies zu untersuchen. (Vollständige Offenlegung: Ich habe einen großen Teil meiner derzeitigen Finanzierung erhalten, um Antworten auf Fragen dieser Art zu finden und möglicherweise tiefere Einblicke in SAT in effizientere SAT-Löser umzuwandeln.)

Wenn man einen Satz beantworten müsste, denke ich

Niemand weiß es wirklich und dies ist ein aktives Forschungsgebiet

ist so ziemlich so gut wie es nur geht. Abgesehen davon, dass es viel mehr Raum für mehr Aktivität gibt, insbesondere von der theoretischen Seite.

Einige vorgeschlagene Erklärungen (die sich nicht gegenseitig ausschließen), die bereits in anderen Antworten und Kommentaren diskutiert wurden, sind

• (a) Hintertüren,
• (b) Überlegungen zur parametrisierten Komplexität,
• (c) Graphstruktur des CNF-Problems,
• d) Überlegungen zur Beweiskomplexität und
• (e) Phasenübergänge.

Ab dem Ende (e) scheint es hinsichtlich der Phasenübergänge einige Verwirrung zu geben. Die kurze Antwort lautet: Es gibt keinen Grund zu der Annahme, dass das Verhältnis von Klauseln zu Variablen für angewandte Probleme oder theoretische kombinatorische Probleme (auch als gestaltete Instanzen bezeichnet) relevant ist. Aber aus irgendeinem Grund ist es ein nicht allzu ungewöhnliches Missverständnis im angewandten Teil der SAT-Community, dass das Verhältnis von Klauseln zu Variablen irgendwie eine allgemein relevante Maßnahme sein sollte. Das Verhältnis von Klausel zu Variable ist für zufälliges k-SAT sehr relevant, für andere Modelle jedoch nicht.

Ich habe das Gefühl, dass Hintertüren (a) eine beliebte Erklärung waren, aber ich persönlich habe nicht wirklich überzeugende Beweise dafür gesehen, dass sie erklären, was in der Praxis vor sich geht.

Die parametrisierte Komplexität (b) liefert eine schöne Theorie über einige Aspekte von SAT, und eine sehr attraktive Hypothese ist, dass SAT-Instanzen einfach sind, weil sie dazu neigen, "in der Nähe einer Traktabilitätsinsel" zu sein. Ich denke, diese Hypothese eröffnet viele spannende Forschungsrichtungen. Wie in einigen Antworten erwähnt, gibt es viele Verbindungen zwischen (a) und (b). Bisher sehe ich jedoch keine Belege dafür, dass die parametrisierte Komplexität zu stark mit den tatsächlichen Gegebenheiten in der Praxis korreliert. Insbesondere scheinen Instanzen, die nachvollziehbar sind, in der Praxis sehr, sehr schwierig zu sein, und Instanzen ohne kleine Hintertüren können immer noch sehr einfach sein.

Die Erklärung, die mir für industrielle Fälle am glaubwürdigsten erscheint, ist (c), nämlich dass die (grafische) Struktur der fraglichen CNF-Formeln mit der praktischen SAT-Leistung korreliert werden sollte. Die Idee dabei ist, dass Variablen und Klauseln von industriellen Instanzen zu gut verbundenen Communities mit wenigen Verbindungen zusammengefasst werden können und dass SAT-Löser diese Struktur irgendwie ausnutzen. Leider scheint es ziemlich schwierig zu sein, dies strenger festzulegen, und ebenso leidet dieser Bereich leider unter ziemlich viel Hype. Die vorgeschlagenen Erklärungen, die ich bisher in Zeitungen gesehen habe, sind ziemlich unbefriedigend und die Modelle scheinen leicht abzuschießen zu sein. Das Problem scheint zu sein, dass, wenn man dies wirklich gründlich tun will, Dann wird die Mathematik wirklich schwierig (weil es ein schwieriges Problem ist) und es wird auch extrem chaotisch (weil Sie Ihr Modell nah genug an der Realität haben müssen, um relevante Ergebnisse zu erzielen). Insbesondere die Arbeiten, die ich gesehen habe, um zu erklären, dass die Leistung der VSIDS-Heuristik (Variable State Independent Decaying Sum) für variable Entscheidungen gut funktioniert, weil sie Communities in der Graphendarstellung der Instanzen untersucht, sind ziemlich nicht überzeugend, obwohl die Hypothese als solche immer noch besteht sehr attraktiv.

Ein Forschungsschwerpunkt, den ich persönlich verfolgt habe, ist die Frage, ob die praktische SAT-Leistung in irgendeiner Weise mit den Beweiskomplexitätsmaßen der betreffenden CNF-Formeln korreliert. Leider scheint die kurze Antwort zu sein, dass es wirklich keinen klaren und zwingenden Zusammenhang gibt. Es kann immer noch sein, dass es nichttriviale Zusammenhänge gibt (das untersuchen wir derzeit auf unterschiedliche Weise), aber es scheint, dass die Theorie zu schön und sauber und hübsch und die Realität zu chaotisch ist, um wirklich gut zusammenzupassen. (In Bezug auf die Abhandlung zum Nachweis von Komplexitätsmaßen und der praktischen Härte von SATvon Järvisalo, Matsliah, Nordström und Živný in CP '12 hat sich herausgestellt, dass detailliertere Experimente ein viel komplexeres Bild mit weniger klaren Schlussfolgerungen liefern. aber es ist kompliziert, aber trotzdem hoffentlich interessant.)

Eine weitere verwandte Aufgabe im Bereich der Beweiskomplexität besteht darin, hochmoderne SAT-Löser als Beweissysteme zu modellieren und in diesen Modellen Theoreme zu beweisen, um die Eigenschaften der entsprechenden Löser abzuleiten. Dies ist jedoch ein kleines Minenfeld, da kleine und scheinbar harmlose Konstruktionsentscheidungen auf der theoretischen Modellseite dazu führen können, dass die Ergebnisse aus praktischer Sicht so gut wie völlig irrelevant sind. Wenn man andererseits ein theoretisches Modell haben möchte, das der Realität nahe genug ist, um relevante Ergebnisse zu liefern, wird dieses Modell äußerst chaotisch. (Dies liegt daran, dass die Leistung des SAT-Lösers von der globalen Historie aller bisher nichttrivialen Vorgänge abhängt. Dies bedeutet, dass das Modell nicht so modular sein kann, wie wir es normalerweise in unseren Beweissystemen einrichten. Ob ein bestimmter Ableitungsschritt vorliegt "richtig"

Zwei Arbeiten, die wirklich als Ausnahmen hiervon erwähnt werden sollten, sind [Pipatsrisawat und Darwiche 2011] und [Atserias, Fichte und Thurley 2011], in denen gezeigt wird, dass konfliktgetriebene SAT-Löser mit Klausellernen auf natürliche Weise modelliert sind Potenzial zur polynomialen Simulation einer vollständigen, allgemeinen Auflösung. Es gibt eine ziemlich lange Liste von Artikeln vor [PD11] und [AFT11], die im Wesentlichen dasselbe Ergebnis behaupten, die jedoch alle schwerwiegende Probleme mit der Modellierung haben. (Es ist wahr, dass [PD11] und [AFT11] auch einige Annahmen benötigen, um zu funktionieren, aber sie sind so ziemlich die Minimalannahmen, die Sie erwarten würden, wenn Sie nicht nach Beiträgen fragen, die auch zeigen, dass die parametrisierte Komplexitätshierarchie zusammenbricht.)

Wiederum schreibe ich das alles sehr schnell, aber wenn es ein erhebliches Interesse für irgendetwas oben Genanntes gibt, könnte ich versuchen, es auszuarbeiten (obwohl es eine Weile dauern könnte, bis ich wieder darauf zurückkomme - bitte zögern Sie nicht, mich anzupingen, wenn ich da bin ist alles, was Sie möchten, dass ich kommentiere). Lassen Sie mich zur schnellen Referenzierung einige schamlose Self-Plugs machen (obwohl die Schande etwas nachlässt, wenn ich sehe, dass einige Kommentare auch einige dieser Referenzen zitiert haben):

Tutorial-artiger Vortrag über das Zusammenspiel von Beweiskomplexität und SAT-Lösung , gehalten an der Internationalen Sommerschule für Zufriedenheit, Modulo-Theorien zur Zufriedenheit und automatisiertes Reasoning im Jahr 2016, mit zahlreichen vollständigen Referenzen am Ende der Folien: http://www.csc .kth.se / ~ jakobn / research / TalkInterplaySummerSchool2016.pdf

Etwas jüngerer und kürzerer Umfragegespräch zum Verständnis konfliktbedingter SAT-Lösungen durch die Linse der Beweiskomplexität ab Anfang 2017 (auch mit vollständigen Referenzen am Ende): http://www.csc.kth.se/~jakobn/research /TalkProofComplexityLensCDCL1702.pdf

Übersicht über Zusammenhänge zwischen Beweiskomplexität und SAT-Lösung: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Quellenangabe: Jakob Nordström. Zum Zusammenspiel von Beweiskomplexität und SAT-Lösung. ACM SIGLOG News, Band 2, Nummer 3, Seiten 19-44, Juli 2015. (Leicht bearbeitete Version mit einigen Tippfehlern behoben.)]

SAT '16-Papier mit CDCL, das originalgetreu als Beweissystem modelliert wurde: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [ Quellenangabe : Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard , Jakob Nordström und Marc Vinyals. Kompromisse zwischen Zeit und Speicher in einem engeren Modell von CDCL-SAT-Solvern. In Proceedings of the 19. International Conference on Theory and Applications of Satisfiability Testing (SAT '16), Lecture Notes in Computer Science, Band 9710, Seiten 160-176, Juli 2016.]

Lassen Sie mich meine zwei Cent Verständnis hinzufügen, obwohl ich noch nie in der Gegend gearbeitet habe.

Sie stellen eine von zwei Fragen: "Welche Ansätze sind bekannt, um die theoretische Effizienz eines SAT-Lösers für bestimmte Instanzen zu beweisen?" Und "Warum sind SAT-Löser in der Realität effizient?".

Bei der ersten Frage möchte ich Sie nur auf die Recherche von Stefan Szeider verweisen. Er scheint mir der derzeit aktivste Bereich im Bereich der Backdoor- und FPT-Parametrisierung von SAT zu sein (der sowohl strukturelle Ansätze wie treewidth-Maßnahmen und sogenannte Backdoor-Sets als auch eine Mischung aus beiden umfasst).

Um ehrlich zu sein, wurde die letzte Frage bei jedem SAT-Lösungsworkshop, an dem ich teilgenommen habe (einschließlich der letzten Jahre), genau erörtert. Aber mein Eindruck ist wie folgt.

Zunächst müssen Sie quantifizieren oder einschränken, was Sie mit "in der Realität" meinen. Es ist nicht wahr, dass SAT-Löser universell gute Löser für jedes Problem sind, auf das Sie sie werfen (natürlich), und zwischen verschiedenen Problemen brauchen Sie am Ende unterschiedliche Strategien. Zum Beispiel gibt es in letzter Zeit mehrere Erfolge, bei denen mathematische Vermutungen durch eine enorme Computersuche mit Hilfe eines SAT-Lösers überprüft oder verschärft wurden. In diesem Fall sind die cleveren Verbesserungen und Heuristiken im CDCL-Stil, die moderne SAT-Löser normalerweise anwenden, anscheinend oftmals nicht sehr leistungsfähig, und das Spiel läuft auf eine clevere Art und Weise ab, Ihr Quellproblem aufzuteilen Teile, gefolgt von (im Wesentlichen) einem Brute-Force-Verzweigungsalgorithmus mit einem kleinen konstanten Faktor in der Laufzeit.

Möglicherweise habe ich diesen Punkt leicht überbewertet, aber mein Punkt war, dass SAT-Löser, als sie beispielsweise die Erdos-Diskrepanz-Vermutung angriffen, aus einem anderen Grund erfolgreich waren als wenn sie industrielle Instanzen lösten, die aus Schaltungstests stammten.

Wir müssen uns also die Frage stellen, warum CDCL-basierte Solver in industriellen Fällen, beispielsweise bei der Verifizierung von Schaltkreisen (Prüfung der Schaltkreisäquivalenz), so gut funktionieren. Denke ichdass die mächtigste Sicht (oder die Konsenssicht) hier die Suchstrategie eines CDCL-Lösers ist, passt sehr gut zur Struktur dieser Instanzen. Dies bedeutet zum Beispiel, dass die Schaltungen aus relativ komplexen Teilen (so genannten Clustern) bestehen, die durch relativ wenige und einfachere Verbindungen, möglicherweise auf hierarchische Weise, miteinander verbunden sind. und dass die CDCL-Löser mit all ihren Heuristiken sehr gut darin sind, dies (de facto) auszunutzen und diese Cluster auf die gemeinsam genutzten Variablen zu "projizieren", wie oder in welcher Reihenfolge dies für die Überprüfung der vorliegenden Schaltung am nützlichsten ist. Es scheint aber auch immer noch Konsens darüber zu bestehen, dass dies keine ausreichenden Erklärungen sind (z. B. können wir die Effizienz von CDCL-SAT-Solvern in diesem Bereich wahrscheinlich nicht theoretisch erklären, indem wir uns nur auf die Graphstruktur der Instanz beziehen).

Erklären die verfolgbaren Parametrisierungen letztere? Um ehrlich zu sein, ich weiß es nicht. Ich denke, es gibt wahrscheinlich einen starken Effekt im Spiel, dass die Instanzen in der realen Welt weder der schlimmste Fall sind, noch (wahrscheinlich) der wirklich durchschnittliche Fall gemäß einer Instanzverteilung, mit der wir umgehen können. Aber es lohnt sich wahrscheinlich immer noch zu fragen.

In CP '12 gibt es eine Veröffentlichung " Relating Proof Complexity Measures and Practical Hardness of SAT " von Matti Järvisalo, Arie Matsliah, Jakob Nordström und Stanislav Živný, die versucht, die Härte oder Leichtigkeit der Lösung bestimmter Formeln durch CDCL-Löser mit Auflösungsbeweisen zu verknüpfen Komplexitätsmaße, insbesondere Auflösungsbeweisraum. Die Ergebnisse sind etwas uneinheitlich, aber ich denke, es ist ein Schritt in die richtige Richtung.

Ich bin kein Experte auf diesem Gebiet, aber ich denke, dass das zufällige SAT / Phasenübergangs-Zeug fast nichts mit dem industriellen / praktischen Anwendungs-Zeug zu tun hat.

ZB basieren die sehr guten Löser für zufällige Instanzen (wie https://www.gableske.net/dimetheus ) auf den statistischen Methoden der Physik (Glaubensausbreitung usw.), wohingegen die sehr guten "allgemeinen" Löser (wie z Ich glaube, da http://fmv.jku.at/lingeling/ ) nicht verwandte Techniken verwenden (mehr wie das, worüber Kaveh sprach).

Aber wie gesagt, nimm vielleicht nicht mein Wort dafür; Dies kommt von einem bestimmten Nicht-Experten.