Gustav Sennton: On conflict driven clause learning — a comparison between theory and practice

The boolean satisifiability (SAT) problem is the canonical NP-complete problem and every other NP-complete problem can be reduced to the SAT problem. Since the SAT problem is NP-complete large instances of this problem should be difficult to solve. However, in practice conflict driven clause learning (CDCL) solvers solve large real-world instances of the SAT problem efficiently. Recently, a theoretical upper bound was shown for the efficiency of a certain version of such solvers, but that solver version differs in several ways from solvers used in practice. In this project experiments are used to investigate whether such a solver is realistic and whether its theoretical bound holds for solvers used in practice. These experiments compare all the components that differ between the theoretical solver version and a real implementation of a solver. The experimental results show that the running times of the two solvers often differ substantially. At the same time, the theoretical running time bound seems to hold for the practical solvers. I.e. the running time of practical solvers seems to grow polynomially for formulas for which the theoretically predicted running time is polynomial. However, some of the formulas used should be tested further since not enough data points have been collected for these formulas. For these formulas we cannot rule out high asymptotical running times of real-world solvers.