Deterministic Parallel DPLL

Youssef Hamadi, Said Jabbour, Cedric Piette, Lakhdar Sais


Current parallel SAT solvers suffer from a non-deterministic behavior. This is the consequence of their architectures which rely on weak synchronizing in an attempt to maximize performance. This behavior is a clear downside for practitioners, who are used to both runtime and solution reproducibility. In this paper, we propose the first Deterministic Parallel DPLL engine. Our experimental results clearly show that our approach preserves the performance of the parallel portfolio approach while ensuring full reproducibility of the results.


SAT solving, parallelism

Full Text:



  • There are currently no refbacks.