PaQuBE

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

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.

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