On the Relation between Resolution Calculi for QBFs and First-order Formulas

ABSTRACT. Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations from QBFs to first-order formulas exist. We analyze the effect of such a translation on the complexity of resolution proofs. More precisely, we show that there are classes $(\Phi_i)_{i\geq 1}$ of QBFs where any Q-resolution refutation of $\Phi_i$ has length super-polynomial in $i$, but the translated version of $\Phi_i$ possesses a short resolution refutation. Moreover we discuss that first-order predicate logic can be used to succinctly represent refutations of QBFs obtained in different QBF calculi.