ALCOMFT-TR-03-104

Albert Atserias and Mar\'\ia Luisa Bonet
On the Automatizability of Resolution and Related Propositional Proof Systems
Barcelona. Work package 4. November 2003.

Abstract: A propositional proof system is automatizable if there is an algorithm that, given a tautology, produces a proof in time polynomial in the size of its smallest proof. This notion can be weakened if we allow the algorithm to produce a proof in a stronger system within the same time bound. This new notion is called weak automatizability. Among other characterizations, we prove that a system is weakly automatizable exactly when a weak form of the satisfiability problem is solvable in polynomial time. After studying the robustness of the definition, we prove the equivalence between: (i) Resolution is weakly automatizable, (ii) Res(k) is weakly automatizable and (iii) Res(k) has feasible interpolation, when k>1. In order to prove this result, we show that Res(2) has polynomial-size proofs of the reflection principle of Resolution, which is a version of consistency. We also show that Res(k), for every k>1, proves its consistency in polynomial size, while Resolution does not. In fact, we show that Resolution proofs of its own consistency require almost exponential size. This gives a better lower bound for the monotone interpolation of Res(2) and a separation from Resolution as a byproduct. Our techniques also 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 related to whether Resolution is automatizable in quasipolynomial-time.

Postscript file: ALCOMFT-TR-03-104.ps.gz (94 kb).