Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR13-097 | 25th June 2013 16:17

On Propositional QBF Expansions and Q-Resolution


Authors: Mikolas Janota, Joao Marques-Silva
Publication: 26th June 2013 09:34
Downloads: 1623


Over the years, proof systems for propositional satisfiability (SAT)
have been extensively studied. Recently, proof systems for
quantified Boolean formulas (QBFs) have also been gaining attention.
Q-resolution is a calculus enabling producing proofs from
DPLL-based QBF solvers. While DPLL has become a dominating technique
for SAT, QBF has been tackled by other complementary and competitive
approaches. One of these approaches is based on expanding variables
until the formula contains only one type of quantifier; upon which a
SAT solver is invoked. This approach motivates the theoretical
analysis carried out in this paper. We focus on a two phase proof system,
which expands the formula in the first phase and applies propositional
resolution in the second. Fragments of this proof system are defined and
compared to Q-resolution.

ISSN 1433-8092 | Imprint