PaQuBE

| project staff | description | benchmarks | publications |

PaQuBE is the parallel version of the search-based QBF Solver QuBE6. This is achieved by extending its sequential core by a Master/Slave architecture based on the Message Passing Interface (MPI), that allows to divide the problems being solved over an arbitrary number of distributed processes. It also is the first parallel solver supporting advanced knowledge sharing, in which solution cubes as well as conflict clauses can be shared. In addition, solution cubes are compressed before sending, so that the network traffic overhead due to broadcasting MPI messages is reduced. Lastly, when PaQuBE was introduced, it was able to solve multiple QBF problems that had remained unsolved for years by all other QBF solvers.

PaQuBE was developed within the DAAD/Vigoni project "Bounded Model Checking of Blackbox Designs via Quantified Boolean Formulas" in co-operation with the STAR-Lab research group of University of Genoa, Italy, that is co-responsible for the distribution.

Any Quantified Boolean Formula (QBF) in QDimacs format. QBFLIB is the official library of QBF formulas.