Publications

Measuring the Hardness of SAT Instances

Publication Type:

Conference Paper

Authors:

Carlos Ansótegui; María Luisa Bonet; Jordi Levy; Felip Manyà

Source:

Proc. of the 23th AAAI Conference on Artificial Intelligence, AAAI-08, AAAI Press, Chicago, USA, p.222-228 (2008)

Keywords:

SAT

Abstract:

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.

Projects: 
MULOG 2
»