Near optimal seperation of tree-like and general resolution
From MaRDI portal
Publication:558312
DOI10.1007/s00493-004-0036-5zbMath1063.03043OpenAlexW2092984557MaRDI QIDQ558312
Russell Impagliazzo, Avi Wigderson, Eli Ben-Sasson
Publication date: 5 July 2005
Published in: Combinatorica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00493-004-0036-5
automated theorem provinggeneral resolution refutationsnear optimal seperationpolynomial run-timetree-like resolution refutations
Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items (26)
On the automatizability of resolution and related propositional proof systems ⋮ A note about \(k\)-DNF resolution ⋮ The state of SAT ⋮ A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games ⋮ Unnamed Item ⋮ On (simple) decision tree rank ⋮ Unnamed Item ⋮ Regular and General Resolution: An Improved Separation ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ Cliques enumeration and tree-like resolution proofs ⋮ The depth of resolution proofs ⋮ A characterization of tree-like resolution size ⋮ On semantic cutting planes with very small coefficients ⋮ The Complexity of Propositional Proofs ⋮ Reversible pebble games and the relation between tree-like and general resolution space ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ A Tutorial on Time and Space Bounds in Tree-Like Resolution ⋮ An Exponential Lower Bound for Width-Restricted Clause Learning ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search ⋮ Resolution over linear equations modulo two ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ Proofs and Certificates for Max-SAT ⋮ MaxSAT Resolution and Subcube Sums ⋮ A proof builder for Max-SAT
This page was built for publication: Near optimal seperation of tree-like and general resolution
