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

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