Having good algorithms to verify tautologies as efficiently as possible is of prime interest in different fields of computer science. In this paper we present an algorithm for finding Resolution refutations based on finding tree-like Res(k) refutations. The algorithm is based on the one of Beame and Pitassi cite{BP96} for tree-like Resolution, but it is provably more efficient. On the other hand our algorithm is also more efficient than Davis-Putnam and better in the sense of space usage than the one of Ben-Sasson and Wigderson cite{BSW01}. We also 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 slightly subexponential 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 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 cite{AR01b} related to whether Resolution is automatizable in quasipolynomial-time.
展开▼
