Uni-Logo
English       Login
Rechnerarchitektur - Arbeitsgruppe Bernd Becker
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

QMiraXT

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur
Matthew Lewis, Dr. Entwickler
Lehrstuhl für Rechnerarchitektur
Paolo Marin, PhD Kontakt


Beschreibung

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.



Benchmarks

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



Publikationen
Matthew Lewis, Tobias Schubert, Bernd Becker
QMiraXT - A Multithreaded QBF Solver
GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2009