Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers

Recent attempts to create versions of Satisfiability (SAT) solvers that exploit parallel hardware and information shar-ing have met with limited success. In fact, the most suc-cessful parallel solvers in recent competitions were based on portfolio approaches with little to no exchange of informa-tion between processors. This experience contradicts the ap-parent parallelizability of exploring a combinatorial search space. We present evidence that this discrepancy can be ex-plained by studying SAT solvers through a proof complexity lens, as resolution refutation engines. Starting with the obser-vation that a recently studied measure of resolution proofs, namely depth, provides a (weak) upper bound to the best possible speedup achievable by such solvers, we empirically show the existence of bottlenecks to parallelizability that res-olution proofs typically generated by SAT solvers exhibit. Further, we propose a new measure of parallelizability based on the best-case makespan of an offline resource constrained scheduling problem. This measure explicitly accounts for a bounded number of parallel processors and appears to em-pirically correlate with parallel speedups observed in prac-tice. Our findings suggest that efficient parallelization of SAT solvers is not simply a matter of designing the right clause sharing heuristics; even in the best case, it can be — and in-deed is — hindered by the structure of the resolution proofs current SAT solvers typically produce