Q-resolution and its variations provide the underlying proof
systems for the DPLL-based QBF solvers. While (long-distance) Q-resolution
models a conflict driven clause learning (CDCL) QBF solver, it is not
known whether the inverse is also true. This paper provides a negative
answer to this question. This contrasts with SAT solving, ... more >>>

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Jussila et al. '07 who ... more >>>

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important
QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular
lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ... more >>>

Several calculi for quantified Boolean formulas (QBFs) exist, but
relations between them are not yet fully understood.
This paper defines a novel calculus, which is resolution-based and
enables unification of the principal existing resolution-based QBF
calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based
calculus ... more >>>

Propositional Satisfiability (SAT) solvers are routinely used for
solving many function problems.

A natural question that has seldom been addressed is: what is the
best worst-case number of calls to a SAT solver for solving some
target function problem?

This paper develops tighter upper bounds on the query complexity of
more >>>

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 ... more >>>