Space proof complexity for random 3-CNFs

DOI10.1016/J.IC.2017.06.003MaRDI QIDQ2013560zbMATHOpenAlexWikidataFDO

Authors Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, Paul Wollan

Publication date 8 August 2017

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.01613

zbMATH Keywords

resolutionproof complexityrandom CNFspolynomial calculustotal spacemonomial space

Mathematics Subject Classification ID

Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Complexity of proofs (03F20)

Abstract: We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $phi$ in $n$ variables requires, with high probability, $Omega(n)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $phi$ requires, with high probability, $Omega(n)$ clauses each of width $Omega(n)$ to be kept at the same time in memory. This gives a $Omega(n^2)$ lower bound for the total space needed in Resolution to refute $phi$. These results are best possible (up to a constant factor). The main technical innovation is a variant of Hall's Lemma. We show that in bipartite graphs $G$ with bipartition $(L,R)$ and left-degree at most 3, $L$ can be covered by certain families of disjoint paths, called VW-matchings, provided that $L$ expands in $R$ by a factor of $(2-epsilon)$, for $epsilon<1/23$.

Recommendations

• Space complexity of random formulae in resolution
• An Upper Bound on the Space Complexity of Random Formulae in Resolution
• Total space in resolution
• scientific article; zbMATH DE number 1775444
• From small space to small width in resolution

Cites work

• scientific article; zbMATH DE number 1256733 (Why is no real title available?)
• scientific article; zbMATH DE number 3029852 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A combinatorial characterization of resolution width
• A framework for space complexity in algebraic proof systems
• An exponential separation between the parity principle and the pigeonhole principle
• Many hard examples for resolution
• Narrow proofs may be spacious: separating space and width in resolution
• On Representatives of Subsets
• On sufficient conditions for unsatisfiability of random formulas
• Sharp thresholds of graph properties, and the $k$-sat problem
• Short proofs are narrow—resolution made simple
• Size space tradeoffs for resolution
• Space Complexity in Propositional Calculus
• Space bounds for resolution
• Space complexity of random formulae in resolution
• Space proof complexity for random 3-CNFs
• Total space in resolution
• Total space in resolution is at least width squared
• Towards an understanding of polynomial calculus: new separations and lower bounds (extended abstract)
• Tree matchings

Cited in

(9)

• An Upper Bound on the Space Complexity of Random Formulae in Resolution
• A framework for space complexity in algebraic proof systems
• Trade-offs between time and memory in a tighter model of CDCL SAT solvers
• Narrow proofs may be maximally long
• Total space in resolution
• Space Complexity in Polynomial Calculus
• Supercritical space-width trade-offs for resolution
• Space proof complexity for random 3-CNFs
• Space complexity of random formulae in resolution

This page was built for publication: Space proof complexity for random 3-CNFs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2013560)