×

zbMATH — the first resource for mathematics

Parallel SAT solving using bit-level operations. (English) Zbl 1170.68594
Summary: We show how to exploit the 32/64 bit architecture of modern computers to accelerate some of the algorithms used in satisfiability solving by modifying assignments to variables in parallel on a single processor. Techniques such as random sampling demonstrate that while using bit vectors instead of Boolean values solutions to satisfiable formulae can be obtained faster. Here, we reveal that more complex algorithms like unit propagation and detection of autarkies, can be parallelized efficiently, as well.
We capitalize on the developed parallel algorithms by modifying the state-of-the-art local search SAT solver UnitWalk accordingly. Experiments show that the parallel version performs much faster than the original implementation.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
PSATO; SATO; UnitWalk
PDF BibTeX XML Cite