On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution

DOI10.1007/978-3-642-22006-7_54zbMath1334.03057OpenAlexW2125291897MaRDI QIDQ3012839

Jakob Nordström, Alexander A. Razborov

Publication date: 6 July 2011

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22006-7_54

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Cites Work

• Unnamed Item
• Unnamed Item
• Exponential separation between Res(\(k\)) and Res(\(k+1\)) for \(k \leqslant \varepsilon\log n\)
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
• On the automatizability of resolution and related propositional proof systems
• On the complexity of resolution with bounded conjunctions
• Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution
• On the weak pigeonhole principle
• Space Complexity in Propositional Calculus
• Many hard examples for resolution
• Lower bounds for k-DNF resolution on random 3-CNFs
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• Narrow Proofs May Be Spacious:Separating Space and Width in Resolution