Space proof complexity for random 3-CNFs

DOI10.1016/J.IC.2017.06.003zbMATH Open1423.03242arXiv1503.01613OpenAlexW2963843567WikidataQ61732560 ScholiaQ61732560MaRDI QIDQ2013560FDOQ2013560

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)

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$.

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

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

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)

Cites Work

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

Cited In (9)

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