3 ms·
SAT solvers overwhelmingly don't use resolution. Modern state of the art solvers use DPLL/CDCL.
by andrepd 6y ago
SAT solvers overwhelmingly don't use resolution. Modern state of the art solvers use DPLL/CDCL.
- 53x15 6y agoI think neel_k was referring to the fact that when a DPLL or CDCL solver concludes UNSAT you can take the trace its backtracking activity and rewrite it from the bottom up as a resolution refutation. So in this sense the solvers are finding resolution proofs.
- CJefferson 6y agoWhile they indeed don't use resolution directly, DPLL/CDCL is in many ways equivalent. Most modern SAT solvers will still have trouble with the pigeon-hole style problems (although some have inbuilt explicit detection, or symmetry breaking, which will let them solve it efficiently).