Long Proofs of (Seemingly) Simple Formulas
(2014) 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 In Lecture Notes in Computer Science 8561. p.121-137- Abstract
In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become... (More)
In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley 2011].
(Less)
- author
- Mikša, Mladen and Nordström, Jakob LU
- publishing date
- 2014
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Theory and Applications of Satisfiability Testing, SAT 2014 : 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings - 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings
- series title
- Lecture Notes in Computer Science
- volume
- 8561
- pages
- 17 pages
- publisher
- Springer
- conference name
- 17th International Conference on Theory and Applications of Satisfiability Testing, SAT 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
- conference location
- Vienna, Austria
- conference dates
- 2014-07-14 - 2014-07-17
- external identifiers
-
- scopus:84958552506
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783319092836
- DOI
- 10.1007/978-3-319-09284-3_10
- language
- English
- LU publication?
- no
- id
- 330ace3f-aa27-42de-a0d9-41cb46762463
- date added to LUP
- 2020-12-18 22:24:18
- date last changed
- 2024-01-03 01:20:50
@inproceedings{330ace3f-aa27-42de-a0d9-41cb46762463,
abstract = {{<p>In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley 2011].</p>}},
author = {{Mikša, Mladen and Nordström, Jakob}},
booktitle = {{Theory and Applications of Satisfiability Testing, SAT 2014 : 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings}},
isbn = {{9783319092836}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{121--137}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{Long Proofs of (Seemingly) Simple Formulas}},
url = {{http://dx.doi.org/10.1007/978-3-319-09284-3_10}},
doi = {{10.1007/978-3-319-09284-3_10}},
volume = {{8561}},
year = {{2014}},
}