A Distributed Algorithm to Evaluate Quantified Boolean Formulae

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

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.