Deterministic Parallel DPLL
Youssef Hamadi, Saïd Jabbour, Cédric Piette, Lakhdar Saïs · Journal on Satisfiability Boolean Modeling and Computation · 2011
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