Resolution Is Not Automatizable Unless W[P] Is Tractable
- 1 January 2008
- journal article
- Published by Society for Industrial & Applied Mathematics (SIAM) in SIAM Journal on Computing
- Vol. 38 (4), 1347-1363
- https://doi.org/10.1137/06066850x
Abstract
We show that neither Resolution nor tree-like Resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error.Keywords
This publication has 12 references indexed in Scilit:
- Non-Automatizability of Bounded-Depth Frege Proofscomputational complexity, 2004
- On the hardness of approximating label-coverInformation Processing Letters, 2004
- On the automatizability of resolution and related propositional proof systemsInformation and Computation, 2004
- Pseudorandom Generators in Propositional Proof ComplexitySIAM Journal on Computing, 2004
- Minimum propositional proof length is NP-hard to linearly approximateThe Journal of Symbolic Logic, 2001
- Short proofs are narrow—resolution made simpleJournal of the ACM, 2001
- On Interpolation and Automatization for Frege SystemsSIAM Journal on Computing, 2000
- Some Consequences of Cryptographical Conjectures forS12and EFInformation and Computation, 1998
- On the efficiency of polynomial time approximation schemesInformation Processing Letters, 1997
- The relative efficiency of propositional proof systemsThe Journal of Symbolic Logic, 1979