Q U BE: A system for deciding Quantified Boolean Formulas Satisfiability
Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella DIST, Universit`a di Genova, Viale Causa 13, 16145 Genova – Italy
1 Introduction
Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important re- search issue in Artificial Intelligence. Many reasoning tasks involving planning [1], abduction, reasoning about knowledge, non monotonic reasoning [2], can be directly mapped into the problem of deciding the satisfiability of a QBF.
In this paper we present QUBE, a system for deciding QBFs satisfiability. We start our presentation in 2 with some terminology and definitions necessary for the rest of the paper. In 3 we present a high level description of QUBE’s basic algorithm.
QUBE’s available options are described in 4. We end our presentation in 5 with some experimental results showing QUBE effectiveness in comparison with other sys- tems. QUBE, and more information about QUBE, are available at www.mrg.dist.
unige.it/star/qube.
2 Formal preliminaries
Consider a set P of propositional letters. Anatomis an element of P. Aliteralis an atom or the negation of an atom. For each literal , isif , and isif ;
is the atom occurring in . Aclauseis an-ary disjunction of literals such that no atom occurs twice in. Apropositional formulais a-ary conjunction of clauses. As customary, we represent a clause as a set of literals, and a propositional formula as a set of clauses.
AQBFis an expression of the form
½
½
(1)
where every
is a quantifier, either existentialor universal;½
are pairwise distinct atoms in P; and is a propositional formula in the atoms½
.
½
½
is theprefixand is the (quantifier-free)matrixof (1).
Consider a QBF of the form (1). A literal occurring in is:
– existentialifbelongs to the prefix of (1), and isuniversalotherwise.
– unitin (1) if is existential, and, for some,
a clause ½
belongs to , and
each expression
() is at the right ofin the prefix of (1).
We wish to thank Marco Cadoli, Rainer Feldmann, Theodor Lettman, Jussi Rintanen, Marco Schaerf and Stefan Schamberger for providing us with their systems and helping us to figure them out during our experimental analisys. This work has been partially supported by ASI and MURST.
1 = the input QBF; 2 Stack = the empty stack;
3 functionSimplify() 4 do
5 ¼= ;
6 if ( a contradictory clause is in ) 7 return FALSE;
8 if ( the matrix of is empty) 9 return TRUE;
10 if (is unit in )
11 =UNIT;Extend (); 12 if (is monotone in )
13 =PURE;Extend (); 14 while ( ¼!= );
15 return UNDEF;
16 functionBacktrack (res) 17 while ( Stack is not empty) 18 =Retract ();
19 if (( ==L-SPLIT) &&
20 ((res == FALSE&& ==) ||
21 (res == TRUE&& ==))) 22 =R-SPLIT; return;
23 return NULL;
24 functionQubeSolver() 25 do
26 res =Simplify();
27 if (res == UNDEF)=ChooseLiteral ();
28 else =Backtrack (res);
29 if (!= NULL) Extend ();
30 while (!= NULL);
31 return res; Fig. 1. The algorithm of QUBE.
– monotoneif either is existential, occurs in , and does not occur in ; or is universal, does not occur in , and occurs in .
A clauseiscontradictoryif no existential literal belongs to.
The semantics of a QBF can be defined recursively as follows. If contains a contradictory clause then is not satisfiable. If the matrix of is empty then is satisfiable. If is (resp. ), is satisfiable if and only if or (resp. and)
are satisfiable. If is a QBF and is a literal, is the QBF obtained from by deleting the clauses in which occurs, and removing from the others. It is easy to see that if is a QBF without universal quantifiers, the problem of deciding satisfiability reduces to propositional satisfiability (SAT).
Notice that we allow only for propositional formulas in conjunctive normal form (CNF) as matrices of QBFs. Indeed, by applying standard CNF transformations (see, e.g., [3]) it is always possible to rewrite a QBF into an equisatisfiable one satisfying our restrictions.
3 Q
UBE algorithm
QUBE is implemented in C on top of SIM, an efficient SAT decider developed by our group. A C-like high-level description of QUBE is shown in Figure 1. In this Figure,
– is a global variable initially set to the input QBF.
– Stack is a global variable storing the search stack, and is initially empty.
– ,, FALSE, TRUE, UNDEF, NULL,UNIT,PURE,L-SPLIT,R-SPLITare pairwise distinct constants.
– for each atom in , is a variable whose possible values areUNIT,
PURE,L-SPLIT,R-SPLIT, and isifis existential, andotherwise.
– Extend( ) first pushes and in the stack; then deletes the clauses of in which occurs, and removes from the others.
– Retract() pops the literal and corresponding QBF that are on top of the stack: the literal is returned, while the QBF is assigned to .
– Simplify() simplifies till a contradictory clause is generated (line 6), or the matrix of is empty (line 8), or no simplification is possible (lines 5, 14).
– ChooseLiteral() returns a literal occurring in such that for each atomoccurring to the left ofin the prefix of ,does not occur in , oris existential iff is existential.ChooseLiteral() also sets toL-SPLIT.
– Backtrack(res): pops all the literals and corresponding QBFs (line 18) from the stack, till a literal is reached such that isL-SPLIT(line 19), and either
is existential and res = FALSE(line 20); or is universal and res = TRUE
(line 21). If such a literal exists, is set to R-SPLIT, and is returned (line 22). If no such literal exists, NULLis returned (line 23).
QUBE returns TRUEif the input QBF is satisfiable, and FALSEotherwise. It is easy to see that QUBE, like other QBF procedures (see, e.g., [4–6]), is a generalization of the Davis, Logemann, Loveland procedure (DLL) for SAT: QUBE and DLL have the same behavior on QBFs without universal quantifiers.
4 Q
UBE options
Consider Figure 1. QUBE ver. 1.0 features backjumping, trivial truth, six different branching heuristics, i.e., implementations of ChooseLiteral, and other control options.
The backjumping procedure implemented in QUBE [7] is a generalization of the conflict-direct backjumping procedure as implemented in SAT solvers. As far as we know, QUBE is the only QBF solver with backjumping. Because of the potential over- head, backjumping has to be enabled when compiling the system, while all the other heuristics and optimizations can be enabled/disabled using QUBE’s command line.
QUBE’s command line is:
qube [-tt] [-heuristics unit|bohm|jw2] [-length exists|all]
[-verbose] [-timeout <n1>] [-memout <n2>] <file-name>.
By default, after the simplifications following the branch on an universal variable have been performed, QUBE checks whether the formula obtained from by deleting universal literals is satisfiable. If it is, then is satisfiable [4]. This optimization can produce dramatic speed-ups, particularly on randomly generated QBFs (see, e.g. [4]).
The option -tt disables this check. Notice that ours is an optimized version of “trivial truth” as described in [4], where the check is performed at each branching node.
QUBE branching heuristics have been inspired by the SAT literature. Our current version includes b¨ohm,jw2 and unit heuristics. The behavior of these heuristics de- pends on the notion of “length” of a clause. QUBE features two definitions of length of a clause: the number of literals in(-length all) as in [4, 5], and the number of existential literals in(-length exists) as in [6]. By combining these options, six different branching heuristics are possible.
The b¨ohmand jw2 heuristics are, respectively, a generalization of B¨ohm’s heuris- tic [8] and “two-sided Jeroslow-Wang” heuristic [9] for SAT. The idea behind b ¨ohm
and jw2 is to choose literals that occur as often as possible in the shortest clauses of . The hope is that by assigning such literals, we will have the largest amount of simplifi- cation. The unit heuristic is based on the one implemented inSATZ[10]. As opposed to b¨ohmand jw2, the unit heuristic tentatively assigns truth values to atoms in order to get the exact amount of simplification caused by such assignments.
Independently from the particular branching heuristic used, if the selected atomis existential (resp. universal), QUBE tries firstifhas more (resp. less) positive than negative occurrences in the matrix of . The idea is to maximize the chances of showing
satisfiability (resp. unsatisfiability) in the first branch.
The -verbose options enables printing search information during the execution, including the variablebeing assigned, its mode (whether is a unit, a pure, . . . ), and –in case it is aL-SPLIT– whetheroris tried first.
The -timeout <n1> and -memout <n2> options are used to limit the amount of resources used by QUBE. Whenever QUBE exceeds <n1> seconds of CPU time (resp. <n2> megs of RAM), its execution is halted.
5 Q
UBE performances
To evaluate QUBE performances, we compare it with DECIDE [5], EVALUATE [4], QKN [11], and QSOLVE[6]. According to our preliminary experimental results, the op- tions -heuristics bohm -length exists give good performances on all the problems, and are thus the default. The tests run on a Pentium III, 600MHz, 128MBRAM.
We consider sets of randomly generated QBFs. We generate QBFs according to model A as described in [12]. In this model, each QBF has the following 4 properties:
the prefix consists of sequences, each sequence has quantifiers, and any two quantifiers in a sequence, are of the same type, the rightmost quantifier is,
the matrix consists of clauses, each clause consists ofliterals of which at least 2 are existential. The Figure 2 shows the median, out of 100 samples, of the CPU times when , (left) and , (right). We fixed because it yields harder QBFs than (see [12]), and (on the-axis) is varied in such a way to cover the “100% satisfiable – 100% unsatisfiable” transition (shown in the background). Notice the logarithmic scale on the-axis.
Looking at Figure 2 (left) we immediatly see that QUBE and QSOLVE perform roughly the same (with QSOLVEbeing slightly better than QUBE) and better than all the other solvers that we tested. Still in Figure 2, forwe further observe that QUBE is always faster than QSOLVE, sometimes by orders of magnitude. Since QSOLVEruns trivial truth (and trivial falsity), but no backjumping, we take this as an evidence on the effectiveness of backjumping.
Our experimental analysis includes the 38 problems contributed by Rintanen in [5].
They are translations from planning problems into the language of QBFs and the best solver overall turns out to be DECIDE with 33 problems solved and 42.28s average running time (on solved samples), followed by QUBE, with 18 problems solved and 73.21s, and QSOLVEwith 11 problems solved and 149.29s. QKN and EVALUATEwith, respectively, 1 and 0 problems solved, trail the list. In this regard, we point out that
DECIDEfeatures “inversion of quantifiers” and “sampling” mechanisms which are par- ticularly effective on these benchmarks .
0 200 400 600 800 1000 1200 1400 1600 1800 2000 10−2
10−1 100 101 102 103
104 2 QBF − 5 CNF − 100 VARIABLES
NUMBER OF CLAUSES
CPU TIME [SEC]
Decide QKN Evaluate QuBE−BJ QSolve
% True
0 200 400 600 800 1000 1200 1400 1600 1800 2000
10−2 10−1 100
101 3 QBF − 5 CNF − 100 VARIABLES
NUMBER OF CLAUSES
CPU TIME [SEC]
QuBE−BJ QSolve
% True
Fig. 2. CPU times, median, 100 samples/point. Background: satisfiability percentage. Left:
, Right: ,
References
1. Jussi Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323–352, 1999.
2. U. Egly, T. Eiter, H. Tompits, and S. Woltran. Solving advanced reasoning tasks using quan- tified boolean formulas. In Proc. AAAI, 2000.
3. D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.
4. M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An algorithm to evaluate quan- tified boolean formulae and its experimental evaluation. Journal of Automated Reasoning, 2000. To appear. Reprinted in [13].
5. Jussi T. Rintanen. Improvements to the evaluation of quantified boolean formulae. In Dean Thomas, editor, Proceedings of the 16th International Joint Conference on Artificial Intelli- gence (IJCAI-99-Vol2), pages 1192–1197, S.F., July 31–August 6 1999. Morgan Kaufmann Publishers.
6. R. Feldmann, B. Monien, and S. Schamberger. A distributed algorithm to evaluate quantified boolean formulae. In Proc. AAAI, 2000.
7. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Backjumping for quanti- fied boolean logic satisfiability. In Proc. of the International Joint Conference on Artificial Intelligence (IJCAI’2001), 2001.
8. M. B¨ohm and E Speckenmeyer. A fast parallel SAT-solver – efficient workload balancing.
Annals of Mathematics and Artificial Intelligence, 17:381–400, 1996.
9. Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. An- nals of Mathematics and Artificial Intelligence, 1:167–187, 1990.
10. Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems.
In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI- 97), pages 366–371, San Francisco, August 23–29 1997. Morgan Kaufmann Publishers.
11. Kleine-B¨uning, H. and Karpinski, M. and Fl¨ogel, A. Resolution for quantified boolean for- mulas. Information and computation, 117(1):12–18, 1995.
12. Ian Gent and Toby Walsh. Beyond NP: the QSAT phase transition. In Proc. AAAI, pages 648–653, 1999.
13. Ian P. Gent, Hans Van Maaren, and Toby Walsh, editors. SAT2000. Highlights of Satisfiability Research in the Year 2000. IOS Press, 2000.
