Konvertieren von (mathematischen) Problemen in SAT-Instanzen

Ich möchte ein mathematisches Problem in ein boolesches Erfüllbarkeitsproblem (SAT) umwandeln und es dann mit einem SAT-Solver lösen. Ich frage mich, ob jemand ein Handbuch, eine Anleitung oder etwas anderes kennt, das mir hilft, mein Problem in eine SAT-Instanz umzuwandeln.

Außerdem möchte ich dies in einer besseren als einer exponentiellen Zeit lösen. Ich hoffe ein SAT Solver hilft mir weiter.

Kapitel 2 des SAT-Handbuchs (von Steven Prestwich) befasst sich eingehend mit der Umwandlung diskreter Entscheidungsprobleme in CNF. (Leider glaube ich nicht, dass eine Entwurfsversion online ist - am besten konsultieren Sie Ihre lokale Bibliothek.) Einige der anderen Referenzen, die in Magnus Björks skurriler Übersicht Erfolgreiche SAT-Codierungstechniken zitiert werden, sind ebenfalls nützlich.

Wenn Ihre Probleme andauern oder Sie sich besonders für Ungleichungssysteme interessieren, sind andere Arten von Lösern mit größerer Wahrscheinlichkeit nützlich. Wie Kyle betont , könnten SMT-Löser (wie Z3 , Yices oder OpenSMT ) nützlich sein, obwohl sich SMT-Theorien traditionell auf die Verifizierung von Computersoftware konzentrieren, sodass SMT-Löser in der Regel Ausdrücke mit Intervallen von ganzen Zahlen hervorragend unterstützen , kann aber bei Injektionsbeschränkungen schlecht abschneiden. Bei Problemen, die auf natürliche Weise als Ungleichungssysteme ausgedrückt werden, ist CPLEX dasjenige, das es zu überwinden gilt (früher war es für die akademische Nutzung kostenlos verfügbar, und möglicherweise ist es noch vorhanden). Bei einigen kombinatorischen Entscheidungsproblemen (wie zPackungen von Rechtecken zu Quadraten ), Constraint-Löser wie Minion übertreffen SAT-Löser und sind häufig einfacher zu verwenden.

Wenn Sie mathematische Probleme nicht als Lernübung in SAT-Instanzen übersetzen, wird Ihre Zeit viel fruchtbarer damit verbracht, sich mit Modulo-Theorien der Erfüllbarkeit zu befassen . Mit SMT können Sie Gleichungen und andere Einschränkungen viel natürlicher ausdrücken als mit booleschen SAT-Instanzen. Einige SMT-Löser unterstützen existenzielle und universelle Quantifizierer, sodass Sie über NP hinausgehen und PSPACE-Probleme ausdrücken können.

SMT-Löser sind nicht nur aussagekräftiger, sondern auch schneller. Nicht P = NP schneller, aber effizienter, da ein guter SMT-Löser keine theoriespezifischen Strukturinformationen verwirft, die den Löser durch den Suchraum führen. Wenn Sie eine Karp-Reduktion direkt auf eine SAT-Instanz anwenden, muss der SAT-Solver die gesamte Struktur neu lernen, was häufig zu exponentiellen Kosten führt. Beispielsweise geht die Tatsache, dass die Addition kommutativ ist, sowohl bei DPLL-basierten als auch bei lokalen suchbasierten SAT-Solvern verloren. Dem Löser ist nicht bewusst, dass es sich überhaupt um Zahlen handelt! Um zu vermeiden, dass alle Permutationen von x + y + z = 10 ausprobiert werden, benötigt ein SAT-Löser symmetriebrechenden Code, der eine Graph-Automorphismus-Erkennung erfordert. Die besten aktuellen Algorithmen zur Erkennung des Automorphismus von Graphen benötigen im schlimmsten Fall eine Zeit, die der Anzahl der Eckpunkte entspricht.

Zwei Tools, die Hochsprachen in SMT oder CNF konvertieren.

CVC Die Syntax ist CAS ähnlich.

CBMC Konvertiert ein C-Programm in CNF, wodurch Aussagen möglich werden. Die Aussagen sind entweder immer wahr oder wenn falsch, wird eine Gegenbeispieleingabe gefunden. CBMC löst Schleifen auf, sodass bestimmte C-Programme einen exponentiell großen CNF / SMT aufweisen.