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 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].
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Bipartite Graph
- Conjunctive Normal Form
- Cardinality Constraint
- Random Instance
- Conjunctive Normal Form Formula
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM Journal on Computing 31(4), 1184–1211 (2002), preliminary version appeared in STOC 2000
Alekhnovich, M., Razborov, A.A.: Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics 242, 18–35 (2003), http://people.cs.uchicago.edu/razborov/files/misha.pdf , Preliminary version appeared in FOCS 2001
Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research 40, 353–373 (2011), preliminary version appeared in SAT 2009
Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203–208 (July 1997)
Beck, C., Impagliazzo, R.: Strong ETH holds for regular resolution. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 487–494 (May 2013)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow—resolution made simple. Journal of the ACM 48 48(2), 149–169 (2001), preliminary version appeared in STOC 1999
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010), system description
Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285–301. Springer, Heidelberg (2014)
Blake, A.: Canonical Expressions in Boolean Algebra. Ph.D. thesis, University of Chicago (1937)
Bondy, J.A., Murty, U.S.R.: Graph Theory. Springer (2008)
Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the ACM 35(4), 759–768 (1988)
Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC 1996), pp. 174–183 (May 1996)
Cook, W., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics 18(1), 25–38 (1987)
The Glucose SAT solver, http://www.labri.fr/perso/lsimon/glucose/ .
Haken, A.: The intractability of resolution. Theoretical Computer Science 39(2-3), 297–308 (1985)
Hoory, S., Linial, N., Wigderson, A.: Expander graphs and their applications. Bulletin of the American Mathematical Society 43(4), 439–561 (2006)
Impagliazzo, R., Pudlák, P., Sgall, J.: Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity 8(2), 127–144 (1999)
Lingeling and Plingeling, http://fmv.jku.at/lingeling/
March, http://www.st.ewi.tudelft.nl/~marijn/sat/march_dl.php
Markström, K.: Locality and hard SAT-instances. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4), 221–227 (2006)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999), preliminary version appeared in ICCAD 1996
The MiniSat page, http://minisat.se/
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530–535 (June 2001)
Nordström, J.: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science 9, 15:1–15:63 (2013)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence 175, 512–525 (2011), preliminary version appeared in CP 2009
Spence, I.: sgen1: A generator of small but difficult satisfiability benchmarks. Journal of Experimental Algorithmics 15, 1.2:1.1–1.2:1.15 (2010)
Urquhart, A.: Hard examples for resolution. Journal of the ACM 34(1), 209–219 (1987)
Van Gelder, A., Spence, I.: Zero-one designs produce small hard SAT instances. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 388–397. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Mikša, M., Nordström, J. (2014). Long Proofs of (Seemingly) Simple Formulas. In: Sinz, C., Egly, U. (eds) Theory and Applications of Satisfiability Testing – SAT 2014. SAT 2014. Lecture Notes in Computer Science, vol 8561. Springer, Cham. https://doi.org/10.1007/978-3-319-09284-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-09284-3_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09283-6
Online ISBN: 978-3-319-09284-3
eBook Packages: Computer ScienceComputer Science (R0)