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.

PDF file

Details