Regular resolution effectively simulates resolution
Sam Buss, Emre Yolcu
TL;DR
The paper studies how to compare propositional proof systems beyond standard simulations by introducing effective simulation, which permits a size-aware translation between systems. It proves the central result that regular resolution and resolution are equivalent under effective simulation, via a height-parameterized transformation $f( Gamma,h)$ that introduces new variables $W[x,j]$ and equates them along levels, yielding a regular resolution refutation of $f( Gamma,h)$ from any resolution refutation of $ Gamma$ with size bound $O(h n s)$ and height bound $O(h n)$. The construction relies on a lowering technique to preserve regularity by ensuring decreasing level usage along all paths. The corollaries show that regular resolution cannot be closed under substitutions and that effective simulation transfers automatability properties between the systems, enabling black-box transfer of hardness results (e.g., automatic proof search) from regular resolution to resolution; this provides a framework to translate known automata-based hardness results into the standard resolution setting.
Abstract
Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an "effective simulation," which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution.