Conflict-Driven Clause Learning algorithms are well known from an engineerpoint of view. Thanks to Minisat, their designs are well understood, and mostof their implementations follow the same ideas, with essentially the samecomponents. Same heuristics, fast restarts, same learning mechanism.However, their efficiency has an important drawback: they are more and morelike complex systems and harder and harder to handle. Unfortunately, only afew works are focusing on understanding them rather than improving them. Inmost of the cases, their studies are often based on a generate and testpattern: An idea is added to an existing solver and if it improves itsefficiency the idea is published and kept. In this paper, we analyse``post-mortem'' the proofs given by one typical CDCL solver,Glucose. The originality of our approach is that we only consider it as aresolution proofs builder, and then we analyze some of the proofcharacteristics on a set of selected unsatisfiable instances, by shuffling each ofthem 200 times. We particularly focus on trying to characterize useless anduseful clauses in the proof as well as proofs shapes. We also show thatdespite their incredible efficiency, roughly 90% of the time spent in aCDCL is useless for producing the final proof.
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
