@inproceedings{JarvisaloMNZ:CP2012,
 author = {Matti J\"arvisalo and Arie Matliah and 
	Jakob Nordstr\"om and Stanislav \v{Z}ivn\'y\},
 title = {Relating Proof Complexity Measures and Practical Hardness of {SAT}},
 booktitle = {Proceedings of the 18th International Conference on 
	  Principles and Practice of Constraint Programming (CP 2012)},
 editor = {Michela Milano},
 series = {Lecture Notes in Computer Science},
 volume = {7514},
 pages = {316--331},
 year = {2012},
}

Abstract:

Boolean satisfiability (SAT) solvers have improved enormously in performance
over the last 10-15 years and are today an indispensable tool for solving
a wide range of computational problems. However, our understanding of what
makes SAT instances hard or easy in practice is still quite limited. A recent line
of research in proof complexity has studied theoretical complexity measures such
as length, width, and space in resolution, which is a proof system closely related
to state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Although
it seems like a natural question whether these complexity measures could be relevant
for understanding the practical hardness of SAT instances, to date there has
been very limited research on such possible connections. This paper sets out on
a systematic study of the interconnections between theoretical complexity and
practical SAT solver performance. Our main focus is on space complexity in resolution,
and we report results from extensive experiments aimed at understanding
to what extent this measure is correlated with hardness in practice. Our conclusion
from the empirical data is that the resolution space complexity of a formula
would seem to be a more fine-grained indicator of whether the formula is hard
or easy than the length or width needed in a resolution proof. On the theory side,
we prove a separation of general and tree-like resolution space, where the latter
has been proposed before as a measure of practical hardness, and also show
connections between resolution space and backdoor sets.