QBF 2014 WORKSHOP REPORT: PAPERS WITH ABSTRACTS

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.

ABSTRACT. Resolution is a fundamental part of modern search and learning based QBF solvers, and the extraction of Skolem-function models and Herbrand-function countermodels from QBF resolution proofs is a key enabler for various applications. Although long-distance resolution (LQ-resolution) came into existence a decade ago, its superiority to short-distance resolution (Q-resolution) was not recognized until recently. It remains open whether there exists a polynomial time algorithm for model and countermodel extraction from LQ-resolution proofs, although an efficient algorithm does exist for the Q-resolution counterparts. This paper settles this open problem affirmatively by constructing a linear-time extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates.