It is well-known that CDCL-based SAT solvers are, in a precisely defined way, equivalent to resolution. Hence, formulas that are hard for resolution will also be hard for CDCL. One of the most promising approaches to extend the power of CDCL and avoid this limitation is Satisfiability-Driven Clause Learning (SDCL), which allows a CDCL-based SAT solver to simulate more powerful proof systems by learning appropriate redundant clauses. In this paper, we present a MaxSAT-based technique that allows SDCL to learn shorter, and hence better, redundant clauses. This technique is implemented and evaluated in the MapleSAT-SDCL solver.
Learning Shorter Redundant Clauses in SDCL Using MaxSAT