Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes
- 27 June 2022
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 69 (3), 1-32
- https://doi.org/10.1145/3486680
Abstract
The random k-SAT model is one of the most important and well-studied distributions over k-SAT instances. It is closely connected to statistical physics and is a benchmark for satisfiability algorithms. We show that when \( k = \Theta (\log n) \), any Cutting Planes refutation for random k-SAT requires exponential length in the regime where the number of clauses guarantees that the formula is unsatisfiable with high probability.
Keywords
Funding Information
- National Science Foundation (DMS-1638352)
- Natural Sciences and Engineering Research Council
This publication has 38 references indexed in Scilit:
- PseudorandomnessFoundations and Trends® in Theoretical Computer Science, 2012
- An Exponential Lower Bound for the Size of Monotone Real CircuitsJournal of Computer and System Sciences, 1999
- Separation of the Monotone NC HierarchyCombinatorica, 1999
- Interpolation by a GameMathematical Logic Quarterly, 1998
- Lower bounds for resolution and cutting plane proofs and monotone computationsThe Journal of Symbolic Logic, 1997
- Lower bounds for cutting planes proofs with small coefficientsThe Journal of Symbolic Logic, 1997
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmeticThe Journal of Symbolic Logic, 1997
- Unprovability of lower bounds on circuit size in certain fragments of bounded arithmeticIzvestiya: Mathematics, 1995
- Many hard examples for resolutionJournal of the ACM, 1988
- Outline of an algorithm for integer solutions to linear programsBulletin of the American Mathematical Society, 1958