SAT-Löser bieten eine leistungsstarke Möglichkeit, die Gültigkeit einer Booleschen Formel mit einem Quantifizierer zu überprüfen.
Zum Beispiel, um die Gültigkeit von zu überprüfen . φ ( x ) können wir einen SAT-Löser verwenden, um zu bestimmen, ob φ ( x ) erfüllt werden kann. Überprüfung der Gültigkeit von ∀ x . φ ( x ) können wir einen SAT-Löser verwenden, um zu bestimmen, ob ¬ φ ( x ) erfüllt werden kann. (Hier ist x = ( x 1 , … , x n ) ein n -Vektor von booleschen Variablen und φ ist eine Boolesche Formel.)
QBF-Solver dienen dazu, die Gültigkeit einer Booleschen Formel mit einer beliebigen Anzahl von Quantifizierern zu überprüfen.
Was ist, wenn wir eine Formel mit zwei Quantifizierern haben? Gibt es effiziente Algorithmen zur Überprüfung der Gültigkeit, die besser sind, als nur generische Algorithmen für QBF zu verwenden? gesagt habe ich eine Formel der Form ∀ x . ∃ y . ψ ( x , y ) (oder ∃ x . ∀ y . ψ ( x , y ) ) und möchten dessen Gültigkeit überprüfen. Gibt es dafür gute Algorithmen? Edit 4/8: Ich habe gelernt, dass diese Klasse von Formeln manchmal als 2QBF bezeichnet wird, daher suche ich nach guten Algorithmen für 2QBF.
Spezialisierung weiter: In meinem speziellen Fall habe ich eine Formel der Form dessen Gültigkeit ich überprüfen möchte, wobei f , g Funktionen sind, die eine k- Bit-Ausgabe erzeugen . Gibt es Algorithmen, mit denen die Gültigkeit dieser bestimmten Formelsorte effizienter überprüft werden kann als mit generischen Algorithmen für QBF?
PS: Ich frage nicht nach der Worst-Case-Härte in der Komplexitätstheorie. Ich frage nach praktisch nützlichen Algorithmen (so wie moderne SAT-Löser bei vielen Problemen praktisch nützlich sind, obwohl SAT NP-vollständig ist).
Antworten:
Wenn ich ganz offen für mich werben darf, haben wir im letzten Jahr einen Artikel über diesen abstraktionsbasierten Algorithmus für 2QBF geschrieben . Ich habe eine Implementierung für qdimacs, die ich bereitstellen kann, wenn Sie dies wünschen, aber aus meiner Erfahrung heraus kann es von großem Vorteil sein, den Algorithmus auf ein bestimmtes Problem zu spezialisieren. Es gibt auch eine ältere Veröffentlichung Eine vergleichende Studie zu 2QBF-Algorithmen , in der auch relativ leicht implementierbare Algorithmen vorgestellt werden.
quelle
Ich habe zwei Artikel dazu gelesen, einen speziell zu 2QBF. Die Papiere sind die folgenden:
Inkrementelle Determinierung , Markus N. Rabe und Sanjit Seshia, Theorie und Anwendung von Erfüllbarkeitstests (SAT 2016).
Sie haben ihren Algorithmus in einem Tool namens CADET implementiert . Die Grundidee besteht darin, der Formel schrittweise neue Bedingungen hinzuzufügen, bis Bedingungen eine eindeutige Skolem-Funktion beschreiben oder deren Abwesenheit bestätigt wird.
Zweitens Incremental QBF Solving , Florian Lonsing und Uwe Egly.
Implementiert in einem Tool namens DepQBF . Die Anzahl der Quantifiziererwechsel wird nicht eingeschränkt. Es beginnt mit der Annahme, dass wir eng verwandte qbf-Formeln haben. Es basiert auf inkrementellem Lösen und wirft nicht die Klauseln aus, die beim letzten Lösen gelernt wurden. Es fügt der aktuellen Formel Klauseln und Cubes hinzu und stoppt, wenn Klauseln oder Cubes leer sind und unsat oder sat darstellen.
Bearbeiten : Nur um zu sehen, wie gut diese Ansätze für 2QBF-Benchmarks funktionieren. Bitte sehen Sie sich die Ergebnisse des QBFEVal-2018 für die Ergebnisse des jährlichen QBF-Wettbewerbs QBFEVAL an . Im Jahr 2019 gab es keine 2QBF-Spur.
Diese beiden Ansätze funktionieren also in der Praxis sehr gut (zumindest bei den QBFEVAL-Benchmarks).
quelle
quelle