=Paper=
{{Paper
|id=Vol-2046/kovasznai
|storemode=property
|title=What is the state-of-the-art in DQBF solving?
|pdfUrl=https://ceur-ws.org/Vol-2046/kovasznai.pdf
|volume=Vol-2046
|authors=Gergely Kovásznai
}}
==What is the state-of-the-art in DQBF solving?==
https://ceur-ws.org/Vol-2046/kovasznai.pdf
What is the State-of-the-Art in DQBF solving?∗
Gergely Kovásznai
kovasznai.gergely@uni-eszterhazy.hu
IoT Research Institute
Eszterházy Károly University
Eger, Hungary
Abstract
Dependency Quantified Boolean Formulas (DQBF) are obtained by
adding Henkin quantifiers to Boolean formulas and have seen grow-
ing interest in the last years. In contrast to QBF, problem descrip-
tions in DQBF can possibly be exponentially more succinct. An the
other hand, while QBF is PSpace-complete, DQBF was shown to be
NExpTime-complete.
Many practical problems are known to be NExpTime-complete and,
hence, can be reduced to DQBF, e.g., partial information non-
cooperative games, certain bit-vector logics and partial equivalence
checking problems.
In this paper, I give a detailed survey on solving approaches for DQBF
in a chronological order, as well as preprocessing and inprocessing tech-
niques, and further advances in DQBF solving.
1 Introduction
With steadily increasing success of decision procedures for propositional formulas (SAT) and Quantified Boolean
Formulas (QBF), also interest in Dependency Quantified Boolean Formulas (DQBF) has grown during the last
years. DQBF has first been described in [PR79] and comprises the set of propositional formulas which are
obtained by adding Henkin quantifiers [Hen61], also called branching quantifiers, to Boolean logic. In contrast
to QBF, the dependencies of a variable in DQBF are explicitly specified instead of being implicitly defined by
the order of the quantifier prefix. This enables us to also use partial variable orders as part of a formula instead
of only allowing total ones.
As a result, problem descriptions in DQBF can possibly be exponentially more succinct. While QBF is
PSpace-complete [Pap94], DQBF was shown to be NExpTime-complete [PRA01, PR79]. Aside from DQBF,
many practical problems are known to be NExpTime-complete. This includes, e.g., partial information non-
cooperative games [PRA01] or certain bit-vector logics [KFB12, WHdM10, KFB15] used in the context of Satisfi-
ability Modulo Theories (SMT). Although quantifier-free bit-vector logics (QF_BV) are the essential ingredient
for hardware verification, and practically efficient direct solving approaches for QF_BV exist as well as indirect
ones that reduce QF_BV to other targets logics such as EPR [KFB13] or to model checking problems [FKB13],
∗ The research was supported by the grant EFOP-3.6.1-16-2016-00001 “Complex improvement of research capacities and services
at Eszterhazy Karoly University”.
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: E. Vatai (ed.): Proceedings of the 11th Joint Conference on Mathematics and Computer Science, Eger, Hungary, 20th – 22nd of
May, 2016, published at http://ceur-ws.org
185
DQBF has not succeeded to be a target logic for QF_BV so far. More recently, [GRS+ 13a, GRS+ 13b] showed
that partial equivalence checking (PEC) problems can be naturally encoded as DQBFs. Currently, solving PEC
problems seems to be the “killer application” for DQBF, as we will discuss in Section 4.
For DQBF, only a few direct solving approaches exist. In Section 3, we will introduce, chronologically, the
first one called DQDPLL [FKB12], which was followed by no publicly available implementation. In Section 5.1,
another solving approach called bounded unsatisfiability [FT14] will be introduced, which can solve unsatisfiable
DQBFs very efficiently, but cannot deal with satisfiable instances in practice. In Sections 5.2 and 5.3, we
will introduce two concrete, general-purpose DQBF solvers iDQ [FKBV14] and HQS [GWR+ 15], respectively.
While iDQ is publicly available, HQS was reported to be more efficient in practice, but, to the best of our
knowledge, is not yet publicly available. We will dedicate Section 6 to the topic of DQBF preprocessing. In
Section 7, we will summarize the most recent advances in DQBF solving.
2 Preliminaries
Let V be a set of Boolean variables. A positive literal is a Boolean variable x ∈ V , a negative literal is its
negation x. For a given literal l, we write var(l) to reference its corresponding variable. A clause is a disjunction
of literals. A Boolean formula is in Conjunctive Normal Form (CNF), if it is a conjunction of clauses.
A Quantified Boolean Formula (QBF) is defined as
Q1 x1 . . . Qn xn . φ (1)
where Qi ∈ {∀, ∃} are quantifiers, xi ∈ V are distinct variables, and φ is a Boolean formula in CNF over the
variables x1 , . . . , xn . We call Q1 x1 . . . Qn xn the quantifier prefix, and φ the matrix.
A Dependency Quantified Boolean Formula (DQBF) is the generalization of a QBF as follows. A DQBF is
defined as
∀u1 . . . ∀um ∃e1 (u1,1 , . . . , u1,k1 ) . . . ∃en (un,1 , . . . , un,kn ) . φ (2)
where φ is a Boolean formula in CNF over the variables u1 , . . . , um , e1 , . . . , en . The formalism ei (ui,1 , . . . , ui,ki )
means that the existential variable ei depends only on the universal variables ui,1 , . . . , ui,ki . We use Dei :=
{ui,1 , . . . , ui,ki } to denote ei ’s dependency set. Sometimes when we do not need to enumerate the exact depen-
dencies in advance, we will write (2) as
∀u1 . . . ∀um ∃e1 (De1 ) . . . ∃en (Den ) . φ (3)
Furthermore, let us extend the notion of dependency to literals, defining Dl := Dvar(l) for any literal l.
Note that in DQBF the dependencies of existential variables are always explicitly given, in contrast to QBF
where an existential variable depends on all the universal variables to the left in the quantifier prefix. Thus, the
QBF (1) can be considered as a special case of DQBF, where for all Qi = ∃ it holds that Dxi = {xj | 1 ≤ j <
i, Qj = ∀}. While in QBF the dependencies of the existential variables induce linear ordering, in DQBF this
is not always the case.
A truth assignment is a (partial) mapping α : V 7→ {0, 1} from the variables of a formula to truth values.
Sometimes we will denote an assignment as α = {x1 /v1 , . . . , xk /vk } where all xi ∈ V and vi ∈ {0, 1}. Given a
formula φ, the term φ[α] denotes the formula resulted by replacing all the variables xi in φ with α(xi ).
A Boolean formula φ is satisfiable if and only if there exists an assignment α such that φ[α] is evaluated to 1.
We then call α a model of φ. In DQBF (as well as in QBF), a model cannot be expressed by a single assignment.
Instead, we use Skolem functions to represent solutions of a formula. A Skolem function fe : {1, 0}|De | 7→ {1, 0}
describes the evaluation of an existential variable e under a given assignment to its dependencies. Let φsk denote
the formula obtained from φ by replacing all existential variables e by their Skolem function fe . The DQBF (3)
is satisfiable if and only if there exist Skolem functions fe1 , . . . , fen such that φsk is satisfied by all possible
assignments to the universal variables.
Effectively Propositional Logic (EPR), known as the Bernays-Schönfinkel class, is a NExpTime-complete
fragment of first-order logic [Lew80]. It consists of the first-order formulas in prenex form that contain no
function symbol of arity greater than 0, and no existential quantifier within the scope of a universal quantifier.
After Skolemization, existential variables turn into constants (i.e., function symbols of arity 0). Consequently,
an EPR atom can be defined as an expression of the form p(t1 , . . . , tn ) where p is a predicate symbol of arity
n, and each ti is either a universal variable or a constant. EPR literals and clauses are defined similarly as in
Boolean logic, by replacing the word “Boolean variable” with “atom”. An instance of an EPR clause C is a clause
C[α] for some assignment α to the universal variables in C.
186
3 First Solving Approach – DQDPLL
The first direct solving approach for DQBF is called DQDPLL [FKB12], which is the adaptation of
QDPLL [CGS98] being one of the most successful solving approaches for QBF. The paper shows how to adapt
the building blocks of the DPLL-style approach, one by one, like unit propagation, clause learning, backtracking,
universal reduction, pure literal reduction, watched literal schemes, etc.
The fundamental difference between DQDPLL and QDPLL is how decisions are saved in the decision stack:
while QDPLL only has to save the decision literal le where e is an existential variable, DQDPLL additionally
has to save a so-called Skolem clause linked with the current branch of the search tree represented by a partial
assignment α. The Skolem clause that represents this decision le according to the assignments to the universal
variables on which e depends:
_ u, if α(u) = 0
Csk := le ∨ lu , where lu = u, if α(u) = 1
u∈De
0, if α(u) = undef
Unit propagation can be implemented in the same way as done for QDPLL, with the extension of adding a
Skolem clause as already described.
Clause learning also works as in QDPLL, however we need to differentiate between temporary learned clauses
and permanent learned clauses. Any learned clause created by resolution with at least one Skolem clause or with
a temporary learned clause is only valid as long as all clauses participating in the resolution steps are still part
of the formula, and, therefore, will be a temporary learned clause itself. A permanent learned clause is created
when no Skolem clause and no temporary learned clause was part of the resolution process.
Although backtracking seems to be implemented by DQDPLL in a quite standard way, there is a non-standard
solution in dealing with satisfying branches. Whenever the current clause set is satisfied by the current branch of
the search tree, no backtracking takes place, thus, no decisions are undone and no Skolem clauses are removed.
Consequently, whenever the current branch makes the current clause set unsatisfiable and real backtracking
takes places, it might happen that the algorithm jumps back to a previous branch of the search tree. Figure 1
illustrates this particular phenomenon, where the original DQBF has an existential variable e with De = {u2 , u3 }
and DQDPLL has constructed the search tree shown in the figure so far. Let us suppose that the rightmost
branch of the tree makes the formula unsatisfiable and, therefore, the algorithm analyses the conflict and discovers
that the current assignment to e(1, 0) is one of the causes of the conflict and thus it is needed to be changed, e.g.,
from 0 to 1. Since e does not depend on u1 , it might be the case that e(1, 0) was assigned not on the rightmost
branch, but on a previous branch which assigned the same truth values to u2 and u3 as the rightmost branch
does. If this is the case, we need to backtrack to that particular branch.
e(u2 , u3 )
u1 u1
u2 u2 u2 u2
u3 u3
backtrack
e(1, 0)/0 UNSAT
Figure 1: Example of DQDPLL backtracking to a previous branch of the search tree.
Consequently, DQDPLL sometimes needs to jump several branches back and to start to traverse those branches
again. Note that for QBF this cannot happen since e would depend on all of u1 , u2 , and u3 . We think that
this phenomenon is one of the most fundamental reasons why DQDPLL “does not perform very well” [FKB12]
in practice, while QDPLL is considered to be quite effective.
Nevertheless, DQDPLL was a pioneer approach in DQBF solving. It addressed a lot of topics which later
were taken up by others. For example, pure literal reduction for DQBF was later extended and generalized
by [GWR+ 15, WGN+ 15]. Universal reduction was also used by [WGN+ 15]. VSIDS-based selection heuristics
187
were applied by [FKBV14] as well. Furthermore, DQDPLL investigated the topic of clause and cube learning
which has not been addressed by any other DQBF solving approaches yet.
4 First Killer Application – PEC Problems
A fundamental application for DQBF is partial, or imperfect, information non-cooperative games [PR79]. In
the context of Satisfiability Modulo Theories (SMT), certain bit-vector logics provide applications for DQBF,
since they have the same computational complexity [KFB12, WHdM10, KFB15] as DQBF does. Although
quantifier-free bit-vector logics (QF_BV) are the essential ingredient for hardware verification, and efficient
direct solving approaches for QF_BV exist as well as indirect ones that reduce QF_BV to other targets logics
such as EPR [KFB13] or to model checking problems [FKB13], DQBF has not succeeded to be a target logic
for QF_BV so far.
[GRS+ 13a, GRS+ 13b] show that partial equivalence checking problems can be naturally encoded as DQBFs.
Equivalence checking is about to decide if two combinational circuits always produce the same outputs from the
same inputs. If one of the circuits is not completely specified, but contains missing parts, so-called black boxes,
then the problem is called partial equivalence checking (PEC) as shown in Figure 2. PEC asks the question if
there exist implementations of all the black boxes such that the two circuits become equivalent.
Figure 2: Example of a PEC problem [GRS+ 13b].
The inputs of the combined circuit are modeled as universal variables and the outputs of the black boxes as
existential variables. Let us introduce the following notations:
~ are the inputs of the circuit
• X
• I~i are the inputs of the ith black box (1 ≤ i ≤ m)
~i are the outputs of the ith black box
• Y
• F~i (X,
~ Y~1 , . . . , Y
~i−1 ) are the functions defining I~i
~ X,
• R( ~ Y
~1 , . . . , Y
~m ) are the outputs of the circuit
Using these notations, the following DQBF encodes the PEC problem:
~ ∀I~1 . . . ∀I~m ∃Y
∀X ~1 (I~1 ) . . . ∃Y
~m (I~m ) ∃A(
~ X,
~ I~1 , . . . , I~m ) . φ0 (4)
188
where φ0 is a CNF of the following Boolean formula:
φ := I~1 6≡ F~1 (X)
~ ∨ · · · ∨ I~m 6≡ F~m (X,
~ Y~1 , . . . , Y
~m−1 ) ∨ R(
~ X,
~ Y
~1 , . . . , Y
~m )
In (4), A ~ denotes the auxiliary variables introduced by the Tseitin transformation in order to obtain from φ a
0
CNF φ of linear size.
5 Solvers
5.1 Approximation and Unrolling
DQBF generalizes QBF by allowing non-linear dependencies between variables. One could generate from the
original DQBF a QBF approximation and then to apply a QBF solver, one of the several efficient ones like
DepQBF [LB10] and RAReQS [JKMSC12]. Such a method might give non-precise results for the original DQBF
though, due to QBF not being able to capture certain dependencies.
The approach of “bounded unsatisfiability” [FT14] proposes an efficient and precise iterative QBF approxima-
tion technique that focuses on the refutation of a DQBF. Given a DQBF Φ and a bound k ≥ 1, we construct
a QBF Ψk by using k copies v 1 , . . . , v k of each variable v in the quantifier prefix and, similarly, k copies of the
matrix, in which every variable v is replaced by v 1 , . . . , v k , respectively. The approach is a refutation technique
which means to negate Ψk meanwhile, and that the satisfiability of Ψk implies that Φ is unsatisfiable.
In order to ensure the result to be precise, we also need to specify a consistency condition as a guard that
enforces the originally existential variables act according to the original dependencies defined in Φ.
Let (3) be the original DQBF. Given a bound k ≥ 1, the resulting QBF approximation looks as follows:
^ _
Ψk := ∃u11 . . . ∃uk1 ∃u12 . . . ∃ukm ∀e11 . . . ∀ek1 ∀e12 . . . ∀ekn . consistent(ei , k) ⇒ φ[v/v i ]
|{z}
1≤i≤n 1≤i≤k
∀v∈V
Note that the copies of the matrix are negated, as well as the entire quantifier prefix, which results in the type
of the quantifiers being flipped. Note furthermore that in Ψk all the existential variables are in front of the
quantifier prefix, therefore they do not depend on any of the universal variables, thus their assignments are
not restricted in any way. This is why we need the consistency conditions to add which are represented as the
following Ackermann constraints:
^ ^
consistent(e, k) := ui = uj ⇒ ei = ej
1≤i,j≤k u∈De
Note that, for the sake of readability, the formulas above are not in CNF, but it is easy to transform them to
CNF.
Φ is unsatisfiable if and only if there exists a bound k ≥ 1 such that Ψk is satisfiable. In practice, the best
way to run the approach is to start with k = 1. If Ψk is unsatisfiable, then increase the bound to k := k + 1 and
check the satisfiability of the resulting Ψk .
As the experiments in [FT14] show, the approach works fast on PEC benchmarks. This is greatly due to the
fact that for more than 94% of the PEC instances it is sufficient to use bound k = 2. However, k is proportional
to the number of black boxes in a PEC instance.
The downside of the approach is that it works in practice only for unsatisfiable DQBFs. For proving a DQBF
to be satisfiable, we need to iteratively increase k up to 2m , where m is the number of universal variables, and
to check the satisfiability of the resulting QBF in every iteration, which makes this approach infeasible for most
of the satisfiable DQBF benchmark instances.
5.2 Instantiation – iDQ
Effectively Propositional Logic (EPR) is NExpTime-complete [Lew80], i.e., it has the same computational
complexity as DQBF. Consequently, it is possible to use EPR solvers, e.g., iProver [Kor08] being the currently
most successful one, to solve DQBF given some polynomial translation from DQBF to EPR. The translation
from QBF to EPR described in [SLB12] can be extended to DQBF easily [FKBV14], as shown for the following
DQBF:
Φ := ∀u1 ∀u2 ∃e1 (u1 , u2 )∃e2 (u2 ) . (u1 ∨ e1 ) ∧ (u2 ∨ e1 ∨ e2 ) (5)
189
The translation replaces each existential variable with its Skolem function, furthermore, as a technical step,
replaces each universal variable u with p(u) where p is a fixed predicate, and adds the constraints p(1) and p(0).
Thus, the resulting EPR formula looks as follows:
∀u1 ∀u2 . p(u1 ) ∨ e1 (u1 , u2 ) ∧ p(u2 ) ∨ e1 (u1 , u2 ) ∨ e2 (u2 ) ∧ p(1) ∧ p(0)
However, since EPR solvers in general have to reason with predicates and larger domains, solvers directly working
on the Boolean level should have an advantage in solving DQBF. [FKBV14] proposes an instantiation-based
approach to solving DQBF directly, which is closely related to the so-called Inst-Gen calculus [Kor13], the
underlying decision procedure in iProver [Kor08]. The resulting solver iDQ [FKBV14] is the first publicly
available DQBF solver.
Similar to the Inst-Gen calculus and some instantiation-based QBF solving approaches such as [Ben04,
JKMSC12, JMS13], iDQ generates instances of the input clauses in a sophisticated way. A clause instance
is generated by assigning truth values to some of the universal variables in the clause. Given a clause C and lit-
erals l1 , . . . , lk , an instance of C is denoted by Cl1 ...lk , as an alternative notation for C 0 [var(l1 )/v1 , . . . , var(lk )/vk ]
where vi = 0 resp. vi = 1 if li is negative resp. positive, and C 0 is the EPR counterpart of C.
Given a DQBF Φ, iDQ starts the solving with an initial set of clause instances, which contains one instance
for each input clause. An initial instance is generated by the so-called unique minimal instantiation that removes
from the clauses all the universal literals by assigning them to 0. From (5) we get the following initial instances:
(e1 )u1 ∧ (e1 ∨ e2 )u2 (6)
We then create a Boolean over-approximation of the clause instance set by mapping the variable instances to
new Boolean variables. By doing so, we need to respect the dependencies between variables in Φ and to map the
different variable instances to different Boolean variables. The Boolean over-approximation of (6) is as follows:
(x1 ) ∧ (x2 ∨ x3 ) (7)
where x1 , x2 , x3 are the new Boolean variables. Note that the same existential variable e1 is mapped to two
different Boolean variables: the instance (e1 )u1 is mapped to x1 , and (e1 )u2 to x2 . Now we need to check if (7)
is satisfiable by using any off-the-shelf SAT solver. If the SAT solver told us that (7) was unsatisfiable, iDQ
would terminate and claim Φ to be unsatisfiable. However, (7) is satisfiable and the SAT solver could return a
satisfying assignment α = {x1 /1, x2 /0, x3 /0}.
We now check, by applying unification, whether α is a valid satisfying assignment for (6). This is the case if
and only if no pair of oppositely signed, (selected) satisfying literals corresponds to the same existential variable
such that the EPR counterparts of the two literal instances can be unified. In our example, α is indeed not a
valid assignment: x1 and x2 are selected as satisfying literals, both correspond to e1 , and their EPR counterparts
e1 (0, u2 ) and e1 (u1 , 1) can be unified. We use the most general unifier for adding two new clause instances as
follows:
(e1 )u1 ∧ (e1 )u1 u2 ∧ (e1 ∨ e2 )u2 ∧ (e1 ∨ e2 )u1 u2
The Boolean over-approximation is now given by:
(x1 ) ∧ (x2 ) ∧ (x3 ∨ x4 ) ∧ (x2 ∨ x4 ) (8)
Note that e2 is mapped to the same variable x4 in both clause instances since e2 does not depend on u1 in Φ.
(8) is satisfiable and the SAT solver could return the satisfying assignment α = {x1 /1, x2 /1, x3 /0, x4 /1}. Now,
α is valid since we can select a satisfying literal in each clause such that no unification resulting in new instances
can be applied to them. Therefore, the algorithm terminates and Φ is proven to be satisfiable.
[FKBV14] proposes a lot of implementation optimizations. Instantiation, unification, and redundancy checks
are all implemented by only using bit-vectors for the sake of taking advantage of the Boolean domain. Also
because of the Boolean domain, iDQ is able to apply VSIDS heuristics that come from SAT solving. The
reported experiments show that iDQ outperforms iProver on the DQBF benchmarks.
5.3 Elimination – HQS
Similar to the approach in Section 5.1, from DQBF a QBF approximation is generated by the solving technique
in [GWR+ 15]. The resulting DQBF solver called HQS uses an elimination-based strategy accompanied with
190
several optimizations. The strategy eliminates a minimum set of variables that cause the non-linear dependencies
in the DQBF. Once there are only linear dependencies left, an off-the-shelf QBF solver can be applied for the
remaining (QBF) formula. A lot of components of the approach rely on And-Inverter-Graphs (AIGs) [PS09].
HQS’s approach is illustrated in Figure 3. First, some preprocessing steps known from QBF preprocessing
and adapted to DQBF are applied. (We will dedicate Section 6 to the topic of DQBF preprocessing.) Gate
detection counts as a further preprocessing step, since the detected gates are used later by AIG operations.
Figure 3: Algorithmic flow of HQS [GWR+ 15].
[GWR+ 15] proposes a novel technique for observing if there are only linear dependencies left in the DQBF.
It is based on the so-called dependency graph, which is generated from the original DQBF. The vertices of the
dependency graph are the existential variables, and an edge connects e1 with e2 if and only if e1 depends on
some variable on which e2 does not depend. The dependency graph is constantly updated during the solving
process until it becomes acyclic, which shows that there are only linear dependencies left.
As an inprocessing step, unit and pure variables are eliminated in each iteration. HQS employs a rather cheap
syntactic check for unit and pure literals based on the AIG.
The main operation in each iteration is the elimination of existential and universal variables. The elimination
of an existential variable is the less expensive operation because HQS eliminates only the innermost existential
variables in the quantifier prefix, i.e., those ones that depend on all the universal variables. Given the DQBF (3),
the existential variable ei can be eliminated if Dei = {u1 , . . . , um }. In this case, the matrix φ is duplicated such
that the two duplicates replace ei with 0 and 1, respectively:
∀u1 . . . ∀um ∃e1 (De1 ) . . . ∃ei−1 (Dei−1 )∃ei+1 (Dei+1 ) . . . ∃en (Den ) . φ[ei /0] ∨ φ[ei /1] (9)
When eliminating a universal variable ui , all the existential variables ej that depend on ui must be duplicated.
Furthermore, the matrix φ must be duplicated as φ[ui /0] and φ[ui /1], similar to what we did in (9). However,
φ[ui /0] must use the original existential variables ej , while φ[ui /1] must use the duplicates e0j .
∀u1 . . . ∀ui−1 ∀ui+1 . . . ∀um ∃e1 De1 \ {ui } . . . ∃en Den \ {ui } ∃e0j Dej \ {ui } .
(10)
| {z }
∀ej . ui ∈Dej
φ[ui /0] ∧ φ[ui /1, ej /e0j ]
| {z }
∀ej . ui ∈Dej
The elimination of a universal variable is rather expensive, this is why the next universal variable to eliminate is
chosen by some heuristics. First, the approach determines the minimal set of universal variables whose elimination
191
leads to a QBF problem. The problem of finding this minimal set is expressed as a MaxSAT problem as explained
in [GWR+ 15]. Then, these universal variables are ordered according to the number of the existential variables
which would be duplicated in (10).
The experiments reported in [GWR+ 15] compare HQS against iDQ. The results show that HQS is able to
solve 50% more benchmark instances than iDQ and speeds up the computation time by up to four orders of
magnitude. Unfortunately, HQS is not publicly available.
6 Preprocessing
In practice, it is crucial to apply preprocessing to the input formula before it is passed to an actual solver. Pre-
processing techniques often reduce the computation time of solvers by orders of magnitude. For QBF, there exist
efficient preprocessing tools in practice like sQueezeBF [GMN10] and bloqqer [BLS11]. The paper [WGN+ 15] pro-
poses several preprocessing techniques for DQBF, as a continuation of the work has been started in [GWR+ 15],
and reports successful experiments with the solvers iDQ and HQS. All of these preprocessing techniques are
the generalizations of known preprocessing techniques for SAT and QBF.
Universal reduction is a well-known simplification technique for QBF that can be easily adapted to DQBF.
In any clause C, if there is a universal literal l ∈ C such that no other literal k ∈ C depends on l, then l can be
removed from C. The condition of k not depending on l can be formalized as var(l) ∈ / Dk .
Another technique that comes from QBF solving is eliminating an existential variable by resolution. By
applying all the possible resolution steps to the matrix on an existential variable e, one can eliminate e from the
formula completely. However, there is a necessary condition for applying this preprocessing step: in all clauses
C that contain e, all the literals k ∈ C must only depend on variables on which e depends, i.e., Dk ⊆ De .
Note however that it might be rather expensive to apply all the possible resolution steps since the number of
clauses might grow considerably. Therefore it is necessary to apply some cost function, e.g., the one defined
in [WGN+ 15], in order to decide if it is worth to eliminate a particular existential variable in this way.
Unit and pure literals can be replaced by the constants 0 or 1 without influencing the formula’s truth value. For
DQBF, it is worth to generalize unit and pure literals by introducing the concepts of backbones and monotonic
variables, respectively. In a Boolean formula φ, a variable v is a backbone if (B0) φ[v/0] or (B1) φ[v/1] is
unsatisfiable. A variable v is a monotonic if (M0) φ[v/0] ∧ φ[v/1] or (M1) φ[v/1] ∧ φ[v/0] is unsatisfiable. Note
that the checks of a variable being backbone or monotonic can be done by a SAT solver on the matrix of the
DQBF, therefore they count as cheap checks. Of course, we also need to define what to do with the DQBF Φ
if it turned out v was a backbone or monotonic:
• If v is a universal variable:
– In case of (B0) or (B1), Φ is unsatisfiable.
– In case of (M0), eliminate v by replacing with 0.
– In case of (M1), eliminate v by replacing with 1.
• If v is an existential variable:
– In case of (B0) or (M0): eliminate v by replacing with 1.
– In case of (B1) or (M1): eliminate v by replacing with 0.
Blocked clauses are important to detect in both SAT and QBF solving [JBH10, BLS11], since blocked clauses
can be removed from a formula without changing its truth value. For DQBF, a literal l blocks a clause C with
l ∈ C if for all other clauses C 0 with l ∈ C 0
• the resolvent of C and C 0 on l is tautological, i.e., it contains both k and k for some variable k, and
• Dk ⊆ Dl .
Since removing blocked clauses makes the original formula shorter, one might want to increase the chance of
finding blocked clauses by temporarily extending the clauses with so-called hidden and covered literals as detailed
in [GWR+ 15].
In QBF solving it usually pays off to reduce the dependency sets of variables [LB09, Gel11, SS12]. The concept
can be easily adapted to DQBF. Even if u ∈ De for some universal variable u and some existential variable e,
192
due to the structure of the matrix, it might turn out that the Skolem function of e does not use u’s value at all to
satisfy the formula, therefore u can be removed from De . Since this semantic check has the same complexity as
DQBF solving itself, sufficient syntactic criteria called dependency schemes are applied instead. In [GWR+ 15],
the co-called standard dependency scheme is defined for DQBF. From the input formula an undirected graph is
constructed which contains all the formula’s variables v and clauses C as vertices, and creates an edge from v to
C if v appears in C. The standard dependency scheme is defined as follows: an existential variable e does not
depend on a universal variable u if there is no path in the graph between u and e, visiting only such existential
variables e0 that u ∈ De0 .
An interesting choice for a preprocessing step is the QBF approximation technique using unrolling by [FT14],
which we have already described in Section 5.1. In the experiments in [GWR+ 15], this unrolling technique with
a bound k = 1 and k = 2 is used.
The experiments in [GWR+ 15] apply various preprocessing techniques, including the ones above, in several
combinations. Interestingly, the results show that the preprocessor alone is able to solve a considerable amount
of benchmark instances. On the remaining instances, the DQBF solvers iDQ and HQS were executed, and the
results show that preprocessing increases the number of solved instances by a factor of ca. 2.5. Computation
time often drops by orders of magnitude.
7 Further Advances in DQBF Solving
A very recent paper [WSWB16] investigates if the dependency schemes for QBF could be lifted to DQBF. Note
that the standard dependency scheme has already been addressed by [WGN+ 15], cf. Section 6. Other kinds of
dependency schemes are also known for QBF, therefore [WSWB16] investigates how to adapt them to DQBF
and checks if the resulting dependency schemes are sound. The overall picture of those dependency schemes
can be seen in Figure 4, where the ones inside the blue box are proved to be sound for DQBF, while the ones
outside of the blue box to be unsound. Without getting into details, all the different variants of the standard
dependency scheme, whose notations start with ’s’, are sound, which shows that [WGN+ 15] has chosen a proper
dependency scheme for preprocessing, cf. Section 6. It is also interesting that the reflexive dependency schemes,
whose notations start with ’r’, are sound as well. From the soundness point of view, it does not matter if one picks
either a quadrangle or a triangle dependency scheme, and, similarly, if one picks resolution path connectedness
between clauses instead of the usual notion of connectedness.
Figure 4: Different dependency schemes for DQBF [WSWB16]. Those outside of the blue box are not sound.
Even if DQBF solvers like iDQ and HQS can tell us whether a DQBF is satisfiable, in practice we also
need to synthesize Skolem functions for the existential variables. From this point of view, DQBF certification
is investigated in [BCJ13]. Since Skolem functions could be obtained from resolution proofs, the paper presents
a kind of negative result though: the DQBF-version of Q-resolution is incomplete.
A very recent paper [BCSS16] investigates how the different resolution systems for QBF can be lifted to
DQBF, and if the lifted variants are sound and/or complete. The overall picture of those resolution calculi can
be seen in Figure 5. Without getting into details, Q-resolution (Q-Res), which is the best-studied resolution
system for QBF, is incomplete for DQBF, as it was already shown by [BCJ13]. From the completeness point
of view, it does not matter if resolution steps are also allowed on universal variables (QU-Res). Interestingly,
if long-distance resolution is applied (LD-Q-Res, LQU+ -Res), the resulting calculi become unsound. However,
193
there exist instantiation-based calculi that are sound and complete for DQBF: ∀Exp+Res can be considered
a very simple instantiation-based calculus, which IR-calc extends with partial assignments. IRM-calc combines
IR-calc with solutions from LD-Q-Res which make the calculus unsound.
Figure 5: Resolution systems lifted to DQBF and their soundness/completeness [BCSS16].
8 Conclusion
In this paper, we gave a thorough survey on the state-of-the-art of DQBF solving. We reported the advent of
the first practically efficient solving approaches and solver implementations, such as iDQ and HQS. Since, in
practice, it is crucial to apply preprocessing before solving the actual formula, it is good news that a powerful
DQBF preprocessor was implemented recently. DQBF solving is an emerging area as shown by the recent
advances that we summarize at the end of the paper.
References
[BCJ13] V. Balabanov, H. K. Chiang, and J. R. Jiang. Henkin quantifiers and boolean formulae: A certifi-
cation perspective of DQBF. Theoretical Computer Science, 2013.
[BCSS16] O. Beyersdorff, L. Chew, R. A. Schmidt, and M. Suda. Lifting qbf resolution calculi to DQBF. In
Proc. SAT 2016, volume 9710 of LNCS, pages 490–499, 2016.
[Ben04] M. Benedetti. Evaluating QBFs via symbolic skolemization. In Proc. LPAR 2004, pages 285–300,
2004.
[BLS11] A. Biere, F. Lonsing, and M. Seidl. Blocked clause elimination for QBF. In Proc. CADE 2011,
volume 6803 of LNCS, pages 101–115, 2011.
[CGS98] M. Cadoli, A. Giovanardi, and M. Schaerf. Algorithm to evaluate Quantified Boolean Formulae,
pages 262–267. 1998.
[FKB12] A. Fröhlich, G. Kovásznai, and A. Biere. A DPLL algorithm for solving DQBF. In Proc. POS 2012,
2012.
[FKB13] A. Fröhlich, G. Kovásznai, and A. Biere. Efficiently solving bit-vector problems using model checkers.
In Proc. SMT 2013, pages 6–15, 2013.
[FKBV14] A. Fröhlich, G. Kovásznai, A. Biere, and H. Veith. iDQ: Instantiation-based DQBF solving. In
Proc. POS 2014, aff. to SAT 2014, pages 103–116, 2014.
[FT14] B. Finkbeiner and L. Tentrup. Fast DQBF refutation. In Proc. SAT 2014, volume 8561 of LNCS,
pages 243–251, 2014.
[Gel11] A. Van Gelder. Variable independence and resolution paths for quantified boolean formulas. In
Proc. CP 2011, volume 6876 of LNCS, pages 789–803, 2011.
194
[GMN10] E. Giunchiglia, P. Marin, and M. Narizzano. squeezebf: An effective preprocessor for QBFs based
on equivalence reasoning. In Proc. SAT 2010, volume 6803 of LNCS, pages 85–98, 2010.
[GRS+ 13a] K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker. Equivalence checking for
partial implementations revisited. In Proc. MBMV 2013, pages 61–70, 2013.
[GRS+ 13b] K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker. Equivalence checking of
partial designs using dependency quantified boolean formulae. In Proc. ICCD 2013, pages 396–403,
2013.
[GWR+ 15] K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, and B. Becker. Solving DQBF through
quantifier elimination. In Proc. DATE 2015, pages 1617–1622. EDA Consortium, 2015.
[Hen61] L. Henkin. Some remarks on infinitely long formulas. In Infinistic Methods, pages 167–183. Pergamon
Press, 1961.
[JBH10] M. Järvisalo, A. Biere, and M. Heule. Blocked Clause Elimination, volume 6015 of LNCS, pages
129–144. 2010.
[JKMSC12] M. Janota, W. Klieber, J. Marques-Silva, and E. Clarke. Solving QBF with counterexample guided
refinement. In Proc. SAT 2012, volume 7317 of LNCS, pages 114–128, 2012.
[JMS13] M. Janota and J. Marques-Silva. On propositional QBF expansions and Q-resolution. In
Proc. SAT 2013, volume 7962 of LNCS, pages 67–82, 2013.
[KFB12] G. Kovásznai, A. Fröhlich, and A. Biere. On the complexity of fixed-size bit-vector logics with
binary encoded bit-width. In Proc. SMT 2012, 2012.
[KFB13] G. Kovásznai, A. Fröhlich, and A. Biere. BV2EPR: a tool for polynomially translating quantifier-free
bit-vector formulas into EPR. In Proc. CADE 2013, volume 7898 of LNAI, pages 443–449, 2013.
[KFB15] G. Kovásznai, A. Fröhlich, and A. Biere. Complexity of fixed-size bit-vector logics. Theory of
Computing Systems, pages 1–54, 2015.
[Kor08] K. Korovin. iProver – an instantiation-based theorem prover for first-order logic (system description).
In Proc. IJCAR 2008, 2008.
[Kor13] K. Korovin. Inst-Gen - a modular approach to instantiation-based automated reasoning. In Pro-
gramming Logics, pages 239–270, 2013.
[LB09] F. Lonsing and A. Biere. A compact representation for syntactic dependencies in QBFs. In
Proc. SAT 2009, volume 5584 of LNCS, pages 398–411, 2009.
[LB10] F. Lonsing and A. Biere. Depqbf: A dependency-aware QBF solver. JSAT, 7(2-3):71–76, 2010.
[Lew80] H. R. Lewis. Complexity results for classes of quantificational formulas. Journal of Computer and
System Sciences, 21(3):317–353, 1980.
[Pap94] C. H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.
[PR79] G. L. Peterson and J. H. Reif. Multiple-person alternation. In Proc. FOCS 2079, pages 348–363,
1979.
[PRA01] G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete
information, 2001.
[PS09] F. Pigorsch and C. Scholl. Exploiting structure in an AIG based QBF solver. In Proc. DATE 2009,
pages 1596–1601, 2009.
[SLB12] M. Seidl, F. Lonsing, and A. Biere. QBF2EPR: A tool for generating EPR formulas from QBF. In
Proc. PAAR 2012, 2012.
195
[SS12] F. Slivovsky and S. Szeider. Computing resolution-path dependencies in linear time ,. In
Proc. SAT 2012, volume 7317 of LNCS, pages 58–71, 2012.
[WGN+ 15] R. Wimmer, K. Gitina, J. Nist, C. Scholl, and B. Becker. Preprocessing for DQBF. In
Proc. SAT 2015, volume 9340 of LNCS, pages 173–190, 2015.
[WHdM10] C. M. Wintersteiger, Y. Hamadi, and L. de Moura. Efficiently solving quantified bit-vector formulas.
In Proc. FMCAD 2010, 2010.
[WSWB16] R. Wimmer, C. Scholl, K. Wimmer, and B. Becker. Dependency schemes for DQBF. In
Proc. SAT 2016, volume 9710 of LNCS, pages 473–489, 2016.
196