Mutilated chessboard problem is exponentially hard for resolution

DOI10.1016/S0304-3975(03)00395-5zbMath1071.68028WikidataQ57532686 ScholiaQ57532686MaRDI QIDQ1884991

Michael Alekhnovich

Publication date: 27 October 2004

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

zbMATH Keywords

Lower boundsResolutionPropositional proof complexity

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Combinatorial aspects of packing and covering (05B40) Complexity of proofs (03F20)

Related Items (13)

Narrow Proofs May Be Maximally Long ⋮ A tetrachotomy of ontology-mediated queries with a covering axiom ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Satisfiability, branch-width and Tseitin tautologies ⋮ Special issue in memory of Misha Alekhnovich. Foreword ⋮ Simulating strong practical proof systems with extended resolution ⋮ Propositional proof systems based on maximum satisfiability ⋮ Preprocessing of propagation redundant clauses ⋮ Limitations of restricted branching in clause learning ⋮ Unnamed Item ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Resolution for Max-SAT ⋮ Preprocessing of propagation redundant clauses

Cites Work

• Short proofs for tricky formulas
• Resolution proofs of matching principles
• Short proofs are narrow—resolution made simple
• Many hard examples for resolution
• Resolution lower bounds for the weak pigeonhole principle
• Regular resolution lower bounds for the weak pigeonhole principle

This page was built for publication: Mutilated chessboard problem is exponentially hard for resolution