In recent years, various approaches for quantified Boolean formula (QBF) solving have been developed, including methods based on expansion, skolemization and search. Here, we present a novel expansionbased solving technique that is motivated by concepts from the area of parameterized complexity. Our approach relies on dynamic programming over the tree decomposition of QBFs in prenex conjunctive normal form (PCNF). Hereby, BDDs are used for compactly storing partial solutions. Towards efficiency in practice, we integrate dependency schemes and dedicated heuristic strategies. Our experimental evaluation reveals that our implementation is competitive to state-of-the-art solvers on instances with one quantifier alternation. Furthermore, it performs particularly well on instances up to a treewidth of approximately 80. Results indicate that our approach is orthogonal to existing techniques, with a large number of uniquely solved instances.
Quantified Boolean formulae (QBFs) extend propositional logic by explicit
universal and existential quantification over variables. They can be used to
compactly encode many computationally hard problems, which makes them amenable
to application fields where highly complex tasks emerge, e.g. formal verification,
synthesis, and planning. In this work we consider the problem of deciding
satisfiability of QBFs (QSAT) which is, in general, PSPACE-complete [33]. We
present an approach that is motivated by results from the area of parameterized
complexity: many computationally hard problems are fixed-parameter tractable
(fpt) [14], i.e., they can be solved in time f (p) · nO(1) where n is the input size,
p the parameter, and f a computable function. It is known that QSAT is fpt
w.r.t. the combined parameter quantifier alternations plus treewidth of the QBF
instance (this follows from [12]), but not w.r.t. treewidth alone [
Intuitively, treewidth captures the “tree-likeness” of a graph. It emerged from the observation that computationally hard problems are usually easier to be solved on trees than they are on arbitrary graphs. Treewidth is defined on tree decompositions (TDs). Our approach employs dynamic programming (DP) over the TD of the primal graph of QBFs in prenex conjunctive normal form (PCNF). Partial solutions of the DP are obtained via locally restricted expansion. The practical feasibility of this approach rests on the following pillars. First, we make use of binary decision diagrams (BDDs) [10] for compactly storing information in our dedicated data structure. Second, we consider structure in the quantifier prefix by integrating dependency schemes (see, e.g., [31]) into our DP algorithm. Finally, we introduce optimization techniques such as dynamic variable removal and TD selection based on characteristics beyond treewidth. By design, our novel approach is expected suitable for QBF instances of low-to-medium treewidth and a restricted number of quantifier alternations.
The concept most closely related to ours was developed by Pan and Vardi [24].
There, variables are eliminated based on an elimination ordering that also
underlies the construction of the tree decomposition in our approach. However, their
approach requires the variables to be eliminated from the inner- to the
outermost quantifier level, a restriction that we circumvent in this work. Treewidth
and its relation to (empirical) hardness of QBFs was studied, for instance, by
Pulina and Tacchella [27] and Marin etal. [23]. There, quantified treewidth is
considered, a generalization of primal treewidth that includes the variable
ordering as specified in the QBF prefix. Additionally, there exists a QBF solver
that uses treewidth to dynamically decide between resolution and search during
the solving process [26]. Further approaches that consider structural aspects of
QBFs include search-based solving based on dependencies between variables [22],
decomposition of the QBF according to the quantifier level of variables [28], and
restoring structure in instances converted to PCNF [
The presented algorithms are implemented in the QBF solver dynQBF which is freely available at https://dbai.tuwien.ac.at/proj/decodyn/dynqbf/. We conduct an experimental evaluation along the lines of the QBF competition [25] in 2016. In comparison with state-of-the-art solvers, results show that our approach is particularly competitive on instances with one quantifier alternation. Furthermore, the implementation performs well on instances that exhibit a width of up to 80, even for instances with more quantifier alternations. Additionally, we observe a large number of instances that is uniquely solved by dynQBF. These observations underline the practical potential of parameterized algorithms in highly competitive domains and we believe that the techniques used in our system (space efficient storage via BDDs, TD selection, etc.) will also prove useful when efficient dynamic programming algorithms for other problems are to be implemented. 2
As usual, a literal is a variable or its negation. A clause is a disjunction of literals. A Boolean formula in conjunctive normal form (CNF) is a conjunction of clauses. We sometimes denote clauses as sets of literals, and a formula in CNF as a set of clauses. Herein, we consider quantified Boolean formulae (QBFs) in closed prenex CNF (PCNF) form.
Definition 1. In a PCNF QBF Q.ψ, Q is the quantifier prefix and ψ is a CNF formula, also called the matrix. Q is of the form Q1X1Q2X2 . . . QkXk where Qi ∈ {∃, ∀} for 1 ≤ i ≤ k, Qi = Qi+1 for 1 ≤ i < k, and X = {X1, . . . , Xk} is a partition over all variables in ψ. For a variable x ∈ Xl (1 ≤ l ≤ k), l is the level of x, and k − l + 1 the depth of x.
We frequently use the following notation: Given a QBF Q.ψ with Q = Q1X1 . . . QkXk and an index i with 1 ≤ i ≤ k, quantifier Q(i) = Qi gives the i-th quantifier. For a variable x, levelQ (x) returns the level of x; depthQ (x) returns the depth of x in Q; and quantifierQ (x) = QlevelQ (x) returns the quantifier for x. Finally, for a clause c ∈ ψ, we denote by variablesψ(c) the variables occurring in c. We will usually omit the subscripts whenever no ambiguity arises. Example 1. As our running example, we will consider the QBF Q.ψ with Q = ∃ab ∀cd ∃ef and ψ = (a ∨ c ∨ e) ∧ (¬a ∨ b) ∧ (¬b ∨ f ) ∧ (d ∨ ¬e), which is satisfiable.
A tree decomposition (TD) [29] is a mapping from a graph to a tree, where each node in the TD can contain several vertices of the original graph. Definition 2. A tree decomposition of a graph G = (V, E) is a pair T = (T, bagT ) where T = (N, F ) is a (rooted) tree with nodes N and edges F , and bagT : N → 2V assigns to each node a set of vertices, such that: 1. For every vertex v ∈ V , there exists a node n ∈ N such that v ∈ bagT (n). 2. For every edge e ∈ E, there exists a node n ∈ N such that e ⊆ bagT (n). 3. For every vertex v ∈ V , the subtree of T induced by {n ∈ N | v ∈ bagT (n)} is connected.
Intuitively, Condition 1 and 2 guarantee that the whole graph is covered by
the TD, and Condition 3 is the connectedness property, which, roughly speaking,
states that a vertex cannot “reappear” in unconnected parts (w.r.t. the bags).
The width of T is defined as maxn∈N |bagT (n)| − 1. The treewidth t of a graph
is the minimum width over all its TDs. Given a graph and an integer t, deciding
whether the graph has at most treewidth t is NP-complete [
A TD T = ((N, F ), bagT ) is weakly normalized, if each n ∈ N is either a leaf node (n has no children), an exchange node (n has exactly one child n1, such that bagT (n) = baTg(n1)), or a join (n has children n1, . . . , nm such that m ≥ 2, and bagT (n) = bagT (n1) = · · · = bagT (nm)). Given a TD T = (T, bagT ) with T = (N, F ), for a node n ∈ N we denote its set of children in T by childrenT (n). We specify firstChild T (n) and nextChild T (n) to iterate over the children, and hasNextChild T (n) to check whether further children exist. The node type is checked with isLeafT (n), isExchangeT (n) and isJoinT (n). For a node n with single child node n1, changed bag contents are accessed by introduced T (n) = G:
a c e b
f d
T :
n6 a, c, e n3 a, c, e n2 a, b n1 b, f n5 a, c, e n4 d, e bag T (n) \ bag T (n1) and removed T (n) = bag T (n1) \ bag T (n). isRootT (n) returns true if n has no parent node.
Our algorithm for QBF solving is based on a TD of the given QBF Q.ψ, which is obtained from the graph Gψ = (V, E) where V are the variables occurring in ψ and each clause in ψ forms a clique in Gψ, i.e. E = {(x, y) | x, y ∈ variablesψ(c), c ∈ ψ, x = y} (called primal or Gaifman graph). Given a TD T = (T, bag T ) of QBF Q.ψ, we define clausesT ,ψ(n) = {c ∈ ψ | variablesψ(c) ⊆ bag T (n)}.
Example 2. Consider our running example. Figure 1 illustrates the graph representation G of ψ, and T is a weakly-normalized TD for G of width 2. 3
In a nutshell, the algorithm proceeds as follows. Given a QBF instance Q.ψ, we heuristically construct a weakly normalized TD T = (T, bag T ) with T = (N, F ) of the primal graph of ψ. Then, T is traversed in post-order. For each n ∈ N we compute partial solution candidates and store them in a dedicated data structure. In this context, partial means that the data structure is restricted to variables occurring in bag T (n). Candidate refers to the fact that other parts of the QBF might not yet be considered. At the root node, the whole instance was taken into account and the problem is decided. 3.1
We define so-called nested sets of formulae (NSFs) where the innermost sets contain reduced ordered binary decision diagrams (BDDs) [10]. A BDD compactly represents Boolean formulae in form of a rooted directed acyclic graph (DAG). For a fixed variable ordering, BDDs are canonical, i.e., equivalent formulae are represented by the same BDD, a property that is vital to our approach. Intuitively, nestings will be used to differentiate between quantifier blocks, and BDDs store parts of the QBF matrix.
Definition 3. Given a QBF Q.ψ with k quantifiers, we have a nested set of formulae (NSF) of depth k which is inductively defined over the depth of nestings d with 0 ≤ d ≤ k: for d = 0, the NSF is a BDD; for 1 ≤ d ≤ k, the NSF is a set of NSFs of depth d − 1.
For a QBF Q.ψ with Q = Q1X1 . . . QkXk and an NSF N of depth k, for any NSF M appearing somewhere in N we denote by depth(M ) the depth of the nesting of M , level Q(M ) = k − depth(M ) + 1 is the level of M , and quantifier Q(M ) = QlevelQ(M) (for level Q(M ) ≤ k). We define the procedure init (k, φ) that initializes an NSF with k levels (and hence of depth k), such that each set contains exactly one NSF, and the innermost NSF represents φ. For instance, init (3, ) returns {{{ }}}. Furthermore, for an NSF N we denote by N [B/B ] the replacement of each BDD B in N by B . For a BDD B, restriction of a variable v is denoted by B[v/ ] or B[v/⊥]. Quantification and standard logical operators are applied as usual.
Example 3. Suppose we are given an NSF N = {{{ , ⊥}}, {{¬a ∨ b}, {⊥}, {a ∧ b}}}. In the examples, we will illustrate nested sets as trees where leaves contain the formulae represented by the BDDs. Figure 2 shows the tree representing N together with the one resulting from N [B/B ∧ c].
NSFs can be used to efficiently keep track of parts of the solution space
(with respect to the TD), instead of representing the whole QBF instance at
once. Internal elements of the NSF have quantifier semantics, as we will show
later. Opposed to the similar concept of quantifier trees [
Algorithm 1 illustrates the recursive procedure for the post-order traversal of the TD and computing the partial solution candidates. It is called with the root node of the TD and returns an NSF that represents the overall solution. In leaf nodes, an NSF of k levels is initialized with the innermost set containing a BDD that represents the clauses associated with the current node. In an exchange node, variables are removed as well as introduced (w.r.t. the bag’s contents). Removed variables are handled by “splitting” the NSF. Procedure split (N, x) (see Algorithm 2) implements a variant of locally restricted expansion: at the level of x in N , each NSF M contained in N is replaced by two NSFs that distinguish between assignments of x to ⊥ and . Observe that thereby any occurrence of x in the BDDs is removed. This guarantees that the size of each BDD
Output: An NSF with partial solution candidates for n 1 if isLeaf (n) then N := init(k, clauses(n)) 2 if isExchange(n) then 3 N := solve(firstChild(n)) 4 for x ∈ removed(n) do N := split(N, x) 5 N := N [B/B ∧ clauses(n)] 6 if isJoin(n) then 7 N := solve(firstChild(n)) 8 while hasNextChild(n) do 9 M := solve(nextChild(n)) 10 N := join(N, M ) 11 end 12 if isRoot(n) then N := evaluateQ(n, N ) 13 return N
if level(N ) = level(x) then
return {M [B/B[x/⊥]], M [B/B[x/]] | M ∈ N } else return {split(M, x) | M ∈ N }
if depth(N1) = 0 then return N1 ∧ N2 else return {join(M1, M2) | M1 ∈ N1, M2 ∈ N2} is bounded by the bag’s size. Furthermore, since (reduced ordered) BDDs are canonical and thanks to the set semantics of NSFs, the overall resulting NSF’s size is bounded by the bag’s size and depth (i.e., the number of quantifiers). Removal of variable x from the BDDs is admissible due to the connectedness property of the TD: x will never reappear somewhere upwards the TD, and therefore all clauses containing x were already considered. After splitting, the clauses associated with the current node are added to the NSF’s BDDs via conjunction. In join nodes, NSFs computed in the child nodes are successively combined by procedure join(N1, N2) (see Algorithm 3). The procedure guarantees that the structure (nesting) of the NSFs to be joined is preserved. BDDs in the NSFs are combined via conjunction, thus already considered information of both child nodes is retained.
if depth(N ) = 0 then B := N else
X := {x | x ∈ bag(n) and level (x) = level (N )} if quantifier (N ) = ∃ then
B := ∃X M∈N evaluateQ(n, M ) else if quantifier (N ) = ∀ then
B := ∀X M∈N evaluateQ(n, M ) return B n6 n3 n2 ¬a ∧ ¬b
So far, quantifiers were not taken into account in our algorithm. This is only done in the root node r of the TD, where the problem is decided by applying quantifier elimination as shown in Algorithm 4. Our approach is similar to that described by Pan and Vardi [24], but restricted to the bag contents and quantifiers are recursively evaluated over the nestings. Procedure evaluateQ (r, N ) combines the elements of the NSF by disjunction (for existential quantifiers) or conjunction (for universal quantifiers), starting at the innermost NSFs. Thereby, variables contained in the current bag are removed by quantified abstraction (i.e., they get existentially or universally quantified and thereby also removed from the BDDs). Thus, this procedure finally returns a single BDD B without variables. If B ≡ ⊥, the QBF is unsatisfiable, otherwise it is satisfiable.
Example 4. Figure 3 shows the NSFs computed at the TD nodes of our running example (without quantifier evaluation at the root node). In n1, an NSF of depth 3 is initialized with (¬b ∨ f ), i.e., the clause associated with this TD node. In n2, ∃ ∀ ∃
¬a ∧ c variable f is removed. Hence the NSF is split at level (f ) = 3, once by setting f to ⊥ (left NSF branch) yielding ¬b, and once by (right branch), yielding . Furthermore, the current clause (¬a∨b) is added to these BDDs via conjunction, giving {{{¬a ∧ ¬b, (¬a ∨ b)}}}. The algorithm proceeds similarly for nodes n3, n4 and n5. In n6, the NSFs are joined. For instance, the leftmost branches in n3 and n5 are joined by conjunction of ¬a ∧ (c ∨ e) and ¬e ∧ (a ∨ c), yielding ¬a ∧ ¬e ∧ c. Figure 4 shows the NSF N in root node n6 together with the BDDs obtained recursively when applying evaluateQ (n6, N ). The procedure returns , as the QBF from Example 1 is satisfiable. Quantifiers in QBFs introduce dependencies between variables. Let x and y be variables of the QBF, and assume that y is dependent on x. Then, the assignment to y is dependent on the assignment to x [30] (i.e., reordering x and y in the prefix changes satisfiability). So far, when a variable is removed splitting is applied to distinguish between variable assignments. With this, even if x is removed before y, we implicitly keep track of these assignments in our NSF data structure. Hence, when y is removed later, its dependency on x is accounted for, and our algorithm remains sound. However, if all variables dependent on x were already removed, the distinction between assignments is not necessary. We considered several dependency schemes (for details, see e.g., [31]). Let Q.ψ be a PCNF QBF with k quantifiers and x, y be variables of Q.ψ. Then (x, y) ∈ DQS.ψ w.r.t. dependency scheme S ∈ {naive, simple, standard } if: 1. naive: level (x) < k; 2. simple: level (x) < level (y); and 3. standard: level (x) < level (y), quantifier (x) = quantifier (y) and there is an X-path from x to y for some X ⊆ {z | z ∈ Xi, level (x) < i ≤ k, quantifier (z) = ∃}. An X-path is a sequence c1, . . . , cl of clauses in ψ, s.t. x ∈ c1, y ∈ cl and cj ∩ cj+1 ∩ X = ∅ for 1 ≤ j < l (see [21] for details). dependentSQ.ψ(x) = {y | (x, y) ∈ DQS.ψ} denotes the set of variables that are dependent on x in Q.ψ w.r.t. S.
Towards our adapted algorithm, for a TD node n of T , we recursively define by removedSubT (n) = removed T (n) ∪ m∈childrenT (n) removedSubT (m) the set of removed variables in the subtree of T rooted at n. Let removedBelow T (n) = Algorithm 5: S-dependentSplit (n, N, x)
Output: An NSF with abstracted or split x if dependent S(x) ⊆ removedBelow (n) then if quantifier (x) = ∃ then return N [B/∃xB] if quantifier (x) = ∀ then return N [B/∀xB] else return split(N, x) removedSubT (n) \ removed T (n) be the variables removed below n in T . In Algorithm 1, split (M, x) is replaced with S-dependentSplit (n, N, x) (see Algorithm 5). Whenever all variables dependent on x were already removed, x is removed by quantified abstraction. Otherwise, the standard split (N, x) procedure is called. Example 5. The NSF at node n2 of Figure 3 reduces to {{{(¬a∨b)}}} (for all dependency schemes). Furthermore, we have DQst.aψndard = {(a, c), (a, d), (c, e), (d, e)}. Since dependent (b) = {}, b can be existentially abstracted in n3. However, in n5, d must be split, since dependent (d) = {e} ⊆ removedBelow (5n) = {}.
We remark that for all considered dependency schemes variables at the innermost level can be removed by quantified abstraction. Hence our algorithms can be simplified, as the NSFs at depth 1 always only contain a single BDD. In particular, for 2-QBFs (i.e. instances of the form ∀X1∃X2.ψ) the general NSF data structure could then be replaced by just a set of BDDs. Furthermore, we observed that in almost all 2-QBF instances (used in Section 5) variables at level 2 are dependent on those at level 1. For 2-QBFs, we thus apply the easily computable naive dependency scheme. For other instances standard turned out to be superior to simple and naive. 4
Clause splitting. Given a QBF Q.ψ, we construct a TD of width w for the primal graph of ψ. Due to Conditions 2 and 3 of Definition 2, w ≥ maxc∈ψ|c| − 1 holds, i.e., the size of the largest clause gives a lower bound for w. To reduce this bound, we apply clause splitting, which is a standard technique implemented in many QBF solvers and preprocessors: a fresh variable is added (once positively, once negatively) to the parts of a split clause, and quantified existentially in the innermost quantifier block. Experiments preceding this work reveal that splitting clauses larger than 30 yields good results, without introducing too many additional variables.
TD selection. It was shown that TD characteristics besides width play a crucial
role in practice [
end else if depth(N ) > 1 then for M ∈ N do M := removeRedundant(M ) for M1, M2 ∈ N and M1 = M2 do
if M1 ⊂ M2 then N := N \ {M2} for M1, M2 ∈ N and M1 = M2 do if quantifier (N ) = ∃ and M1 ∨ M2 = M1 then
N := N \ {M2} if quantifier (N ) = ∀ and M1 ∧ M2 = M1 then
N := N \ {M2}
end
return N
Additionally, we consider the following TD characteristic. Variable dependencies
can be exploited more efficiently if the variables are removed in the TD from the
innermost to the outermost quantifier block. Let removedBelowLevel T ,Q(n, l) =
{b | b ∈ removedBelow T (n) and level Q(b) < l}. Now, removedLevel (T , Q) =
n∈N r∈removedT (n) |removedBelowLevel T ,Q(n, level (r))|. We construct several
TDs (using the min-fill heuristics [13]) and then select the one minimizing
joinChildCount (T ) (for 2-QBFs) or removedLevel (T , Q) (for instances with more
quantifier blocks). We observe that 10 decompositions are sufficient to increase
performance, despite the additional effort in the decomposition step.
Redundant NSF removal. Two BDDs in the same nesting of an NSF are
redundant if they are in a subset relation w.r.t. the represented models (which
is similar to subsumption checking [
Example 6. Figure 5 shows an NSF N before and after removeRedundant(N ). For instance, consider the leftmost branch of the NSF at depth 1, i.e. {⊥, ¬a}. Since quantifier (N1) = ∃ and ⊥ ∨ ¬a ≡ ¬a, ⊥ is removed. At depth 2, we subsequently have {{¬a}, {¬a, c}}. Since {¬a} ⊆ {¬a, c}, {¬a, c} is removed. Intermediate unsatisfiability checks. Procedure evaluateQ (n, N ) can be applied to any NSF during the TD traversal. If it returns ⊥, the QBF is unsatisfiable. 1 When dependency schemes are considered, the NSFs at depth 1 contain only a single
∃ ∀ ∃ ⊥ ¬a ¬a c a a ∨ c
a ∨ c ∃ ∀ ∃ ¬a
However, if it returns , the QBF might still be unsatisfiable due to clauses that are encountered later in the traversal. In our setting, the overhead for these checks is negligible.
Estimated NSF size. For a node n of decomposition T , let sizeNSF (n) be the number of BDDs in the NSF N computed at node n, and maxSizeBDD (n) be the size of the largest BDD in N . The size of a BDD is determined by the number of nodes in the DAG of the BDD. sizeNSF (n) can be kept small by delaying splitting of removed variables. Instead, the variable is stored in a cache for later removal. However, this usually increases maxSizeBDD (n) (since the variable is not removed from the BDDs), and the size of BDDs is no longer bounded by the bag size. Hence, NSF and BDD sizes have to be carefully balanced. BDD variable ordering. The size of a BDD can be exponential in the number of variables. Nontheless, in practice the size may be exponentially smaller, in particular in case a “good” variable ordering is applied [16]. Since finding an optimal variable ordering is in general NP-hard [10], BDD-internal heuristics for finding such a good ordering can be used. For our purposes, we initialize the ordering with the variables’ occurrence in the instance (which usually implies that the ordering corresponds to their occurrence in the QBF prefix), and apply dynamic reordering during the computation via lazy sifting. 5
The presented algorithms are implemented in the dynQBF system, which relies
on HTD [
In the following, we report on the number of solved, solved satisfiable ( ) and unsatisfiable (⊥) instances. The stated time is the accumulated user time in thousands of seconds (K), including a penalty of 600 seconds per instance that is not solved. Additionally, we give the number of instances uniquely solved by a single system (U). dynQBF is run with one random, fixed seed. However, the performance is influenced by the heuristically constructed TD. To gain an insight into the potential of our current implementation, we also provide a virtual best dynQBF analysis over 10 seeds (each running for up to 10 minutes). Best of 10 (Bo10 ) reports the number of instances solved in any of the 10 runs, as well as the minimum time required, and average of 10 (Ao10 ) reports the average case. 2-QBF’16. Table 1 shows that our system is competitive to state-of-the-art solvers on 2-QBF instances. On the original instances, only the 2-QBF solver AReQS performs better. When considering 10 different seeds, Bo10 indicates that there is still potential for our feature-based tree decomposition selection. Regarding preprocessing, 130 out of 305 instances are directly solved by Bloqqer. Qesto and RAReQS benefit the most from preprocessing. Overall, dynQBF is particularly strong on satisfiable instances. Additionally, we report on a large number of uniquely solved instances. For the original data set, they mostly stem from QBF encodings for ranking functions (“rankfunc*”). Interestingly, after preprocessing we observe that 43 instances from the area of formal verification (“stmt*”) are uniquely solved.
To study the influence of treewidth on solving, we consider the 175
preprocessed instances that are not solved directly by Bloqqer. Since computing the
exact treewidth is infeasible, we use HTD [
PCNF’16. Results for the PCNF’16 data set are summarized in Table 3. The obtained data confirms that dynQBF is indeed sensitive to the number of quantifier blocks (k). For the original instances we measure an average k of 17, and 14.8 for instances solved by dynQBF. 75 instances have 2 (or less) quantifier blocks, of which dynQBF solves the most instances (55). Of the 391 instances with k = 3, dynQBF solves 142 instances, while the best solver here is GhostQ with 299 instances. Of the 359 instances with k > 3, dynQBF solves 168 instances, but GhostQ solves 256 instances. With preprocessing, 341 instances are solved by Bloqqer. Interestingly, all solvers except GhostQ benefit from preprocessing. Regarding the impact of quantifiers on the performance of dynQBF we obtain a similar picture as for the original instances. Overall, we again observe several instances uniquely solved by dynQBF.
As in the 2-QBF setting, we consider the width w of the preprocessed, nontrivial instances. Table 4 again shows that dynQBF performs well on instances where w ≤ 80: here, k is 4.9 for all instances on average, and 3.7 for instances solved by dynQBF. 6
In this paper we introduced an alternative approach for QBF solving. Our algorithm is inspired by concepts from parameterized complexity, yielding a new expansion-based solver technique that mitigates space explosion by dynamic programming over the TD and by using BDDs. First ideas for dependency scheme integration were presented, and we discussed entry points for heuristic optimizations of our technique. We conducted a thorough experimental analysis along the lines of QBFEval’16, which shows that our approach is already competitive for 2-QBF instances as well as on instances of width up to 80 (even for more quantifier blocks). Additionally, we showed that the behavior of our system is indeed different from the diverse field of existing techniques. Seen in a broader context, our results clearly demonstrate the potential of parameterized algorithms for problems beyond NP in practice, in particular when combined with BDDs. 10. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE
Transactions on Computers 100(8), 677–691 (1986) 11. Charwat, G., Woltran, S.: Dynamic programming-based QBF solving. In: Proc.
12. Chen, H.: Quantified constraint satisfaction and bounded treewidth. In: Proc.
ECAI. pp. 161–165. IOS Press (2004) 13. Dechter, R.: Constraint Processing. Morgan Kaufmann (2003) 14. Downey, R.G., Fellows, M.R.: Parameterized Complexity. Monographs in Computer Science, Springer (1999) 15. Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: Local vs. global. In:
Proc. LPAR. LNCS, vol. 3835, pp. 489–503. Springer (2005) 16. Friedman, S.J., Supowit, K.J.: Finding the optimal variable ordering for binary decision diagrams. In: Proc. DAC. pp. 348–356. ACM (1987) 17. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Proc. SAT. LNCS, vol. 7317, pp. 114–128.
18. Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Proc.
SAT. LNCS, vol. 6695, pp. 230–244. Springer (2011) 19. Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proc. IJCAI.
pp. 325–331. AAAI Press (2015) 20. Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based
9450, pp. 418–433. Springer (2015) 21. Lonsing, F., Biere, A.: A compact representation for syntactic dependencies in
QBFs. In: Proc. SAT. LNCS, vol. 5584, pp. 398–411. Springer (2009) 22. Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. J. SAT 7(2-3), 71–76 (2010) 23. Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: An empirical perspective on ten years of QBF solving. In: Proc. RCRA. CEUR Workshop Proceedings, vol. 1451, pp. 62–75. CEUR-WS.org (2015) 24. Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Proc. CP. LNCS, vol. 3258, pp. 453–467. Springer (2004) 25. Pulina, L.: The ninth QBF solvers evaluation - preliminary report. In: Proc. QBF.
26. Pulina, L., Tacchella, A.: A structural approach to reasoning with quantified
27. Pulina, L., Tacchella, A.: An empirical study of QBF encodings: From treewidth estimation to useful preprocessing. Fundam. Inform. 102(3-4), 391–427 (2010) 28. Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: Proc. FMCAD. pp.
136–143. IEEE (2015) 29. Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J. Comb.
Theory, Ser. B 36(1), 49–64 (1984) 30. Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom.
Reasoning 42(1), 77–97 (2009) 31. Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time.
In: Proc. SAT. LNCS, vol. 7317, pp. 58–71. Springer (2012) 32. Somenzi, F.: CU Decision Diagram package release 3.0.0. Department of Electrical and Computer Engineering, University of Colorado at Boulder (2015) 33. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Proc. TOC. pp. 1–9. ACM (1973)