On the complexity of resolution with bounded conjunctions

DOI10.1016/j.tcs.2004.04.004zbMath1056.03036OpenAlexW2074946288MaRDI QIDQ1885907

Nicola Galesi, Jochen Messner, Juan Luis Esteban

Publication date: 12 November 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.04.004

zbMATH Keywords

resolutioncomplexity of Proofs

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items (10)

A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games ⋮ Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ The depth of resolution proofs ⋮ On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution ⋮ The treewidth of proofs ⋮ The Complexity of Propositional Proofs ⋮ A Framework for Space Complexity in Algebraic Proof Systems ⋮ Resolution and the binary encoding of combinatorial principles ⋮ Total Space in Resolution

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A combinatorial characterization of treelike resolution space
• The intractability of resolution
• Some consequences of cryptographical conjectures for \(S_2^1\) and EF
• Space bounds for resolution
• Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
• Short resolution proofs for a sequence of tricky formulas
• A combinatorial characterization of resolution width
• On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
• On the weak pigeonhole principle
• The Efficiency of Resolution and Davis--Putnam Procedures
• Space Complexity in Propositional Calculus
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Size space tradeoffs for resolution
• Resolution lower bounds for the weak pigeonhole principle
• Hard examples for resolution
• Space bounds for a game on graphs
• The relative efficiency of propositional proof systems
• Lower bounds to the size of constant-depth propositional proofs
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• On Interpolation and Automatization for Frege Systems
• A new proof of the weak pigeonhole principle

This page was built for publication: On the complexity of resolution with bounded conjunctions