Relating proof complexity measures and practical hardness of SAT
(2012) 18th International Conference on Principles and Practice of Constraint Programming, CP 2012 In Lecture Notes in Computer Science 7514. p.316-331- Abstract
Boolean satisfiability (SAT) solvers have improved enormously in performance over the last 10-15 years and are today an indispensable tool for solving a wide range of computational problems. However, our understanding of what makes SAT instances hard or easy in practice is still quite limited. A recent line of research in proof complexity has studied theoretical complexity measures such as length, width, and space in resolution, which is a proof system closely related to state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Although it seems like a natural question whether these complexity measures could be relevant for understanding the practical hardness of SAT instances, to date there has been very limited research on... (More)
Boolean satisfiability (SAT) solvers have improved enormously in performance over the last 10-15 years and are today an indispensable tool for solving a wide range of computational problems. However, our understanding of what makes SAT instances hard or easy in practice is still quite limited. A recent line of research in proof complexity has studied theoretical complexity measures such as length, width, and space in resolution, which is a proof system closely related to state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Although it seems like a natural question whether these complexity measures could be relevant for understanding the practical hardness of SAT instances, to date there has been very limited research on such possible connections. This paper sets out on a systematic study of the interconnections between theoretical complexity and practical SAT solver performance. Our main focus is on space complexity in resolution, and we report results from extensive experiments aimed at understanding to what extent this measure is correlated with hardness in practice. Our conclusion from the empirical data is that the resolution space complexity of a formula would seem to be a more fine-grained indicator of whether the formula is hard or easy than the length or width needed in a resolution proof. On the theory side, we prove a separation of general and tree-like resolution space, where the latter has been proposed before as a measure of practical hardness, and also show connections between resolution space and backdoor sets.
(Less)
- author
- Järvisalo, Matti ; Matsliah, Arie ; Nordström, Jakob LU and Živný, Stanislav
- publishing date
- 2012
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Principles and Practice of Constraint Programming : 18th International Conference, CP 2012, Proceedings - 18th International Conference, CP 2012, Proceedings
- series title
- Lecture Notes in Computer Science
- volume
- 7514
- pages
- 16 pages
- publisher
- Springer
- conference name
- 18th International Conference on Principles and Practice of Constraint Programming, CP 2012
- conference location
- Quebec City, QC, Canada
- conference dates
- 2012-10-08 - 2012-10-12
- external identifiers
-
- scopus:84868269243
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9783642335570
- DOI
- 10.1007/978-3-642-33558-7_25
- language
- English
- LU publication?
- no
- id
- e963a526-e865-4496-b714-8908a5d32342
- date added to LUP
- 2020-12-18 22:26:32
- date last changed
- 2025-04-04 14:26:14
@inproceedings{e963a526-e865-4496-b714-8908a5d32342,
abstract = {{<p>Boolean satisfiability (SAT) solvers have improved enormously in performance over the last 10-15 years and are today an indispensable tool for solving a wide range of computational problems. However, our understanding of what makes SAT instances hard or easy in practice is still quite limited. A recent line of research in proof complexity has studied theoretical complexity measures such as length, width, and space in resolution, which is a proof system closely related to state-of-the-art conflict-driven clause learning (CDCL) SAT solvers. Although it seems like a natural question whether these complexity measures could be relevant for understanding the practical hardness of SAT instances, to date there has been very limited research on such possible connections. This paper sets out on a systematic study of the interconnections between theoretical complexity and practical SAT solver performance. Our main focus is on space complexity in resolution, and we report results from extensive experiments aimed at understanding to what extent this measure is correlated with hardness in practice. Our conclusion from the empirical data is that the resolution space complexity of a formula would seem to be a more fine-grained indicator of whether the formula is hard or easy than the length or width needed in a resolution proof. On the theory side, we prove a separation of general and tree-like resolution space, where the latter has been proposed before as a measure of practical hardness, and also show connections between resolution space and backdoor sets.</p>}},
author = {{Järvisalo, Matti and Matsliah, Arie and Nordström, Jakob and Živný, Stanislav}},
booktitle = {{Principles and Practice of Constraint Programming : 18th International Conference, CP 2012, Proceedings}},
isbn = {{9783642335570}},
issn = {{1611-3349}},
language = {{eng}},
pages = {{316--331}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{Relating proof complexity measures and practical hardness of SAT}},
url = {{http://dx.doi.org/10.1007/978-3-642-33558-7_25}},
doi = {{10.1007/978-3-642-33558-7_25}},
volume = {{7514}},
year = {{2012}},
}