A Distributed Algorithm to Evaluate Quantified Boolean Formulae

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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 about114 on 128 processors.To the best of our knowledge we are the first to introduce an efficient parallel QSAT-solver.