Space complexity of random formulae in resolution

DOI10.1002/rsa.10089zbMath1048.03046MaRDI QIDQ4417005

Nicola Galesi, Eli Ben-Sasson

Publication date: 6 August 2003

Published in: Random Structures & Algorithms (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/rsa.10089

zbMATH Keywords

lower bounds on the clause space; matching games on bipartite graphs; space complexity of refuting unsatisfiable random formulas; treelike resolution refutations

Mathematics Subject Classification ID

91A43: Games involving graphs

68R10: Graph theory (including graph drawing) in computer science

05C70: Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.)

03B35: Mechanization of proofs and logical operations

03D15: Complexity of computation (including implicit computational complexity)

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03F20: Complexity of proofs

Related Items

An Upper Bound on the Space Complexity of Random Formulae in Resolution, Cumulative Space in Black-White Pebbling and Resolution, An Introduction to Lower Bounds on Resolution Proof Systems, Supercritical Space-Width Trade-offs for Resolution, From Small Space to Small Width in Resolution, Narrow Proofs May Be Maximally Long, LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE, The impact of heterogeneity and geometry on the proof complexity of random satisfiability, A simplified way of proving trade-off results for resolution, On semantic cutting planes with very small coefficients, On the complexity of resolution with bounded conjunctions, Space proof complexity for random 3-CNFs, A combinatorial characterization of resolution width, A Framework for Space Complexity in Algebraic Proof Systems, Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, Total Space in Resolution, Space Complexity in Polynomial Calculus, On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution

Cites Work

• Short proofs are narrow—resolution made simple
• Setting 2 variables at a time yields a new lower bound for random 3-SAT (extended abstract)
• Space complexity in propositional calculus
• Unnamed Item
• Unnamed Item