Antti E. J. Hyvarinen and Christoph M. Wintersteiger
1 May 2012
Parallelization of unit propagation in SAT solvers is a compelling
way of obtaining an efficient parallel decision procedure for the
propositional satisfiability problem. However, due to the P-completeness
of unit propagation, it is challenging to achieve good efficiency in practice.
In this article, we present two methods for unit propagation on
multi-core systems and their implementation. We throughly evaluate
these techniques by comparison to a simulation that estimates a baseline
efficiency and by experimental evaluation of an implementation on competition
benchmarks. We thereby demonstrate that achieving a speed-up
linear in the number of cores is indeed challenging in practice, but also
that unit propagation on multi-core systems is feasible in practice.