In this paper we approach the problem of reasoning with quantified Boolean formulas (QBFs) by combining search and resolution, and by switching between them according to structural properties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolution alone, can be solved by combining them, and that our approach makes a proof-ofconcept implementation competitive with current QBF solvers.
The development of the first practically efficient QBF solver can be traced back
to [
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., [
1Induced width, as defined in [
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 [
While approaches similar to ours have been proposed for plain Boolean
satisfiability in [
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. 2
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 jlj the variable occurring in the literal l, and with l the complement of l, i.e., :l if l is a variable and jlj otherwise. A clause C is an n-ary (n 0) disjunction of literals such that, for any two distinct disjuncts l; l0 of C, it is not the case that jlj = jl0j. A propositional formula is a k-ary (k 0) conjunction of clauses. A quantified Boolean formula is an expression of the form
Q1z1 : : : Qnzn where, for each 1 i n, zi is a variable, Qi is either an existential quantifier Qi = 9 or a universal one Qi = 8, and is a propositional formula in the variables Z = fz1; : : : ; zng; the expression Q1z1 : : : Qnzn is the prefix and is the matrix; a literal l is existential if jlj = zi for some 1 i n and 9zi belongs to the prefix, and it is universal otherwise.
A prefix p = Q1z1 : : : Qnzn can be viewed as the concatenation of h quantifier blocks, i.e., p = Q1Z1 : : : QhZh, where the sets Zi 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 2 Zi. We also say that variable z comes after a variable z0 in p if lvl(z) lvl(z0).
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:
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 = fz1; : : : ; zng, its Gaifman graph has a vertex set equal to Z with an edge (z; z0) for every pair of different elements z; z0 2 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 z10; : : : ; zn0 of the elements of Z such that 1. the ordering z10; : : : ; zn0 preserves the order of p, i.e., if i < j then zj0 comes after zi0 in p, and 2. for any zk0, its lower numbered neighbors form a clique, that is, for all k, if i < k, j < k, (zi0; zk0) 2 E and (zj0 ; zk0) 2 E, then (zi0; zj0 ) 2 E.
The width wp(') of a scheme is the maximum, over all vertices zk, of the size of the set fi : i < k; (zi; zk) 2 Eg, i.e., the set containing all lower numbered neighbors of zk. The treewidth twp(') of a QBF ' is the minimum width over all schemes for '.
Clause resolution [
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 = fz1; : : : ; zng, we consider a scheme for ' and the associated elimination ordering Z0 = fz10; : : : ; zn0g. Starting from z = zn0 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 [
Unit propagation [
Backjumping is an optimization that can be added on top of search. According
to [
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.
2Case (1) will not apply unless terms are learned, and thus unit propagation may involve universal
variables as well – see [
UNDOELIMINATE(', l) else
UNDOASSIGN(', l) pop( ) if ISBOUND(q, l, ') then if m = LS then push( , hl; FL; NIL i) DOASSIGN(', l) return FALSE return TRUE
PROPAGATE(', ) hl; ri FINDUNIT(') while l 6= NIL do push( , hl; FL; ri) DOASSIGN(', l) hl; ri FINDUNIT(') BACKJUMP(', , q) wr INITREASON(', , q) while 6= EMPTY do hl; m; ri top( ) if m = VE then
UNDOELIMINATE(', l) else
UNDOASSIGN(', l) pop( ) if ISBOUND(q, l, ') then if OCCURS(jlj, wr) then if m = LS then push( , hl; FL; wri) DOASSIGN(', l) return FALSE else if m = FL then
UPDATEREASON(wr, r) return TRUE
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 [
FINDUNIT('), returns a pair hl; ri if l is a unit literal in ' and r is a unit clause in which l occurs, or a pair hNIL ; NIL i 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 jlj.
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 hu; m; ri 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 hl; FL; ri 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 = 9 if the current leaf is a conflict, and q = 8 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 = 9, 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 = 8, 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 STRUQS[BJ,VE](', ) stop FALSE while :stop do
PROPAGATE(', ) if ISTRUE(') then result TRUE stop BACKJUMP(', , 8) else if ISFALSE(') then result FALSE stop BACKJUMP(', , 9) else if PREFERSEARCH(') then SEARCH(', ) else ELIMINATE(', ) return result which is bound by the quantifier q and such that jlj occurs in the current working reason wr (OCCURS(jlj, wr)=TRUE). Also, when popping records hl; FL; ri 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 as follows. If PREFERSEARCH always returns TRUE, then we obtain the search solver STRUQS[BJ], and if it always returns FALSE, then we obtain the variable elimination solver STRUQS[VE]. Replacing BACKJUMP with BACKTRACK, we obtain STRUQS[BT,VE], and if we further assume that PREFERSEARCH always returns TRUE, then we obtain STRUQS[BT].
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 3The source code of STRUQS is available at http://www.mind-lab.it/projects. containing x in '. 2. If condition (1) is met for some x, then consider the number of clauses where x occurs, say nx, and the number of clauses where :x occurs, say n:x, and compute the diversity of x as the product nxn: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 nxn: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 jlj 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 jlj has the maximum degree among all the candidate literals of '.
We mention here that condition (1) is proposed in [
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 [
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 treewidth4 of the input formula as it is modified during
the solution process. The plots have been obtained by running various versions of
STRUQS on the instance test5 quant5 – family jmc quant, suite Katz in
the QBFEVAL’08 dataset. We consider test5 quant5 because it is the
smallest instance (358 variables, 941 clauses, 3 quantifier blocks) which is solved by
STRUQS[BJ,VE], and it is not solved by STRUQS[BJ] and STRUQS[VE].
Looking at Figure 3 (a), we can see that STRUQS[VE] (triangle dots) is able to decrease
slightly treewidth (from an initial estimate of 96 to a final estimate of 86), but it
can go as far as a few hundred steps before exhausting resources. On the other
hand, STRUQS[BJ] (circle dots) can decrease substantially treewidth, but it gets
trapped into structurally simpler subproblems, without managing to solve the input
QBF after about 9 106 steps, when it reaches the time limit.5 From Figure 3
(b) we can see that STRUQS[BJ,VE] changes its behavior according to the
current value of treewidth, i.e., PREFERSEARCH implicitly takes into account
structure. In the first 206 steps, only variable elimination is performed (triangle dots).
Then, as this approach becomes untenable, search (circle dots) is exploited to
obtain structurally simpler subproblems. Comparing the two plots, it is clear that
PREFERSEARCH prevents search to go “too deep”, because as soon as t^wp('i)
becomes small, PREFERSEARCH reckons that variable elimination alone can deal
with 'i. Overall, STRUQS[BJ,VE] solves test5 quant5 in less than 4 105
4More precisely, we consider an approximation of treewidth, computed as described in [
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 reveals that blended solvers are always superior to single ones. In more detail, STRUQS[BT] can solve 11% of the dataset, STRUQS[VE] can deal with 16% of it, and STRUQS[BJ] tops at 18%. Only 273 problems (8% of the dataset) are solved by both STRUQS[BT] and STRUQS[VE], which are incomparable. On the other hand, STRUQS[BJ] dominates STRUQS[BT] and it is incomparable with STRUQS[VE]. As for the blended versions, we see that STRUQS[BT,VE] is more efficient than all the single versions: It can solve 31% of the dataset, which is more than the set of problems solved by at least one of STRUQS[BT] and STRUQS[VE] (635). STRUQS[BJ,VE] turns out to be the most efficient among STRUQS versions: It can solve 39% of the dataset, which is also more than the set of problems solved by at least one of STRUQS[BJ] and STRUQS[VE] (800). If we normalize the number of search steps performed by the solvers considering the problems that are solved, we see a 10 gap between STRUQS[BT,VE] and STRUQS[BJ], while the same gap between STRUQS[BJ] and STRUQS[BT] is only 5 . This means that combining search and variable elimination turns to be efficient per se, and even more efficient than boosting search with backjumping. If we look at variable elimination steps, we can see a substantial increase in the normalized number of steps: nearly 300 (resp. 200 ) gap between STRUQS[VE] and STRUQS[BT,VE] (resp. STRUQS[BJ,VE]). Indeed, variable elimination is used more in STRUQS[BT,VE] and STRUQS[BJ,VE] than in STRUQS[VE], but this happens on subproblems that are structurally simpler, as there is only a 1:7 (resp. 2 ) gap in normalized CPU time between STRUQS[VE] and STRUQS[BT,VE] (resp. STRUQS[BJ,VE]). Notice also that STRUQS[BJ,VE] performs less search and variable elimination steps than STRUQS[BT,VE], and this appears to be the net effect of backjumping.
One last set of considerations about Table 1 regards dominance relationships. In particular, STRUQS[BT,VE] is incomparable with both STRUQS[BT] and STRUQS[VE]. In the case of STRUQS[BT], there are 6 problems in the suite Ansotegui which can be solved by STRUQS[BT], but not by STRUQS[BT,VE]. Indeed, the size of these problems is such that variable elimination becomes prohibitive too quickly for PREFERSEARCH to notice. STRUQS[VE] can solve 162 problems that STRUQS[BT,VE] cannot solve, where the bulk of such problems (121) is from the suite Pan: in these formulas, condition (1) of PREFERSEARCH is almost always unmet, and yet they turn out to be very difficult for search. Relaxing condition (1) of PREFERSEARCH can have positive effects on these formulas, but it can also severely degrade the performance of STRUQS[BT,VE] on other suites. STRUQS[BJ,VE] dominates STRUQS[BT,VE] and STRUQS[BT], but is incomparable with STRUQS[BJ] and STRUQS[VE]. In particular, there are 52 problems solved by STRUQS[BJ] that STRUQS[BJ,VE] cannot solve, whereof 40 are from the family blackbox-01X-QBF. These instances are characterized by the largest number of quantifier blocks among formulas in the dataset, and search is already quite efficient on them. STRUQS[VE] can solve 68 formulas on which STRUQS[BJ,VE] fails, of which 67 are from the suite Pan and have the same peculiarities mentioned about STRUQS[BT,VE].
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 [
STRUQS[BJ,VE]. If we consider that AQME is a multi-engine solver combining the ability of several engines (including QUBE6.1 and SKIZZO), and that both QUBE6.1 and SKIZZO are fairly sophisticated pieces of software, we can conclude that STRUQS[BJ,VE] performances are very satisfactory. Indeed, STRUQS is somewhat limited by the straigthforward implementation of operations such as, e.g., .forward subsumption. On one hand, disabling forward subsumption brings to 1114 the number of problems solved by STRUQS[BJ,VE]. On the other hand, forward subsumption accounts for 8% of the total time spent by STRUQS[BJ,VE] on the formulas that it can solve, but for 20% of the total time on the formulas that it cannot solve. Increasing the time limit to 1200 seconds allows STRUQS[BJ,VE] to solve about one hundred additional problems, indicating that the efficiency of basic operations is currently a limiting factor for STRUQS. 5
Summing up, the combination of search and resolution featured by STRUQS seems to offer a gateway to effective reasoning in QBFs. The two key results of our work are (i) showing that the blended solvers STRUQS[BT,VE] and STRUQS[BJ,VE] outperform the single ones, and (ii) showing that STRUQS[BJ,VE] is competitive with other state-of-the-art solvers. We believe that these results can be improved by pursuing an efficient implementation of STRUQS. The fact that STRUQS, however unsophisticated, is able to solve 24 problems that cannot be solved by other state-of-the-art QBF solvers is promising in this sense. Also, STRUQS[BJ,VE] used as a SAT solver on a subset of 790 QBFEVAL’08 formulas can solve 668 problems within one hour of CPU time and it is competitive with, e.g., MINISAT which can solve 787 of them, while STRUQS[BJ] and STRUQS[VE] top at 553 and 145 problems solved, respectively. Other improvements would be leveraging different structural features and approximations thereof, and/or integrating inductive techniques to synthesize (sub)instance-based PREFERSEARCH policies.