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

PaQuBE

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

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


Beschreibung

PaQuBE ist die parallele Version des such-basierten QBF Solvers QuBE6. Der sequentielle Kern des Solvers wurde um eine Master/Slave Architektur basierend auf Message Passing Interface (MPI) erweitert, die es erlaubt, QBF Probleme auf eine beliebige Anzahl an Prozessen zu verteilen. Weiterhin ist PaQuBE der erste parallele Solver, der advanced knowledge sharing unterstützt, das heißt sowohl solution cubes als auch Konfliktklauseln können ausgetauscht werden. Zudem werden solution cubes vor dem Senden komprimiert, so dass die Netzwerkauslastung verursacht durch MPI Nachrichten reduziert wird. Bei seiner Einführung konnte PaQuBE mehrere QBF Probleme lösen, die jahrelang für alle anderen Solver unlösbar blieben.

PaQuBE wurde im DAAD/VIGONI Projekt "Bounded Model Checking of Blackbox Designs via Quantified Boolean Formulas" in Kooperation mit der STAR-Lab Gruppe der Universität Genua, Italien entwickelt.



Benchmarks

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



Publikationen
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, and Enrico Giunchiglia
PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing
International Conference on Theory and Applications of Satisfiability Testing (SAT'09), 2009, pp 509--523, LNCS 5584, Springer
Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, and Bernd Becker
Comparison of Knowledge Sharing Strategies in a Parallel QBF Solver
High-Performance Computing and Simulation Conference (HPCS'09), 2009
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, and Enrico Giunchiglia
Parallel QBF Solving with Advanced Knowledge Sharing
Fundamenta Informaticae, vol. 107 no. 2--3, pp 139-166, 2011