Improvements to the Evaluation of Quantified Boolean Formulae

1 Introduction

Many computational problems can be conveniently for­ mulated in classical propositional logic. Examples of such are many constraint satisfaction problems, forms of planning, and many problems in graph-theory. A com­ mon property of these problems is that they belong to the complexity class NP and that there are therefore polynomial-time translations from them to the satisfia­ bility of formulae in the classical propositional logic.

However, there are many important problems that are (under plausible complexity-theoretic assumptions) out­ side the complexity class NP, and therefore cannot be in general efficiently translated to the problem of satisfia­ bility of propositional formulae. Many such problems are PSPACE-hard or harder and can be forced to NP only by making restrictions that make the problems lose most of their practically interesting aspects. There are, however , a number of problems that belong to the classes in the polynomial hierarchy, many of them to its lower levels. These include determining the truth-value of quantified Boolean formulae [Meyer and Stockmeyer, 1972], com­ puting the radius of a covering code [McLoughlin, 1984], many decision problems in nonmonotonic logics [Gott­ lob, 1992], some forms of abduction JEiter and Gottlob, 1995], and determining the Vapnik-Cervonenkis dimen­ sion in probability theory [Schafer, 1996].

Like satisfiability algorithms can be used for solving problems in NP, a similar approach is applicable to prob­ lems higher in the polynomial hierarchy: implement an efficient decision procedure for one problem, and give good polynomial-time translations from other problems to that problem. The use of QBF this way has not been investigated partly because there have been no efficient decision procedures. Translation to QBF has recently been proposed as a solution method for conditional plan­ ning [Rintanen, 1999).

In this work we present an algorithm for determining the truth of quantified Boolean formulae, and evaluate it with randomly generated quantified Boolean formulae and formulae from conditional planning.

2 Preliminaries

Quantified Boolean formulae are of the form q1x1 · · · qnxn¢ where ¢ is a propositional formula and the prefix consists of universal V and existential 3 quan­ tifiers qi and the propositional variables Xi occurring in ¢. Define ¢[7/J/x) as the formula obtained from¢ by re­ placing occurrences 1 of the propositional variable x by the formula 7/J . The truth of formulae is defined recur­ sively as follows. The truth of a formula that does not contain variables, that is, that consists of connectives and the constants true T and false ..1 , is defined by the truth-tables for the connectives. A formula 3x¢ is true if and only if ¢[T jx] or ¢[..1/x) is true. A formula Vx¢ is true if and only if ¢[T jx] and ¢[..1/x) are true. Examples of true formulae are 'ix3y(x t-ty) and 3x3y(x 1\ y) . The formulae 3x'iy(x t-ty) and 'ix'iy(x V y) are false.

1 We assume that nested quantifiers do not quantify the same variable.

PROCEDURE decide(e, (M1, M2, ... , Mn), C) BEGIN C := unit(C); IF 0 E C THEN RETURN false; IF n = 0 THEN RETURN true; remove from M1 all variables not inC; IF M1 = 0 THEN RETURN decide( note, (M2, ... , Mn), C); x := a member of M1; M1 := M1 \{x}; !Fe THEN IF decide(e, (M1, ... , Mn), C U { {x}}) THEN RETURN true; ELSE IF not decide(e, (M1, ... , Mn), C U { {x}}) THEN RETURN false; RETURN decide(e, (M1, ... , Mn), C U { { ·x}}) END

3 The Basis Algorithm

We have designed and implemented an algorithm that determines the truth-value of quantified Boolean formu­ lae. The Davis-Putnam procedure [Davis et al., 1962] is a special case of the algorithm. The main differences are that instead of only or-nodes, the search tree for quanti­ fied Boolean formulae contains also and-nodes that cor­ respond to universally quantified variables, and that the order of the variables in the prefix constrains the order in which the variables generate a search tree.

The main procedure of the algorithm sketched in Figure 1 takes three parameters. 2 The variable e is true if the first quantifier in the prefix of the formula is :3. The sequence (M1, ... , Mn) represents the pre­ fix. For example, if the prefix is :lx1:lx2\fxs:lx4 , then M1 = {x1,x2},M2 = {x3 } and M3 = {x4 }. The set C consists of clauses { h, ... , ln} where n 2: 0 and li are literals. The empty clause 0 is false.

The subprocedure unit performs simplification by unit resolution and unit subsumption; unit(S) is defined as the fixpoint of F under a set S of clauses.

So for the purposes of this paper, our definition of unit subsumption retains unit clauses in the clause set.

4 Pruning Techniques

An important difference between the Davis-Putnam pro­ cedure and the algorithm for QBF is that the order in which branching variables are chosen is dependent on

2 The algorithm is simplified because we just want to indi­ cate what the main differences from the Davis-Putnam pro­ cedure are. For example, we do not require that the variable x does not have a truth-value when it is branched on.

let A1, ... , An be consistent subsets of Y U { ·YIY E Y} ; FOR i := 1 TO n DO C' := unit(C u U(Ai)); R := C' n U(X U {·xlx EX}); IF 0 (j. C' THEN C := unit(C U R); FOR EACHp EX DO C" := unit( C' U { { ·P}}); IF 0 E C" THEN C := unit(C U { {p}}); IF 0 E C THEN RETURN false; (* Similarly for p *) C" := unit(C' U {{p}}); IF 0 E C" THEN C := unit(C u { { ·p}} ); IF 0 E C THEN RETURN false; END END

their location in the prefix. The branching variable is always quantified by the outermost quantifier. In struc­ tured problems it is often the case that many of the first variables occur only in clauses that also contain vari­ ables quantified by inner quantifiers, and an almost ex­ haustive search through all truth-values for the variables may be needed because unit propagation does not yield the truth-values. Already for a small number of vari­ ables this can be prohibitively expensive. For example in a formula :JX\fY:JZI!>, if lXI = 20, the variables in X induce a search tree with 2 20 leaf nodes, with a poten­ tially difficult QBF to evaluate in each.

In this section we first propose two pruning techniques that are based on reasoning with variables that are not quantified by the current outermost quantifier. The third technique is an extension of the use of unit propa­ gation for detecting failed literals, and the fourth reduces the computation needed in going through all valuations of universally quantified variables.

4.1 Inverting Quantifiers

Given :JX\fY 4>, it is useful to look also at the formula \fY:JX 4>. 3 If for some valuation of variables in Y only certain valuations of X are possible, these valuations are the only possible ones also for the formula :JX\fY 4> .

The technique we propose is based on the above idea, and we therefore call it the inversion of the quantifiers. We randomly assign some truth-values to variables in Y (it may be possible and useful to try out all possible valuations of Y), and then try to detect failed literals with unit propagation [Li and Anbulagan, 1997]. Any truth-values obtained for variables in X are those that must be chosen when evaluating :JX\fYI!>. Inversion is only applicable to formulae with :3 as the first quantifier. The program code in Figure 2 outlines how quantifier inversion is performed. This code is run before the first call to the main procedure is made. The function U(L) = { {l}ll E L} produces a set of unit clauses from a set of literals.

3 The formula <P may contain quantifiers.

FOR EACH p EX such that { {p}, { ·p}} n C = 0 FOR i := 1 TO numberOfSamples DO R := random consistent subset of Y U { ·YIY E Y} ; C' := unit(C u U( {p} u R)); IF 0 E C' THEN C := unit(C U { { ·p}}); IF 0 E C THEN RETURN false; (* Similarly for ·p *) R :=random consistent subset of Y U {·YIY E Y}; C' := unit(C u U( { ·p} u R)); IF 0 E C' THEN C := unit(C U { {p}} ); IF 0 E C THEN RETURN false; END END

4.2 Sampling

When choosing a truth-value for a variable x E X in a formula :JX'v'Y.P, it would be useful to check that the choice is possible under all valuations of variables in Y. This is, however, expensive. Nevertheless, it has turned out that trying out at least some valuations of Y and per­ forming unit propagation helps in the detection of wrong choices. The valuations of a small number of variables in Y are chosen randomly. We call this sampling of Y. This technique is similar to the first one, but because it is performed for many variables in every node of the search tree, valuations of Y cannot be covered very ex­ haustively.

Sampling is best combined with the use of unit prop­ agation in choosing branching variables and detecting failed literals , but here we describe it separately. The program code in Figure 3 outlines how sampling is per­ formed. The code is inserted right after the first call to the function unit in the main procedure.

4.3 Failed Literal Detection

The third technique is the use of unit propagation for detecting failed literals [Li and Anbulagan, 1997] also for variables quantified by inner quantifiers. This proceeds by adding a literal to the clause set, and then performing unit propagation. If an empty clause is obtained and the literal is existential, the complement of the literal must be true and it is added to the clause set. If the literal is universal , the formula is false .

In the quantified case also the occurrence of a clause with universal variables only may yield a failed literal. Here the ordering of variables in the prefix has to be observed. Consider the formula 'v'x:Jy(x t-+ y) which is in clausal form 'v'x:Jy( (x V ·y) A ( ·x Vy)). If we try to see whether y is a failed literal by adding the literal y to the clause set and performing unit propagation, we get the unit clause x with a universal variable. This would seem to indicate that y should be assigned false. However, the value of y is a function of the value of x, and y may assume different values for different values of x.

Lemma I Let F = :JX1 'v'Y1:JX2'v'Y2 · · · 1> be a QBF. Assume 1> U {I} ~ 11 V ... V ln such that the propo-

sitional variables p, p1 , . .. , Pn occur respectively in lit­ erals l,ll , ... , ln . Then F is false if {PI, .. ·,Pn} ~ Yj U Yj+l U · · · for some j and p E Xk for some k ::; j.

4.4 Splitting Clause Sets

Apart from the above techniques specific to QBF, we maintain a graph describing the dependencies between variables: there is an edge between two variables if they occur in the same clause. In each node of the search tree, for separate connected components separate recur­ sive calls to the main procedure of the algorithm are made. This has a noticeable effect on the efficiency of the algorithm on certain random problems as well as on some structured problems. For example, for a true 'v':J QBF not all combinations of truth-values for universally quantified variables have to be considered if the variables occupy different connected components. This is often the case for random QBF with a low clauses/variables ratio. Consider a formula with n universai variables. Normally a tree with 2n leaves has to be traversed, but if the clause set is split so that universal variables are evenly in m components, m search trees with only 2n!m leaves have to be traversed. For example, for n = 20 and m = 2 this means a decrease from about 10 6 to 2000.

5 Experiments

We have tested the implementation of our algorithm and the new techniques on a number of problems from con­ ditional planning and on a number of random quantified Boolean formulae. Our Davis-Putnam implementation that we have extended to handle QBF and on top of which all the new techniques have been implemented, is closest to Li and Anbulagan's [1997] SatO, but slower.

The basis of the generation of random quantified Boolean formulae is the fixed clause length model [Mitchell et al., 1992] for generation of random propo­ sitional formulae, in which 3-literal clauses are gener­ ated by randomly choosing three variables from a set of N variables and negating each with probability 0.5. The presence of clauses with less than two existential variables asymptotically causes all formulae to be false when the number of variables increases [Gent and Walsh, 1998] . This is because the probability of a clause with universal literals only or two clauses with complementary existential literals and both with two universal literals becomes very high. Hence for the generation of random quantified formulae we use model A of Gent and Walsh [1998] in which no clauses with less than two existential literals are generated. In our test runs N = 50 and the QBF have the prefix :J'v':J. Effect of the techniques on formulae with prefixes 'v':J and 'v':J'v':J is similar. We ran our program by varying two parameters, the proportion of universal variables in the prefix and the number of clauses. The proportion of universal variables was in­ creased by 3 per cent steps and the clauses/variables ratio by steps of 0.2. If we have 100 variables and 50 per cent of them are universal , the first quantifier quantifies the variables 1- 25, the second quantifier the variables

26- 75, and the third quantifier the variables 76-100. We have observed that (in the presence of the other tech­ niques) both inversion and sampling - the techniques that turn out to be most effective for the structured prob­ lems we consider - affect very little the number of nodes in search trees. Therefore the test runs were with these techniques disabled.

The results from the test runs are depicted in Figures 4, 5, 6, 7 and 8. The runtime for every combination of parameter values is the average of runtimes for 60000 formulae. All the runs were on a Sun Ultra II worksta­ tion with a 296 MHz processor. The execution times are not very accurate because the smallest measurable unit of CPU time was 10 milliseconds. Figure 4 depicts the proportion of true formulae for all parameter values considered. When increasing the proportion of universal variables, the region of formulae that are more difficult to evaluate shifts to the direction of lower clauses/variables ratios. The phase transition region from true to false shifts similarly. Figure 5 shows the runtimes with full detection of failed literals (Section 4.3) and partitioning of clause sets (Section 4.4.) . Figure 6 shows runtimes without full detection of failed literals and Figures 7 and 8 runtimes without partitioning. The peak in Figure 7 is due to a very small number of difficult formulae. As is obvious from a comparison between Figures 5 and 8, the effect of partitioning on formulae with few universal variables is small.

The diagrams show that detection of failed literals for all variables is useful , although the effect is not dramatic. Partitioning of clause sets reduces the amount of compu­ tation dramatically for a small number of formulae with many universal variables and a small clauses/variables ratio. This is because partitioning produces several small clause sets with disjoint variables, and hence considering all 2" valuations of n universal variables takes much less than 0(2 11 ) time.

The structured problems we consider are translations from conditional planning to QBF [Rintanen, 1999] . The most basic form of planning is the identificat ion of se­ quences of operations that reach a goal state from a given initial state. That problem has been success­ fully solved by algorithms that test propositional sat­ isfiability [Kautz and Selman, 1996]. In conditional planning, plans that work under several different cir­ cumstances are constructed. A conditional plan is es­ sentially a program in a simple programming language with conditional statements that chooses at execution time which operations to apply. When there is only one initial state, planning can be represented by formu­ lae ::lp1 · · · p71 ::le1 ···em <I> that say that there is a plan (represented by the variables p;) such that its execution (represented by the variables e;) produces a goal state. Conditional planning can be represented by formulae ::lp1 · .. Pn '<lc1 · · · cp::le1 ···em <I> where variables c; repre­ sent the different circumstances the plan has to work in.

Runtimes for formulae from conditional planning are given in Table 1. These formulae encode the problem of existence of conditional plans for taking three or four blocks from all possible initial configurations to a unique goal configuration. We have evaluated the effect of each technique separately. The first column identifies the for­ mulae in question. The second column gives the number of propositional variables in each QBF, and the third the number of clauses. The fourth column gives the truth­ value of the formula. The fifth gives the runtime of our theorem-prover with all techniques enabled. The sixth gives the runtime with inversion disabled. The seventh with sampling disabled. The eighth with detection of fai led literals for inner quantifiers disabled. The ninth without partitioning of clause sets. For sampling the number of samples was 10 with at most 16 variables in each sample (the formulae all have less than 16 univer­ sal ,·ariables), and for inversion the number of valuations considered was at most 100.

In some cases disabling one of the pruning techniques leads to a better runtime, but these are the easier formulae and the differences are relatively small. The only technique that in most cases does not have any effect is the partitioning of clause sets. Only for three formulae there is a significant decrease in the runtimes, from 14.6 to 1.7, from 165.1 to 76.1 and from 13802.7 to 192.5. We would expect that on many structured problems the decrease is small. When none of the techniques is used, none of the runs end in 4 hours. Sampling and inversion are the most effective techniques: without them four of the formulae could not be evaluated in 4 hours .

6 Related work

Automated reasoning with quantified Boolean formulae has been investigated by Kleine Biining et al. [1995] who define a resolution rule for quantified Bool~an formulae and a polynomial time decision procedure for quantified Horn clauses. Aspvall et al. [1979] give a polynomial time decision procedure for quantified 2-literal clauses.

Cadoli et al. [1998] extend the Davis-Putnam pro­ cedure to handle quantified Boolean formulae. Their algorithm is similar to the one in Section 3. Cadoli et al. generalize techniques familiar from the Davis­ Putnam procedure to QBF. For example, they introduce the pure literal rule for universal variables and a rule that concludes that formulae with clauses without exis­ tential variables are false. A technique not employed by us is testing whether the set of clauses with all univer­ sal literals deleted is satisfiable. If it is, the formula is true. Cadoli et al. perform this test in every node of the search tree. It seems to us that on random problems with many universal variables and a low clauses/variables ra­ tio it may be beneficial like the technique we present in Section 4.4. The algorithm by Cadoli et al. does not evaluate any of the formulae in Table 1 in 16 hours. We also ran an experiment on a small set of random ::JV::J for­ mulae with 150 variables and parameters varying like in the experiments reported in this paper. A small number of the formulae were much more difficult for the program by Cadoli et al. and some of the very easy formulae were evaluated faster. The sum of the runtimes for our pro­ gram was 85.7 seconds versus 4965.28 seconds for the Cadoli et al. program. For a bigger set of random for­ mulae with 100 variables the runtimes were 25.36 seconds versus 410.79 seconds.

7 Conclusions and Future Work

Future work includes a systematic study of computa­ tional properties of QBF arising from applications, in­ cluding AI planning, automated theorem-proving and computer-aided verification, and then improving the QBF algorithm accordingly. There are several degrees of freedom in the use of the new techniques , and only by analyzing a wider range of problems it is possible to determine what is the best way of using them.

As an important research topic we see the reduction of exhaustive search needed in handling universal quanti­ fiers. The technique presented in this paper is applicable only in relatively simple cases .

Acknowledgements

This research was funded by the Deutsche Forschungsge­ meinschaft through the SFB 527. We thank the referees for comments on the generation of random QBF and Marco Cadoli et a!. for access to their program.