The development of the first practically efficient QBF solver can be traced back to [4], wherein a search-based solver is proposed. Since then, researchers have proposed improvements to the basic search algorithm including, e.g., backjumping and learning [7], as well as different approaches to the problem including, e.g., skolemization [1], and resolution [2,12]. However, in spite of such efforts, current QBF reasoners still cannot handle many instances of practical interest. This is witnessed, e.g., by the results of the 2008 QBF solver competition (QBFEVAL'08) where even the most sophisticated solvers failed to decide encodings obtained from real-world applications [14].
In this work, we consider search and resolution for QBFs, and we propose a new approach that combines them dynamically. The key point of our approach is to implicitly leverage graph abstractions of QBFs to yield structural features which support the decision between search and resolution. As for the choice of a particular feature, it is known, see, e.g., [16], that resolution on plain Boolean formulas may require computational resources that are exponential in the treewidth. 1 This connection has been studied also for quantified formulas in [5,8,13]. In particular, in [5], an extension of treewidth is shown to be related to the efficiency of reasoning about quantified Boolean constraints, of which QBFs are a subclass. This result tells us that treewidth is a promising structural parameter to gauge resolution and search: Resolution is the choice when treewidth is relatively small, and search is the alternative when treewidth is relatively large. Switching between the two options may occur as long as search is able to obtain subproblems whose treewidth is smaller than the one of the original problem. In practice, QBFs of some interest for applications may have thousands of variables, and thus even approximations of treewidth -a well-known NP-complete problem -are too expensive to compute on-the-fly [15]. Also, while deciding if treewidth is bounded by a constant can be done in asymptotic linear time [3], an actual implementation of such algorithm would be too slow to be of practical use. In this paper we show how these issues can be overcome by considering alternative parameters indicating whether resolution is bound to increase the size of the initial set of clauses beyond "reasonable" limits. To this purpose, we compute estimates of the number of new clauses generated during resolution, and we require that the number of such clauses is less than the number of old clauses used to generate them. Also, we require that the expected number of clauses is less than a predefined threshold. Both these conditions can be checked without a prohibitive overhead, and respecting them can be as informative as tracking treewidth in many situations.
To test our approach, we implemented it in STRUQS (for "Stru"ctural "Q"BF "S"olver), a proof-of-concept tool consisting of less than 2K lines of C++ code. We have experimented with STRUQS on the QBFEVAL'08 dataset [14], which is comprised of more than three thousands QBF encodings in various application domains -the largest publicly available collection of QBFs to date. Here, we show that exploiting dynamic combination of search and resolution enables STRUQS to solve QBFs which, all other things being equal, cannot be solved by the search and resolution components of STRUQS alone. Moreover, STRUQS is competitive with respect to current QBF solvers, as it would have ranked third best among QBFEVAL'08 competitors if considering the number of problems solved within a given amount of resources.
While approaches similar to ours have been proposed for plain Boolean satisfiability in [16], and for non-quantified constraint satisfaction in [11], we notice that this is the first time that a structural approach combining search and resolution is designed, implemented and empirically tested for QBFs. Learning in search-based QBF solvers such as, e.g., QUBE [7] and YQUAFFLE [18], can also be seen as a way to integrate resolution and search. However, as shown in [7], this is true of a particular form of control strategy for general resolution known as tree resolution, while here we focus on variable elimination instead. Moreover, since STRUQS features backjumping, and backjumping is essentially space-bounded tree resolution, we could say that our work extends the above contributions in this sense. The solver 2CLSQ [17] is another example of integration between search and resolution. Also in this case, the contribution is limited to a specific form of resolution, namely hyper-binary resolution, which is seen as a useful complement to the standard unit clause resolution step performed by most search-based QBF solvers, and not as an alternative resolution-based decision procedure as we do in STRUQS. Also QUANTOR [2] provides some kind of integration between resolution and search, but with two fundamental differences with respect to STRUQS. The first one is that QUANTOR intertwines resolution with the expansion of univer-sally quantified variables, whereas in STRUQS no such expansion is performed. The second one is that QUANTOR uses search only at the very end of the decision process, when the input QBF has been reduced to an equi-satisfiable propositional formula.
The paper is structured as follows. In Section 2 we lay down the foundations of our work considering relevant definitions and known results. In Section 3 we define the basic STRUQS algorithms, including search, resolution and their combination. In Section 4 we describe our experiments and in Section 5 we summarize our current results and future research directions.
A variable is an element of a set P of propositional letters and a literal is a variable or the negation thereof. We denote with |l| the variable occurring in the literal l, and with l the complement of l, i.e., ¬l if l is a variable and |l| otherwise. A clause C is an n-ary (n ≥ 0) disjunction of literals such that, for any two distinct disjuncts l, l of C, it is not the case that |l| = |l |. A propositional formula is a k-ary (k ≥ 0) conjunction of clauses. A quantified Boolean formula is an expression of the form
where, for each 1 ≤ i ≤ n, z i is a variable, Q i is either an existential quantifier Q i = ∃ or a universal one Q i = ∀, and Φ is a propositional formula in the variables Z = {z 1 , . . . , z n }; the expression Q 1 z 1 . . . Q n z n is the prefix and Φ is the matrix; a literal l is existential if |l| = z i for some 1 ≤ i ≤ n and ∃z i belongs to the prefix, and it is universal otherwise.
A prefix p = Q 1 z 1 . . . Q n z n can be viewed as the concatenation of h quantifier blocks, i.e., p = Q 1 Z 1 . . . Q h Z h , where the sets Z i with 1 ≤ i ≤ h are a partition of Z, and consecutive blocks have different quantifiers. To each variable z we can associate a level lvl(z) which is the index of the corresponding block, i.e., lvl(z) = i for all the variables z ∈ Z i . We also say that variable z comes after a variable z in p if lvl(z) ≥ lvl(z ).
The semantics of a QBF ϕ can be defined recursively as follows. A QBF clause is contradictory exactly when it does not contain existential literals. If ϕ contains a contradictory clause then ϕ is false. If ϕ has no conjuncts then ϕ is true. If ϕ = Qzψ is a QBF and l is a literal, we define ϕ l as the QBF obtained from ψ by removing all the conjuncts in which l occurs and removing l from the others. Then we have two cases:
• If ϕ is ∃zψ, then ϕ is true exactly when ϕ z or ϕ ¬z are true.
• If ϕ is ∀zψ, then ϕ is true exactly when ϕ z and ϕ ¬z are true.
The QBF decision problem (QSAT) can be stated as the problem of deciding whether a given QBF is true or false.
Given a QBF ϕ on the set of variables Z = {z 1 , . . . , z n }, its Gaifman graph has a vertex set equal to Z with an edge (z, z ) for every pair of different elements z, z ∈ Z that occur together in some clause of ϕ. A scheme for a QBF ϕ having prefix p is a supergraph (Z, E) of the Gaifman graph of ϕ along with and ordering z 1 , . . . , z n of the elements of Z such that 1. the ordering z 1 , . . . , z n preserves the order of p, i.e., if i < j then z j comes after z i in p, and 2. for any z k , its lower numbered neighbors form a clique, that is, for all k,
The width w p (ϕ) of a scheme is the maximum, over all vertices z k , of the size of the set {i : i < k, (z i , z k ) ∈ E}, i.e., the set containing all lower numbered neighbors of z k . The treewidth tw p (ϕ) of a QBF ϕ is the minimum width over all schemes for ϕ.
Clause resolution [10] for a QBF ϕ is an operation whereby given two clauses Q ∨ x and R ∨ ¬x of ϕ, the clause min(Q ∨ R) can be derived, where
x is an existential variable, 3. Q and R do not share any literal l such that l occurs in Q and l occurs in R, and 4. min(C) is obtained from C by removing the universal literals coming after all the existential literals in C.
Variable elimination is a control strategy for resolution defined as follows. Given a QBF ϕ on the set of variables Z = {z 1 , . . . , z n }, we consider a scheme for ϕ and the associated elimination ordering Z = {z 1 , . . . , z n }. Starting from z = z n and scanning the elimination ordering in reverse, we eliminate the variables as follows. If z is existential, and assuming that ϕ contains k > 0 clauses in the form Q ∨ z and h > 0 clauses in the form R ∨ ¬z, then we add O(kh) clauses to ϕ obtained by performing all the resolutions on z. In the case where either k = 0 or h = 0, no operation is performed. If z is universal, we simply skip to the next variable. If all the variables in ϕ can be eliminated without generating a contradictory clause, then ϕ is true, else it is false.
Backtracking search [4] for a QBF ϕ is a depth-first exploration of an AND-OR tree defined as follows. Initially, the current QBF is ϕ. If the current QBF is of the form ∃xψ then we create an OR-node, whose children are obtained by checking recursively whether ϕ x is true or ϕ ¬x is true. If the current QBF is of the form ∀yψ then we create an AND-node, whose children are obtained by checking recursively whether both ϕ y and ϕ ¬y are true. We call ϕ l a branch (also, an assignment), and since we explore the tree in a depth-first fashion, a node wherein only the first branch was taken is said to be open, and closed otherwise. The leaves are of two kinds: If the current QBF contains a contradictory clause we have a conflict, while if the current QBF contains no conjuncts we have a solution. Backtracking from a conflict amounts to reaching back to the deepest open OR-node: if there is no such node, then ϕ is false; backtracking from a solution amounts to reaching back to the deepest open AND-node: if there is no such node, then ϕ is true.
Unit propagation [4] is an optimization that can be added on top of basic variable elimination and search. A clause C is unit in a QBF ϕ exactly when (i) C contains only one existential literal l (unit literal) and, (ii) all the universal literals in C come after l in the prefix of ϕ. If ϕ contains a unit literal l, then ϕ is true if and only if ϕ l is true. Unit propagation is the process whereby we keep assigning unit literals until no more such literals can be found.
Backjumping is an optimization that can be added on top of search. According to [7] the computation performed by a QBF search algorithm corresponds to a particular kind of deductive proof, i.e., a tree wherein clause resolution and term resolution alternate, where a term is a conjunction of literals, and term resolution is the "symmetric" operation of clause resolution -see [7] for details. The clause/term tree resolution proof corresponding to search for a QBF ϕ can be reconstructed as follows. In case of a conflict, there must be two clauses, say Q ∨ x and R ∨ ¬x such that all the literals in Q and R have been deleted by previous assignments. We can always resolve such clauses to obtain the working reason min(Q ∨ R)where Q ∨ x and R ∨ ¬x are the initial working reasons. The other clauses can be derived from the working reason when backtracking over any existential literal l such that |l| occurs in the working reason. There are three cases:
1. If l is a unit literal, then there is a clause C where l occurs -the reason of assigning l -and we obtain a new working reason by resolving the current one with C.
l is an open branch, then proof reconstruction stops, because we must branch on l, and the reason of this assignment is the current working reason.
3. If l is a closed branch, then its reason was computed before, and it can be treated as in (1).
In case of a solution, the initial working reason is a term which is the conjunction of (a subset of) all the literals assigned from the root of the search tree, down to the current leaf, i.e., a Boolean implicant of the matrix of ϕ. The other terms can be derived when backtracking over any universal literal l such that l is in the working reason, considering cases (ii) and (iii) above, and using term instead of clause resolution. 2 Given the above, it is easy to see that closing branches over existential (resp. universal) literals that do not appear in the current working reason is useless, i.e., they are not responsible for the current conflict (resp. solution). Backjumping can thus be described as the process whereby useless branches are skipped while backtracking.
SEARCH(ϕ, Γ) l ← CHOOSELIT(ϕ, Γ) push(Γ, l, LS, NIL ) DOASSIGN(ϕ, l)
In Figure 1 we present STRUQS basic routines in pseudo-code format. All the routines take as by-reference parameters the data structure ϕ which encodes the input QBF, and a stack Γ which keeps track of the steps performed. We consider the following primitives for ϕ:
• DOASSIGN(ϕ, l) implements ϕ l as per Section 2, where clauses and literals are disabled rather than deleted.
• DOELIMINATE(ϕ, v) implements the elimination of a single variable as described in Section 2, with the addition that clauses subsumed by some clause already in ϕ are not added -a process named forward subsumption in [2]; as in the case of DOASSIGN, the eliminated variables and the clauses where they occur are disabled.
• FINDUNIT(ϕ), returns a pair l, r if l is a unit literal in ϕ and r is a unit clause in which l occurs, or a pair NIL , NIL if no such literal exists in ϕ.
• CHOOSELIT(ϕ, Γ) returns a literal l subject to the constraint that all the remaining variables of ϕ which do not appear in Γ come after |l|.
• CHOOSEVAR(ϕ, Γ) returns a variable v subject to the constraint that v comes after all the remaining variables of ϕ which do not appear in Γ.
Because updates in DOASSIGN and DOELIMINATE are not destructive, we can further assume that their effects can by "undo" functions, i.e., UNDOASSIGN and UNDOELIMINATE.
The routines SEARCH and ELIMINATE (Figure 1, top-left) perform one step of search and variable elimination, respectively. SEARCH (resp. ELIMINATE), asks CHOOSELIT (resp. CHOOSEVAR) for a literal l (resp. a variable v) and then it (i) pushes l (resp. v) in the stack and (ii) it updates ϕ. In both cases step (i) amounts to push a triple u, m, r in Γ where r is always NIL , u is the literal being assigned or the variable being eliminated, and m is the mode of the assignment, where LS ("L"eft "S"plit) indicates an open branch in the search tree, and VE ("V"ariable "E"limination) indicates the corresponding resolution step. The task of PROPAGATE (Figure 1, top-right) is to perform unit propagation in ϕ. For each unit literal l, PROPAGATE pushes a record l, FL, r in Γ, where l and r are the results of FINDUNIT, and the mode is always FL ("F"orced "L"iteral).
BACKTRACK (Figure 1 bottom-left) and BACKJUMP (Figure 1, bottom-right) are alternative backtracking procedures to be invoked at the leaves of the search tree with an additional parameter q, where q = ∃ if the current leaf is a conflict, and q = ∀ otherwise. BACKTRACK goes back in the stack Γ, popping records for search (LS) or deduction steps (VE, FL), and undoing the corresponding effects on ϕ. Notice that, if BACKTRACK is a component of a plain search solver, then VE-type records will not show up in Γ. BACKTRACK stops when an open branch (LS) corresponding to a literal l bound by the quantifier q is found (ISBOUND(q, l, ϕ)=TRUE). In this case, BACKTRACK closes the branch by assigning l with mode FL and returning FALSE to indicate that search should not stop. On the other hand, if all the records are popped from Γ without finding an open branch then search is over and BACKTRACK returns TRUE.
BACKJUMP implements backjumping as per Section 2 on top of the following primitives:
• INITREASON(ϕ, Γ, q) initializes the working reason wr. If q = ∃, then we have two cases: (i) If top(Γ) is a FL-type record, then wr is any clause in ϕ which is contradictory because all of its existential literals have been disabled. (ii) If top(Γ) is a VE-type record, this means that a contradictory clause C has been derived when eliminating a variable, and thus wr is C. If q = ∀, then wr is a term obtained considering a subset of the literals in Γ such that the number of universal literals in the term is minimized -VE-type records are disregarded in this process.
• UPDATEREASON(wr, r) updates wr by resolving it with r, i.e., the reason of the assignment which is being undone.
When BACKJUMP is invoked in lieu of BACKTRACK, it first initializes the working reason, and then it pops records from Γ until either the stack is empty, or some open branch is found -the return values in these cases are the same as BACKTRACK.
BACKJUMP stops at open branches (LS) only if they correspond to some literal l which is bound by the quantifier q and such that |l| occurs in the current working reason wr (OCCURS(|l|, wr)=TRUE). Also, when popping records l, FL, r such that l occurs in the working reason, the procedure UPDATEREASON is invoked to update the current working reason wr. As described in Section 2, all the literals bound by q that are not in the current working reason are irrelevant to the current conflict/solution and are simply popped from Γ without further ado.
On top of the basic algorithms of Figure 1, we define five different versions of STRUQS: Three "single" versions, namely STRUQS[BJ], STRUQS[BT], and STRUQS[VE], and two "blended" ones, namely STRUQS[BT,VE] and STRUQS[BJ,VE]. The single solvers implement basic reasoning algorithms and are provided for reference purposes, while the blended ones implement our structural approach. 3 The pseudo-code of STRUQS[BJ,VE] is detailed in Figure 2 where we consider some additional primitives on ϕ: ISTRUE(ϕ) returns TRUE exactly when all clauses in ϕ have been disabled; ISFALSE(ϕ) returns TRUE exactly when there is at least one contradictory clause in ϕ; finally, PREFERSEARCH(ϕ) is some heuristic to choose between search and variable elimination. The other versions of STRUQS can be obtained from the code in Figure 2 We now consider the implementation of PREFERSEARCH for the blended versions of STRUQS. As discussed in Section 1, PREFERSEARCH needs to be based on parameters which are informative, yet computable without a prohibitive overhead. To this end, in PREFERSEARCH we resort to the following criteria:
1. Given the current ϕ and Γ, check if there is any existential variable x which respects CHOOSEVAR's constraints, and such that the number of clauses potentially generated by DOELIMINATE(ϕ, x) is less than the number of clauses containing x in ϕ. 1) is met for some x, then consider the number of clauses where x occurs, say n x , and the number of clauses where ¬x occurs, say n ¬x , and compute the diversity of x as the product n x n ¬x ; check if the diversity of x is less than a predefined threshold div.
Notice that, when checking for conditions (1) we compute an upper bound on the number of clauses generated as n x n ¬x , and we stop checking when the first variable respecting both conditions is found. If both conditions above are met for some x, then PREFERSEARCH returns FALSE, and CHOOSEVAR is instructed to return x. If either condition is not met, then PREFERSEARCH returns TRUE. In this case, CHOOSELIT tries to pick a literal l which respects CHOOSELIT's constraints, and such that |l| is a node in the neighborhood of some variable x tested during the last call to PREFERSEARCH. If no such literal can be found, then CHOOSELIT returns a literal l such that |l| has the maximum degree among all the candidate literals of ϕ.
We mention here that condition (1) is proposed in [6] to control variable elimination during preprocessing of plain Boolean encodings, and diversity is introduced in [16] to efficiently account for structure of Boolean formulas. Intuitively, in our implementation condition (1) provides the main feedback that implicitly considers the treewidth of the current formula: If variable elimination becomes less efficient, then this means that the structure of the current QBF is probably less amenable to this kind of approach. Condition (2) fine tunes (1): Whenever some variable x meets condition (1), but n x n ¬x is too large, eliminating x could be overwhelmingly slow. Finally, the search heuristic in CHOOSELIT is modified in order to use search for breaking large clusters of tightly connected variables. If this cannot be done, then CHOOSELIT falls back to assigning the variable which is most constrained.
4 Putting the structural approach to the test All the experimental results that we present are obtained on a family of identical Linux workstations comprised of 10 Intel Core 2 Duo 2.13 GHz PCs with 4GB of RAM. The resources granted to the solvers are always 600s of CPU time and 3GB of memory. To compare the solvers we use the QBFEVAL'08 dataset, which is comprised of 3326 formulas divided into 17 suites and 71 families (suites may be comprised of more than one family). All the formulas considered are QBF encodings of some automated reasoning task [14]. In the following, we say that solver A dominates solver B whenever the set of problems solved by A is a superset of the problems solved by B; we say that two solvers are incomparable when neither one dominates the other.
Our first experiment aims to provide an empirical explanation on why alternating between search and resolution can be effective. In Figure 3 (a,b) we present two plots showing the connection between the behaviour of STRUQS -as dictated by PREFERSEARCH -and the treewidth 4 of the input formula as it is modified during the solution process. steps, of which about 25% are search steps. Another interesting phenomenon is that even when search is prevailing -for t w p (ϕ) values roughly in between 75 and 25 -PREFERSEARCH still gives a chance to variable elimination. In these cases, variable elimination plays essentially the same role of unit propagation, i.e., it stops in advance the exploration of irrelevant portions of the search space.
In the above experiment, PREFERSEARCH turns out to be effective in switching between variable elimination and search with a specific value of the threshold div (2000). Since different values of div influence the behaviour of PREFERSEARCH, it is reasonable to ask how much a particular setting of div will influence the performance of STRUQS, if at all, and which is the best setting, at least in the dataset that we consider. In figure 3 (c) we present the result of running STRUQS[BJ,VE] with various settings of the parameter div on the formulas in the QBFEVAL'08 dataset which cannot be solved by either STRUQS[VE] or STRUQS[BJ] alone (660 formulas). In particular, we consider an initial value div = 125 and we increase it by a ×2 factor until div = 16000, each time running STRUQS[BJ,VE] on the above dataset. The plot in Figure 3 clearly shows that (i) div ≈ 2000 appears to be the best setting in the QBFEVAL'08 dataset, and that (ii) only 15 instances separate the performance of the best STRUQS[BJ,VE] setting (div = 2000) with respect to the worst one (div = 125). In all the experiments that we show hereafter div is fixed to 2000, but we conjecture that while tuning div helps in making STRUQS faster in some cases, relatively small changes in the number of problems solved are to be expected.
As we anticipated, there is a number of instances that can be solved by STRUQS[BJ,VE], but cannot be solved by the corresponding single solvers. Our next experiment is to compare all STRUQS versions to see whether blended solvers have an edge over single ones. Indeed, a quick glance at the results shown in Table 1 In Table 2 we conclude this section by comparing STRUQS[BJ,VE] with stateof-the-art QBF solvers. We have considered all the competitors of QBFEVAL'08, namely AQME, QUBE6.1, NENOFEX, QUANTOR, and SSOLVE. To them, we have added the solvers SKIZZO [1] which is representative of skolemization-based approaches, QUBE3.0 [7] which is the same as QUBE6.1 but without preprocessing, YQUAFFLE [18] and 2CLSQ [17] which are also search-based solvers, and QM-RES [12] which features symbolic variable elimination. Although STRUQS[BJ,VE] is just a proof-of-concept solver, Table 2 reveals that it would have ranked third best considering only the participants to QBFEVAL'08, and it ranks as fourth best in Table 2. Moreover, there are 24 instances that can be solved only by