On the Structure of Resolution Refutations Generated by Modern CDCL Solvers

Sammanfattning: Modern solvers for the Boolean satisfiability problem (SAT) that are based on conflict-driven clause learning (CDCL) are known to be able to solve some instances significantly more efficiently than older kinds of solvers such as ones using the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. In addition to solving instances that can be satisfied, SAT solvers will implicitly generate proofs of unsatisfiability for formulae that are unsatisfiable. Theoretical models of CDCL based solvers are known to have access to more powerful forms of reasoning compared to their DPLL counterparts and as a result, are able to generate proofs that are significantly shorter for certain kinds of formulae. Additionally, certain characteristics are expected when representing these proofs as graphs, such as them not being strictly tree-like in shape. It is however less well known if these theoretical justifications are indeed the reason CDCL solvers are so successful in practice. This project attempts to answer this question by modifying a modern CDCL solver to output the proof and comparing these proofs to what theoretical results would predict. Firstly, the results indicate that CDCL solvers generate significantly shorter proofs for all kinds of formulae that were investigated as compared to a DPLL solver. Furthermore, it appears that this is in large part due to the proof not being tree-like. Secondly, utilizing restarts was found to make for significantly shorter proofs for most families of formulae but the effect was the opposite for formulas representing the relativized pigeonhole principle. The explanation for this is seemingly not clear. Lastly, it appears that the Tseitin formulae used do not exhibit timespace trade-offs but instead simply require a large amount of space. This is indicated by the run time being significantly greater if clause erasure if more aggressive but the refutation being similar in both length and number of learned clauses. To summarize, it has been found that modern CDCL solvers appear to result in significantly different proofs that largely mirror what one would expect. However, the results are unclear on the role of restarts and how their effect on the proof best can be explained.