Near optimal seperation of tree-like and general resolution

DOI10.1007/S00493-004-0036-5MaRDI QIDQ558312zbMATH OpenOpenAlexFDO

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

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

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

(37)

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

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)