Backjumping for Quantified Boolean Logic Satisfiability

1 Introduction

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many reasoning tasks involving abduction, reasoning about knowledge, non monotonic reasoning, are PSPACE-complete reasoning problems and are reducible in polynomial time to the problem of determining the satisfaction of a QBF. More important, since QBF reasoning is the prototypical PSPACE problem, many of these reductions are readily available. For these reasons, we have seen in the last few years the presentation of several implemented decision procedures for QBFs, like QKN [Kleine-B¨uning, H. and Karpinski, M. and Fl¨ogel, A., 1995], EVALUATE [Cadoli et al., 1998, Cadoli et al., 2000], DECIDE [Rintanen, 1999b], QUIP [Egly et al., 2000], QSOLVE [Feldmann et al., 2000]. Most of the above decision procedures are based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability [Davis et al., 1962] (SAT). This is because it is rather easy to extend DLL to deal with QBFs, and also because DLL is at the core of many state-of-the-art deciders for SAT.

In this paper we show how it is possible to extend the conflict-directed backjumping schema for SAT (see, e.g., [Prosser, 1993, Bayardo, Jr. and Schrag, 1997]) to QBF: when applicable, it allows to jump over existentially quantified literals while backtracking. We introduce solutiondirected backjumping, which allows the same for universally quantified literals. Then, we show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for QBF satisfiability. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained. While there have been several proposals for backjumping in SAT, this is the first time -as far as we know- this idea has been proposed, implemented and experimented for QBFs.

The paper is structured as follows. In Section 2 we introduce some formal preliminaries necessary for the rest of the paper. In Section 3 we present QUBE, a DLL based decision procedure for QBFs. Section 4 is devoted to the presentation of the theoretical results at the basis of the backjumping procedure presented in Section 5. The experimental analysis is reported in Section 6. We end the paper with the conclusions and future work in Section 7. Proofs are omitted for lack of space.

2 Formal preliminaries

Consider a set P of propositional letters. An atom is an element of P. A literal is an atom or the negation of an atom. In the following, for any literal D0,

• AF CYD0CY is the atom occurring in D0; and
• AF D0 is BMD0 if D0 is an atom, and is CYD0CY otherwise.

A clause BV is an D2-ary B4D2 AL BCB5 disjunction of literals such that, for any two distinct disjuncts D0BN D0 BC in BV, it is not the case that CYD0CY BP CYD0 BC CY. A propositional formula is a CZ-ary B4CZ AL BCB5 conjunction of clauses. As customary in SAT, we represent a clause as a set of literals, and a propositional formula as a set of clauses. With this notation, e.g.,

• AF the clause CUCV is the empty clause and stands for the empty disjunction,
• AF the propositional formula CUCV is the empty set of clauses and stands for the empty conjunction,
• AF the propositional formula CUCUCVCV stands for the set of clauses whose only element is the empty clause.

A QBF is an expression of the form

where

• AF every CX B4BD AK CX AK D2B5 is a quantifier, either existential BL or universal BK,
• AF DC BD BN BM BM BM BN DC D2 are pairwise distinct atoms in P, and
• AF A8 is a propositional formula in the atoms DC BD BN BM BM BM BN DC D2 .

BD DC BD BM BM BM D2 DC D2 is the prefix and A8 is the matrix of (1). 1 For example, the expression

is a QBF with 7 clauses.

Consider a QBF (1). A literal D0 is

• AF existential if BLCYD0CY belongs to the prefix of (1), and is universal otherwise.
• AF unit in (1) if D0 is existential, and, for some D1AL BC,
• a clause CUD0BN D0 BD BN BM BM BM BN D0 D1 CV belongs to A8, and
• each expression BKCYD0 CX CY (BD AK CX AK D1) occurs at the right of BLCYD0CY in the prefix of (1).
• AF monotone if either D0 is existential, D0 occurs in A8, and D0 does not occur in A8; or D0 is universal, D0 does not occur in A8, and D0 occurs in A8.

A clause BV is contradictory if no existential literal belongs to BV. For example, the empty clause is contradictory.

The semantics of a QBF B3 can be defined recursively as follows. If B3 contains a contradictory clause then B3 is FALSE. If the matrix of B3 is the empty set of clauses then B3 is TRUE. If B3 is BLDCAW (respectively BKDCAW), B3 is TRUE if and only if B3 DC or (respectively and) B3 BMDC are TRUE. If B3 BP DCAW is a QBF and D0 is a literal, B3 D0 is the QBF obtained from AW by deleting the clauses in which D0 occurs, and removing D0 from the others. It is easy to see that if B3 is a QBF without universal quantifiers, the problem of deciding B3 satisfiability reduces to SAT.

3 QUBE

QUBE is implemented in C on top of SIM, an efficient decider for SAT developed by our group [Giunchiglia et al., 2001a]. A high-level description of QUBE is presented in Figure 1. 2 In Figure 1,

• AF B3 is a global variable initially set to the input QBF.

1 Traditionally, the syntax of QBFs allows for arbitrary propositional formulas as matrices. However, the problem of determining the satisfiability of a QBF whose matrix is a set of clauses remains

1 B3 := CWthe input QBFCX; Stack:= CWthe empty stackCX; 2 function Simplify() 3 do 4 B3 BC := B3; 5 if (CWa contradictory clause is in B3CX) return FALSE; 6 if (CWthe matrix of B3 is emptyCX) return TRUE; 7 if (CWD0 is unit in B3CX) 8 CYD0CYBMD1D3CSCT := UNIT; Extend(D0); 9 if (CWD0 is monotone in B3CX) 10 CYD0CYBMD1D3CSCT := PURE; Extend(D0); 11 while (B3 BC BIBP B3); 12 return UNDEF; 13 function Backtrack(res) 14 while (CWStack is not emptyCX) 15 D0 := Retract(); 16 if (CYD0CYBMD1D3CSCT = L-SPLIT) and 17 ((res = FALSE and CYD0CYBMD8DDD4CT = BL) or 18 (res = TRUE and CYD0CYBMD8DDD4CT = BK)) 19 CYD0CYBMD1D3CSCT := R-SPLIT; return D0; 20 return NULL; 21 function QubeSolver() 22 do 23 res := Simplify(); 24 if (res = UNDEF) D0 := ChooseLiteral(); 25 else D0 := Backtrack(res); 26 if (D0 BIBP NULL) Extend(D0); 27 while (D0 BIBP NULL); 28 return res;

• AF Stack is a global variable storing the search stack, and is initially empty.
• AF FALSE, TRUE, UNDEF, NULL, UNIT, PURE, L-SPLIT, R-SPLIT are pairwise distinct constants.
• AF for each atom DC in the input QBF,
• DCBMD1D3CSCT is a property of DC whose possible values are UNIT, PURE, L-SPLIT, R-SPLIT, and have the obvious meaning, and
• DCBMD8DDD4CT is BL if DC is existential, and BK otherwise.
• AF Extend(D0) deletes the clauses of B3 in which D0 occurs, and removes D0 from the others. Additionally, before performing the above operations, pushes D0 and B3 in the stack.
• AF Retract() pops the literal and corresponding QBF that are on top of the stack: the literal is returned, while the QBF is assigned to B3. (Intuitively, Retract is the "inverse" operation of Extend ).
• AF Simplify() simplifies B3 till a contradictory clause is generated (line 5), or the matrix of B3 is empty (line 6),

PSPACE complete.

2 We use the following pseudocode conventions. Indentation indicates block structure. Two instructions on the same line belong to the same block.":=" is the assignment operator. The constructs while CWcondCX CWblockCX, do CWblockCX while CWcondCX, ifCWcondCX CWblock BD CX else CWblock BE CX have the same interpretation as in the C language.

or no simplification is possible (lines 4, 11). The simplifications performed in lines 8 and 10 correspond to Lemmas 6, 4-5 respectively of [Cadoli et al., 1998, Cadoli et al., 2000].

• AF ChooseLiteral() returns a literal D0 occurring in B3 such that for each atom DC occurring to the left of CYD0CY in the prefix of the input QBF,
• DC and BMDC do not occur in B3, or
• DC is existential iff D0 is existential.

ChooseLiteral () also sets CYD0CYBMD1D3CSCT to L-SPLIT.

• AF Backtrack(res): pops all the literals and corresponding QBFs (line 15) from the stack, till a literal D0 is reached such that CYD0CYBMD1D3CSCT is L-SPLIT (line 16), and either
• D0 is existential and res = FALSE (line 17); or
• D0 is universal and res = TRUE (line 18).

If such a literal D0 exists, CYD0CYBMD1D3CSCT is set to R-SPLIT, and D0 is returned (line 19). If no such literal exists, NULL is returned (line 20).

It is easy to see that QUBE is a generalization of DLL: QUBE and DLL have the same behavior on QBFs without universal quantifiers.

To understand QUBE behavior, consider the QBF (2). For simplicity, assume that ChooseLiteral returns the negation of the first atom in the prefix which occurs in the matrix of the QBF under consideration. Then, the tree searched by QUBE when B3 is (2) is represented in Figure 2. In Figure 2, each node shows

• AF the sequence of literals assigned by QUBE before a branch takes place (first line): for each literal D0 in the sequence, we also show the value of CYD0CYBMD1D3CSCT; and
• AF the matrix of the resulting QBF, prefixed by a label (second line).

As the result of the computation, QUBE would correctly return FALSE, i.e., (2) is unsatisfiable.

4 Backjumping

Let B3 be a QBF (1). Consider B3.

In the following, for any finite sequence AM BP D0 BD BN BM BM BM BN D0 D1 B4D1 AL BCB5 of literals, we write

• AF AssignB4AMBN A8B5 as an abbreviation for

where, if A9 is a set of clauses, AssignB4D0BNA9B5 is the set of clauses obtained from A9 by deleting the clauses in which D0 occurs, and removing D0 from the others.

• AF CJ BD DC BD BM BM BM D2 DC D2 CL AM as an abbreviation for the expression obtained from BD DC BD BM BM BM D2 DC D2 by removing CX DC CX whenever DC CX or BMDC CX is in AM.
• AF B3 AM as an abbreviation for the QBF

Intuitively, if AM is a sequence of literals representing an assignment, B3 AM is the QBF resulting after the literals in AM are assigned. For example, considering Figure 2, if B3 is (2), A8 is (BYBG), and AM is BMDC BD BN DC BF , then B3 AM is BLDC BE BLDC BG BLDC BH A8.

As in constraint satisfaction (see, e.g., [Dechter, 1990, Prosser, 1993, Bayardo, Jr. and Schrag, 1997]) it may be the case that only a subset of the literals in the current assignment is responsible for the result (either TRUE or FALSE) of B3 AM satisfiability. Then, assuming that it is possible to effectively determine such a subset AN, we could avoid doing a right branch on a literal D0, if D0 is not in AN. To make these notions precise we need the following definitions.

A finite sequence AM BP D0 BD BN BM BM BM BN D0 D1 B4D1 AL BCB5 of literals is an assignment for B3 if for each literal D0 CX in AM

• AF D0 CX is unit, or monotone in B3 D0 BD BNBMBMBMBND0 CXA0BD ; or
• AF D0 CX occurs in B3 D0 BD BNBMBMBMBND0 CXA0BD and for each atom DC occurring to the left of CYD0 CX CY in the prefix of the input QBF,
• A0 DC and BMDC do not occur in B3 D0 BD BNBMBMBMBND0 CXA0BD , or
• A0 DC is existential iff D0 CX is existential.

Consider an assignment AM BP D0 BD BN BM BM BM BN D0 D1 for B3.

A set of literals AN is a reason for B3 AM result if

• AF AN AI CUD0 BD BN BM BM BM BN D0 D1 CV, and
• AF for any assignment AM BC for B3 such that

• CUCYD0CY BM D0 is in AM BC CV BP CUCYD0CY BM D0 is in AMCV,

B3 AM BC is satisfiable iff B3 AM is satisfiable.

For example, if B3 is (2),

• AF if AM is DC BD BN BMDC BE , then CUDC BD CV is a reason for B3 AM result: For each assignment AM BC BE CUDC BD BN BMDC BE BN DC BD BN DC BE CV, B3 AM BC is unsatisfiable, and
• AF if AM is BMDC BD BN BMDC BF , then CUBMDC BD CV is a reason for B3 AM result: For each assignment AM BC BE CUBMDC BD BN BMDC BF BN BMDC BD BN DC BF CV, B3 AM BC is satisfiable.

Intuitively,

• AF when given an assignment AM such that either the matrix B3 AM is empty or it contains a contradictory clause, we first compute a reason AN for B3 AM result, and
• AF while backtracking, we dynamically modify the reason AN for the current result. Furthermore, we use AN in order to avoid useless branches: In particular, we avoid doing a right branch on a literal D0 if D0 is not in AN.

The theorems in the next subsections -in which we show how to compute the reason- are an easy consequence of the following proposition.

Let AN be a reason for B3 AM result. We say that

• AF AN is a reason for B3 AM satisfiability if B3 AM is satisfiable, and
• AF AN is a reason for B3 AM unsatisfiability, otherwise.

Proposition 1 Let B3 be a QBF (1). Let AM BP D0 BD BN BM BM BM BN D0 D1 B4D1 AL BCB5 be an assignment for B3. Let AM BC be a sequence obtained by removing some of the literals in AM. Let AN be the set of literals in AM BC .

Figure 2: QUBE computation tree for (2). U, P, L, R stand for UNIT, PURE, L-SPLIT, R-SPLIT respectively. The prefix is BKDC BD BLDC BE BKDC BF BLDC BG BLDC BH .

4.1 Conflict-directed Backjumping

The following Theorem allows us to compute the reason for B3 AM result when the matrix of B3 AM contains a contradictory clause. Given a sequence of literals AM, we say that a literal D0 is FALSE-irrelevant in AM if -assuming AM BC is the sequence obtained by deleting D0 in AM- B3 AM BC contains a contradictory clause.

Theorem 1 Let B3 be a QBF. Let AM be an assignment for B3 such that B3 AM contains a contradictory clause. Let AM BC be a sequence obtained by recursively eliminating a FALSEirrelevant literal in AM. Let AN be the set of literals in AM BC . Then AN is a reason for B3 AM unsatisfiability.

If B3 is (2), this Theorem allows us to conclude, e.g., that -with reference to Figure 2-

• AF if AM is DC BD BN BMDC BE BN DC BH BN BMDC BF BN DC BG , then CUDC BD BN BMDC BF BN DC BG CV is a reason for B3 AM unsatisfiability, and
• AF if AM is DC BD BN BMDC BE BN DC BH BN BMDC BF BN BMDC BG , then CUDC BD BN BMDC BF BN BMDC BG CV is a reason for B3 AM unsatisfiability.

Our next step is to show how it is possible to compute reasons for B3 AM unsatisfiability while backtracking.

Theorem 2 Let B3 be a QBF. Let D0 be a literal. Let AMBN D0 be an assignment for B3. Let AN be a reason for B3 AMBND0 unsatisfiability.

1. If D0 is not in AN, then AN is a reason for B3 AM unsatisfiability.
2. If D0 BE AN, and D0 is universal, then AN D2 CUD0CV is a reason for B3 AM unsatisfiability.
3. If D0 BE AN, D0 is existential andmonotone in B3 AM , then AN D2CUD0CV is a reason for B3 AM unsatisfiability.
4. If D0 BE AN, D0 BE AN BC , AN BC is a reason for B3 AMBND0 unsatisfiability, and D0 is existential, then B4AN CJ AN BC B5 D2 CUD0BN D0CV is a reason for B3 AM unsatisfiability.

If B3 is (2), considering Theorem 2 and Figure 2:

• AF given what we said in the paragraph below Theorem 1, the 4th statement allows us to conclude that CUDC BD BN BMDC BF CV is a reason for B3 AM unsatisfiability when AM is DC BD BN BMDC BE BN DC BH BN BMDC BF ,
• AF from the above, the 2nd statement allows us to conclude that CUDC BD CV is a reason for B3 AM unsatisfiability when AM is DC BD BN BMDC BE BN DC BH ,
• AF from the above, the 1st statement allows us to conclude that CUDC BD CV is a reason for B3 AM unsatisfiability when AM is in CUDC BD BN BMDC BE BN DC BD CV.

From the last item, it follows that looking for assignments satisfying B3 AM when AM begins with DC BD , is useless. Given this, our "backjumping" procedure would have avoided the generation of the branch leading to (BYBK) in Figure 2.

4.2 Solution-directed Backjumping

The following Theorem allows us to compute the reason for B3 AM result when the matrix of B3 AM is empty. Given a sequence of literals AM, we say that a literal D0 is TRUE-irrelevant in AM if -assuming AM BC is the sequence obtained by deleting D0 in AMthe matrix of B3 AM BC is empty.

Theorem 3 Let B3 be a QBF. Let AM be an assignment for B3 such that the matrix of B3 AM is empty. Let AM BC be a sequence obtained by recursively eliminating a TRUE-irrelevant literal in AM. Let AN be the set of literals in AM BC . Then AN is a reason for B3 AM satisfiability.

With reference to Figure 2, the above Theorem allows us to conclude that, e.g., CUBMDC BD BN DC BG BN DC BH CV is a reason for B3 AM satisfiability, if AM is BMDC BD BN BMDC BF BN DC BG BN DC BH and B3 is (2).

Theorem 4 Let B3 be a QBF. Let D0 be a literal. Let AMBN D0 be an assignment for B3. Let AN be a reason for B3 AMBND0 satisfiability.

1. If D0 is not in AN, then AN is a reason for B3 AM satisfiability.
2. If D0 BE AN, and D0 is existential, then AN D2 CUD0CV is a reason for B3 AM satisfiability.
3. If D0 BE AN, D0 is universal and monotone in B3 AM , then AN D2 CUD0CV is a reason for B3 AM satisfiability.
4. If D0 BE AN, D0 BE AN BC , AN BC is a reason for B3 AMBND0 satisfiability, and D0 is universal, then B4AN CJ AN BC B5 D2 CUD0BN D0CV is a reason for B3 AM satisfiability.

If B3 is (2), considering Theorem 4 and Figure 2:

1 function Backjump(res) 2 DBD6 := InitWr(res); 3 while (CWStack is not emptyCX) 4 D0 := Retract(); 5 if (D0 BE DBD6) 6 if (res = FALSE and CYD0CYBMD8DDD4CT = BL) or 7 (res = TRUE and CYD0CYBMD8DDD4CT = BK) 8 if (CYD0CYBMD1D3CSCT = UNIT) or (CYD0CYBMD1D3CSCT = R-SPLIT) 9 DBD6 := B4DBD6 CJ CYD0CYBMD6CTCPD7D3D2B5 D2 CUD0BN D0CV 10 if(CYD0CYBMD1D3CSCT = L-SPLIT) 11 CYD0CYBMD1D3CSCT := R-SPLIT; 12 CYD0CYBMD6CTCPD7D3D2 := DBD6; 13 return D0; 14 else DBD6 := DBD6 D2 CUD0CV; 15 return NULL;

• AF given what we said in the paragraph below Theorem 3, the 2nd statement allows us to conclude that CUBMDC BD BN DC BG CV is a reason for B3 AM satisfiability when AM is BMDC BD BN BMDC BF BN DC BG ,
• AF from the above, the 2nd statement allows us to conclude that CUBMDC BD CV is a reason for B3 AM satisfiability when AM is BMDC BD BN BMDC BF ,
• AF from the above, the 1st statement allows us to conclude that CUBMDC BD CV is a reason for B3 AM satisfiability when AM is BMDC BD .

From the last item, it follows that looking for assignments falsifying B3 AM when AM begins with BMDC BD , is useless. Given this, our "backjumping" procedure would have avoided the generation of the branch leading to (BYBH) in Figure 2.

5 Implementation in QUBE

A procedure incorporating both conflict-directed and solution-directed backjumping has been implemented in QUBE. A high-level description of this procedure is presented in Figure 3. Consider Figure 3. Assume that B3 is the input QBF and that AM BP D0 BD BN BM BM BM BN D0 D1 is the assignment for B3 corresponding to the sequence of literals stored in the stack. Then,

• AF InitWr(res) initializes the variable DBD6, storing the reason for B3 AM result. In our implementation:
• A0if res BP FALSE, B3 AM contains a contradictory clause. Let BV be a clause in B3 such that, for each literal D0 in BV, D0 is in AM or D0 is universal in B3. Then InitWr(res) returns the set of literals D0 in AM such that D0 is in BV (see Theorem 1). For example, if B3 is (2), and AM is DC BD BN BMDC BE BN DC BH BN BMDC BF BN DC BG , then InitWr(res) returns CUDC BD BN BMDC BF BN DC BG CV.
• A0if res BP TRUE, the matrix of B3 AM is empty. Then InitWr(res) returns the set of literals in the sequence obtained from AM by recursively eliminating a universal literal D0 such that, for each clause BV in B3, if D0 BE BV then there is another literal D0 BC in the sequence with D0 BC BE BV (see Theorem 3). For example, if B3 is (2), and AM is BMDC BD BN BMDC BF BN DC BG BN DC BH , then InitWr(res) returns CUBMDC BD BN DC BG BN DC BH CV.
• AF If D0 is a literal D0 CX in AM, CYD0CYBMD6CTCPD7D3D2 is the property of CYD0CY that, if set, stores the reason for B3 D0 BD BNBMBMBMBND0 CX result.

The function QubeSolver in Figure 1 needs to be modified in two ways. First, if D0 is a unit in B3 AM , then B3 AMBND0 contains a contradictory clause. Let BV be a clause in B3 such that, for each literal D0 BC in BV, D0 BC is in AMBN D0 or D0 BC is universal in B3. Then, the set AN of literals D0 BC in AMBN D0 such that D0 BC is in BV is a reason for B3 AMBND0 unsatisfiability. If UnitSetReason(D0) is invoked when D0 is a unit in B3 AM , and assuming this function returns a set AN defined as above, the instruction

CYD0CYBMD6CTCPD7D3D2 := UnitSetReason(D0);

has to be added in line 8. For example, if B3 is (2), and AM is DC BD BN BMDC BE BN DC BH BN BMDC BF , then DC BG is a unit in B3 AM , B3 AMBNBMDC BG contains a contradictory clause, and CUDC BD BN BMDC BF BN BMDC BG CV is stored in DC BG BMD6CTCPD7D3D2. Second, the procedure BackjumpB4resB5 has to be invoked in place of BacktrackB4resB5 at line 25.

Considering the procedure Backjump(res) in Figure 3 - once the working reason is initialized (line 2) according to the above-Backjump(res) pops all the literals and corresponding QBFs (line 4) from the stack, till a literal D0 is reached such that D0 belongs to the working reason DBD6 (line 5), CYD0CYBMD1D3CSCT is L-SPLIT (line 10), and either

• AF D0 is existential and res=FALSE (line 6); or
• AF D0 is universal and res=TRUE (line 7).

If such a literal D0 exists, CYD0CYBMD1D3CSCT is set to R-SPLIT(line 11), the working reason is stored in CYD0CYBMD6CTCPD7D3D2 (line 12), and D0 is returned (line 13). If no such literal exists, NULL is returned (line 15).

Notice that if D0 is not in DBD6, we can safely retract D0 despite the other conditions (see statement 1 in Theorems 2, 4): Assigning D0 would not change the result of the computation.

If D0 is in DBD6, one of the conditions in line 6 or line 7 is satisfied, but CYD0CYBMD1D3CSCT is UNIT or R-SPLIT (line 8), we can use the results in statement 4 of Theorems 2, 4 to compute the new working reason (line 9).

If D0 is in DBD6 but neither the condition in line 6 nor the condition in line 7 is satisfied, then we can retract D0 and remove D0 fromDBD6 (line 14). See the second statement of Theorems 2, 4.

Finally, given the reasons returned by our implementation of InitWr(res), it is easy to see that neither a universal, monotone literal can belong to the reason of an universal literal when res=TRUE, nor an existential, monotone literal can belong to the reason of an existential literal when res=FALSE. Thus, the statement 3 in Theorems 2, 4 (included for theoretical completeness) is never applied in our implementation.

Our implementation of QUBE with Backjump is a generalization of the conflict-directed backjumping procedure implemented, e.g., in RELSAT: assuming that our procedure and RELSAT -without learning- perform the same nondeterministic choices, the two systems have the same behavior on QBFs without universal quantifiers.

6 Experimental analysis

To evaluate the benefits deriving from backjumping, we compare QUBE with backtracking (that we call QUBE-BT), and QUBE with backjumping (that we call QUBE-BJ). For both systems, we use the branching heuristics described in [Feldmann et al., 2000]). All the tests have been run on a Pentium III, 600MHz, 128MBRAM.

We first consider sets of randomly generated QBFs. The generation model that we use is model A by Gent and Walsh [1999]. In this model, each QBF has the following 4 properties:

1. the prefix consists of CZ sequences, each sequence has D2 quantifiers, and each two quantifiers in a same sequence, are of the same type,
2. the rightmost quantifier is BL,
3. the matrix consists of D0 clauses,
4. each clause consists of CW literals of which at least 2 are existential.

Figure 4 shows the median of the CPU times (left) and number of branching nodes (right) of QUBE-BT and QUBE-BJ when CZ BP BG, D2 BP BFBC, CW BP BH, and D0 (on the DC-axis) is varied in such a way to empirically cover the "100% satisfiable

- 100% unsatisfiable" transition (shown in the background). Notice the logarithmic scale on the DD-axis. Consider Figure 4left. As it can be observed, QUBE-BJ is faster (up-to two orders of magnitude) than QUBE-BT. QUBE-BJ better performances are due to its minor number of branching nodes, as shown in Figure 4-right.

We also test QUBE-BT and QUBE-BJ on the structured Rintanen's benchmarks. 3 These problems are translations from planning problems to QBF (see [Rintanen, 1999a]). For lack of space, Table 1 shows QUBE-BT and QUBE-BJ performances on only 8 out of the 38 benchmarks available. On 13 of the other 30 problems, QUBE-BT and QUBE-BJ perform the same number of branching nodes, and on the remaining 17, none of the two systems is able to solve the problem in the time limit of 1200 seconds. As before, QUBE-BJ never performs more branching nodes than QUBE-BT, and is sometimes much faster. The last line of the table shows that when the number of branching nodes performed by QUBEBT and QUBE-BJ is the same, the computational overhead paid by QUBE-BJ is not dramatic.

7 Conclusions and Future work

In the paper we have shown that it is possible to generalize the conflict-directed backjumping schema for SAT to QBFs. We have introduced solution-directed backjumping. Our implementation in QUBE shows that these forms of backjumping can produce significant speed ups. As far as we know, this is the first time a backjumping schema has been proposed, implemented and experimented for QBFs. It is worth remarking that the logics of conflict-directed (section 4.1) and solutiondirected (section 4.2) backjumping are symmetrical: Indeed, it would have been easy to provide a uniform treatment accounting for both forms of backjumping. We decided not to do it in order to improve the readability of the paper, at the same time showing the tight relations with the conflictdirected backjumping schema for SAT.

Beside the above results, we have also comparatively tested QUBE and some of the other QBF solvers mentioned in the introduction. Our results show that QUBE compares well with respect to the other deciders, even without backjumping. For example, of the 38 Rintanen's structured problems, DECIDE, QUBE-BJ, QUBE-BT, QSOLVE, EVALUATE are able to solve 35, 21, 18, 11, 0 samples respectively in less than 1200s. In this regard, we point out that DECIDE features

3 Available at www.informatik.uni-freiburg.de/ ˜rintanen/qbf.html.

"inversion of quantifiers" and "sampling" mechanisms which seem particularly effective on these benchmarks.

QUBE, the experimental results, and the test sets used are available at QUBE web page:

QUBE, besides the backjumping procedure above described, features six different branching heuristics, plus an adaptation of trivial truth (see [Cadoli et al., 1998, Cadoli et al., 2000]). (See [Giunchiglia et al., 2001b] for a description of QUBE's available options.) About trivial truth, backjumping and their interactions, we have conducted an experimental evaluation on this. The result is that neither trivial truth is always better than backjumping, nor the other way around. On the other hand, the overhead of each of these techniques (on the test sets we have tried) is not dramatic, and thus it seems a good idea to use both of them. These and other results are reported in [Giunchiglia et al., 2001c].

About the future work, we are currently investigating the effects of using different branching heuristics. Then, we plan to extend QUBE in order to do some form of "size" or "relevance" learning as it has been done in SAT (see, e.g., [Bayardo, Jr. and Schrag, 1997]).

Acknowledgments

Thanks to Davide Zambonin for the many fruitful discussion about implementation. Thanks to an anonymous reviewer for suggesting the name "solution-directed backjumping". Thanks to 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.