Hard examples for resolution
- 1 January 1987
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 34 (1) , 209-219
- https://doi.org/10.1145/7531.8928
Abstract
Exponential lower bounds are proved for the length-of-resolution refutations of sets of disjunctions constructed from expander graphs, using the method of Tseitin. Since these sets of clauses encode biconditionals, they have short (polynomial-length) refutations in a standard axiomatic formulation of propositional calculus.Keywords
This publication has 6 references indexed in Scilit:
- The intractability of resolutionTheoretical Computer Science, 1985
- A simplified proof that regular resolution is exponentialInformation Processing Letters, 1980
- The relative efficiency of propositional proof systemsThe Journal of Symbolic Logic, 1979
- On Resolution with Clauses of Bounded SizeSIAM Journal on Computing, 1977
- On the complexity of regular resolution and the Davis-Putnam procedureTheoretical Computer Science, 1977
- A short proof of the pigeon hole principle using extended resolutionACM SIGACT News, 1976