On the automatizability of resolution and related propositional proof systems

Abstract

We analyse the possibility that a system that simulates Resolution is automatizable. We call this notion”weak automatizability”. We prove that Resolution is weakly automatizable if and only if Res(2) has feasible interpolation. In order to prove this theorem, we show that Res(2) has polynomial-size proofs of the reflection principle of Resolution (and of any Res(k)), which is a version of consistency. We also show that Resolution proofs of its own reflection principle require slightly subexponential size. This gives a better lower bound for the monotone interpolation of Res(2) and a better separation from Resolution as a byproduct. Finally, the techniques for proving these results give us a new complexity measure for Resolution that refines the width of Ben-Sasson and Wigderson. The new measure and techniques suggest a new algorithm to find Resolution refutations, and a way to obtain a large class of examples that have small Resolution refutations but require relatively large width. This answers a question of Alekhnovich and Razborov related to whether Resolution is automatizable in quasipolynomial-time.