Measuring the Hardness of SAT Instances
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 treelike 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.
Cite
Text
Ansótegui et al. "Measuring the Hardness of SAT Instances." AAAI Conference on Artificial Intelligence, 2008.Markdown
[Ansótegui et al. "Measuring the Hardness of SAT Instances." AAAI Conference on Artificial Intelligence, 2008.](https://mlanthology.org/aaai/2008/ansotegui2008aaai-measuring/)BibTeX
@inproceedings{ansotegui2008aaai-measuring,
title = {{Measuring the Hardness of SAT Instances}},
author = {Ansótegui, Carlos and Bonet, Maria Luisa and Levy, Jordi and Manyà, Felip},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2008},
pages = {222-228},
url = {https://mlanthology.org/aaai/2008/ansotegui2008aaai-measuring/}
}