Conference Paper/Proceeding/Abstract 1130 views 233 downloads
Unified Characterisations of Resolution Hardness Measures
Olaf Beyersdorff,
Oliver Kullmann 
Theory and Applications of Satisfiability Testing – SAT 2014, Volume: 8561
Swansea University Author:
Oliver Kullmann
-
PDF | Author's Original
Download (284.21KB)
DOI (Published version): 10.1007/978-3-319-09284-3_13
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 paper we aim at a unified view of a number of hardness measur...
| Published in: | Theory and Applications of Satisfiability Testing – SAT 2014 |
|---|---|
| Published: |
International Conference on Theory and Applications of Satisfiability Testing: Springer
2014
|
| Online Access: |
http://www.cs.swan.ac.uk/~csoliver/papers.html#HARD2014 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa18004 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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 paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. Our main contribution is a unified game-theoretic characterisation of these measures. As consequences we obtain new relations between the different hardness measures. In particular, we prove a generalised version of Atserias and Dalmau's result on the relation between resolution width and space. |
|---|---|
| Keywords: |
SAT, proof complexity, games, resolution calculus, hardness measures |
| College: |
Faculty of Science and Engineering |
| End Page: |
187 |