Hardness measures and resolution lower bounds
Computational Complexity
2014-02-18 v2 Logic in Computer Science
Abstract
Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this report we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. We also extend these measures to all clause-sets (possibly satisfiable).
Keywords
Cite
@article{arxiv.1310.7627,
title = {Hardness measures and resolution lower bounds},
author = {Olaf Beyersdorff and Oliver Kullmann},
journal= {arXiv preprint arXiv:1310.7627},
year = {2014}
}
Comments
43 pages, preliminary version (yet the application part is only sketched, with proofs missing)