TitleMeasuring the Hardness of SAT Instances
Publication TypeConference Paper
Year of Publication2008
AuthorsAnsótegui C, Bonet MLuisa, Levy J, Manyà F
EditorFox D, Gomes C
Conference NameProc. of the 23th AAAI Conference on Artificial Intelligence, AAAI-08
PublisherAAAI Press
Conference LocationChicago, USA

The search of a precise measure of what hardness of SAT instances means for state-of-the-art solvers is a relevant research question. Among others, the space complexity of tree-like resolution (also called hardness), the minimal size of strong backdoors and of cycle-cutsets, and the treewidth can be used for this purpose. We propose the use of the tree-like space complexity as a solid candidate to be the best measure for solvers based on DPLL. To support this thesis we provide a comparison with the other mentioned measures. We also conduct an experimental investigation to show how the proposed measure characterizes the hardness of random and industrial instances.