A Fast Parallel SAT-Solver - Efficient Workload Balancing

Böhm, Max and Speckenmeyer, Ewald (1996) A Fast Parallel SAT-Solver - Efficient Workload Balancing.
Published in: Annals of Mathematics and Artificial Intelligence Vol. 17 (2). pp. 381-400.


We present a fast parallel SAT-solver on a message based MIMD machine. The input formula is dynamically divided into disjoint subformulas. Small subformulas are solved by a fast sequential SAT-solver running on every processor, which is based on the Davis-Putnam procedure with a special heuristic for variable selection. The algorithm uses optimized data structures to modify boolean formulas. Additionally efficient workload balancing algorithms are used, to achieve a uniform distribution of workload among the processors.We consider the communication network topologies d-dimensional processor grid and linear processor array. Tests with up to 256 processors have shown very good efficiency-values (>0.95).

Download: [img] Postscript - Preprinted Version
Download (242kB) | Preview
Editorial actions: View Item View Item (Login required)
Deposit Information:
ZAIK Number: zpr94-159
Depositing User: Archive Admin
Date Deposited: 13 Sep 2002 00:00
Last Modified: 19 Dec 2011 09:46
URI: http://e-archive.informatik.uni-koeln.de/id/eprint/159