Near optimal seperation of tree-like and general resolution

DOI10.1007/S00493-004-0036-5MaRDI QIDQ558312zbMATHOpenAlexFDO

Authors Eli Ben-Sasson, Russell Impagliazzo, A. Wigderson

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

zbMATH Keywords

automated theorem provinggeneral resolution refutationsnear optimal seperationpolynomial run-timetree-like resolution refutations

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• A characterization of tree-like resolution size
• A near-optimal separation of regular and general resolution
• A lower bound for tree resolution
• Separation algorithm for tree partitioning inequalities
• A complexity gap for tree resolution
• Optimal partition trees
• Optimal partition trees
• Tree approximation and optimal encoding
• Optimal multiway generalized split trees
• Treewidth reduction for constrained separation and bipartization problems

Cited in

(31)

• Resolution over linear equations modulo two
• Typical case complexity of satisfiability algorithms and the threshold phenomenon
• The depth of resolution proofs
• The state of SAT
• A proof builder for Max-SAT
• Reversible pebble games and the relation between tree-like and general resolution space
• Short proofs are narrow -- resolution made simple
• Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT
• MaxSAT Resolution and Subcube Sums
• A characterization of tree-like resolution size
• Space characterizations of complexity measures and size-space trade-offs in propositional proof systems
• The complexity of resolution refinements
• Finding a tree structure in a resolution proof is NP-complete
• An Exponential Lower Bound for Width-Restricted Clause Learning
• Cliques enumeration and tree-like resolution proofs
• Stabbing planes
• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• On the automatizability of resolution and related propositional proof systems
• On the relative complexity of resolution refinements and cutting planes proof systems
• The Complexity of Propositional Proofs
• Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
• On structures of regular standard contradictions in propositional logic
• Proofs and Certificates for Max-SAT
• A tutorial on time and space bounds in tree-like resolution
• A note about \(k\)-DNF resolution
• On semantic cutting planes with very small coefficients
• A near-optimal separation of regular and general resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• On (simple) decision tree rank
• scientific article; zbMATH DE number 7350778 (Why is no real title available?)
• Regular and General Resolution: An Improved Separation

This page was built for publication: Near optimal seperation of tree-like and general resolution

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