Resolution Is Not Automatizable Unless W[P] Is Tractable

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. Key words. Proof complexity, resolution, automatizability AMS subject classifications. 03F20, 03D15

• Type: Journal
• Year: 2008
• Where: SIAMCOMP
• Authors: Michael Alekhnovich, Alexander A. Razborov
• Keywords: One-sided Error, Parameterized Problems, SIAMCOMP 2008, Tree-like Resolution