Space complexity of random formulae in resolution

DOI10.1002/rsa.10089zbMath1048.03046OpenAlexW1974070050MaRDI 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 spacematching games on bipartite graphsspace complexity of refuting unsatisfiable random formulastreelike resolution refutations

Mathematics Subject Classification ID

Games involving graphs (91A43) Graph theory (including graph drawing) in computer science (68R10) Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items

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

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