A Distributed Algorithm to Evaluate Quantified Boolean Formulae

In this paper, we present PQSOLVE, a distributed theorem-prover for Quantified Boolean Formulae. First, we introduce our sequential algorithm QSOLVE, which uses new heuristics and improves the use of known heuristics to prune the search tree. As a result, QSOLVE is more efficient than the QSAT-solvers previously known. We have parallelized QSOLVE. The resulting distributed QSAT-solver PQSOLVE uses parallel search techniques, which we have developed for distributed game tree search. PQSOLVE runs efficiently on distributed systems, i. e. parallel systems without any shared memory. We briefly present experiments that show a speedup of about 114 on 128 processors. To the best of our knowledge we are the first to introduce an efficient parallel QSAT-solver.

Authors

• Rainer Feldmann Burkhard Monien
• and Stefan Schamberger University of Paderborn

Keywords

No keywords are indexed for this paper.