QMiraXT

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

Dieser DPLL such-basierte Solver ist eine Erweiterung des multi-threaded SAT Solvers MiraXT. QMiraXT ist der erste moderne parallele QBF Solver, der knowledge sharing unterstützt. Mit ihm wurden viele Beschleunigungstechniken moderner SAT Solver in die QBF Domäne eingeführt. Dieses Tool unterstützt fortgeschrittene Techniken zur conflict und solution analysis sowie Lernen von Konfliktklauseln. Die bedeutendste Neuerung in QMiraXT ist die Enführung des Single Quantification Level Scheduling Algorithmus für parallele QBF Solver, welcher es erlaubt, große QBF Probleme in viele kleine Probleme effizient zu unterteilen. Somit kann mit QMiraXT verglichen mit früheren parallelen QBF Solvern eine deutlich höhere CPU Auslastung erreicht werden. Weiterführende Arbeit resultierte in PaQuBE.

Jede beliebige QBF in QDimacs Format. Eine Sammlung von QBF Problemen ist in der QBFLIB zu finden.