# «David A. Plaisted Computer Science Department, University of North Carolina Chapel Hill, NC 27599-3175, USA Armin Biere ETH Z¨rich, Computer Systems ...»

A Satisﬁability Procedure for

Quantiﬁed Boolean Formulae

David A. Plaisted

Computer Science Department, University of North Carolina

Chapel Hill, NC 27599-3175, USA

Armin Biere

ETH Z¨rich, Computer Systems Institute

u

8092 Z¨rich, Switzerland

u

Yunshan Zhu

Advanced Technology Group, Synopsys Inc.

Mountain View, CA 94040, USA

Abstract

We present a satisﬁability tester Qsat for quantiﬁed Boolean formulae and a restriction QsatCNF of Qsat to unquantiﬁed conjunctive normal form formulae. Qsat makes use of procedures which replace subformulae of a formula by equivalent formulae. By a sequence of such replacements, the original formula can be simpliﬁed to true or false. It may also be necessary to transform the original formula to generate a subformula to replace. QsatCNF eliminates collections of variables from an unquantiﬁed clause form formula until all variables have been eliminated. Qsat and QsatCNF can be applied to hardware veriﬁcation and symbolic model checking.

Results of an implementation of QsatCNF are described, as well as some complexity results for Qsat and QsatCNF. Qsat runs in linear time on a class of quantiﬁed Boolean formulae related to symbolic model checking. We present the class of “long and thin” unquantiﬁed formulae and give evidence that this class is common in applications. We also give theoretical and empirical evidence that QsatCNF is often faster than Davis and Putnam-type satisﬁability checkers and ordered binary decision diagrams (OBDDs) on this class of formulae. We give an example where QsatCNF is exponentially faster than BDDs.

Key words: QBF, Satisﬁability, Davis & Putnam Procedure, BDDs, Cut Width, Circuit Veriﬁcation, Model Checking.

Preprint submitted to Discrete Applied Mathematics 26 March 2002 Qsat is a new decision procedure for satisﬁability of quantiﬁed Boolean formulae with potential applications to hardware veriﬁcation and symbolic model checking. The philosophy of Qsat is to test satisﬁability of a formula by repeatedly replacing subformulae by simpler equivalent subformulae. QsatCNF is an application of Qsat to unquantiﬁed clause form formulae, interpreted as quantiﬁed Boolean formulae by considering all free variables to be existentially quantiﬁed. Qsat and QsatCNF test satisﬁability of a formula by successively eliminating variables from it, producing an equivalent formula, until all variables have been eliminated. The motivation for Qsat and QsatCNF is that satisﬁability testers for unquantiﬁed formulae such as Davis and Putnam’s method seem tobe more eﬃcient than BDDs (ordered BDDs, OBDDs) when there is not too much backtracking. BDDs can process large (unquantiﬁed) formulae because they make use of an ordering of the variables which breaks the processing down into smaller steps that are easier to perform. The idea of Qsat and QsatCNF is to import this BDD philosophy into satisﬁability testing, by applying a modiﬁcation of Davis and Putnam’s method not to the whole formula at once, but piece by piece, where each application of the modiﬁed Davis and Putnam method to a piece of the formula simpliﬁes the formula. This reduces the amount of backtracking. Qsat and QsatCNF can be built on top of any satisﬁability tester for unquantiﬁed Boolean formulae, including St˚almarck’s method [1].

It appears (see section 11) that BDDs are good for systems that are long and thin, such as adders. These are also systems for which QsatCNF should be eﬃcient, because such systems can be broken into parts having a limited amount of communication between them. Each part corresponds to a subformula of the original formula. QsatCNF can simplify one such subformula, and then be applied recursively to the remaining formula. Thus it may be that QsatCNF is eﬃcient on a large number of applications where BDDs are currently used.

Similarly, Qsat should be eﬃcient for quantiﬁed Boolean formulae that are long and thin, in a certain sense. BDDs can also be eﬃcient on problems that are not long and thin, such as some versions of barrel shifters. QsatCNF may not be as fast on such problems.

The general method by which Boolean formulae are used for system testing is

**the following:**

(1) A Boolean formula G is constructed from a system S and its speciﬁcation, expressing that the system does not satisfy its speciﬁcation. Methods for generating G are well known.

(2) The formula G is tested for satisﬁability (consistency).

(3) If G is unsatisﬁable, then S is correct. If G is satisﬁable, then there is an Email addresses: plaisted@cs.unc.edu (David A. Plaisted), biere@inf.ethz.ch (Armin Biere), yunshan@synopsys.com (Yunshan Zhu).

error in S, and the nature of the satisﬁability of G can help to identify the error in S.

The system S can be a computer circuit or some system containing interconnected objects, which can be deﬁned as a component or part of a physical system, such as a gate in a circuit. The formula G can be obtained by deﬁning the formula A as a Boolean formula representing the system S and B as a Boolean formula representing the statement that S fails to satisfy its speciﬁcation. Then G can be taken to be the conjunction A ∧ B of these two formulae, expressing that S fails to satisfy its speciﬁcation.

Binary decision diagrams (BDDs) [2] have been widely used in CAD applications such as logic synthesis, testing and formal veriﬁcation. BDDs transform a circuit into a canonical form, depending on an ordering of the Boolean variables, and two circuits are equivalent if and only if they have the same canonical form. For many kinds of circuits, BDDs work very well, especially when a good ordering of the variables can be found. Equivalence checking [3,4] is important, because one can verify a new or optimized circuit by showing that it is equivalent to an old and trusted circuit. Commercial equivalence checkers can now verify circuits with millions of gates which are clearly out of reach for traditional simulation.

Satisﬁability algorithms for Boolean formulae in clause form can also be used for hardware veriﬁcation[5]. In this approach, the formula G above is in clause form, which is a special form of unquantiﬁed Boolean formula. An eﬃcient method such as Davis and Putnam’s method can then be applied to test if the formula G is satisﬁable. Davis and Putnam’s method was ﬁrst described in the paper [6], though modern implementations diﬀer in some ways. Most modern implementations use the method of DPLL [7], which eliminates variables by case analysis rather than ordered resolution. A recent, very eﬃcient implementation of DPLL is described in [8]. [9] combined BDDs and satisﬁability testers to solve veriﬁcation problems. Another method for satisﬁability testing of unquantiﬁed Boolean formulae, not necessarily in clause form, is disclosed in [1]. This method works breadth-ﬁrst, trying all possible truth assignments to small subsets of the variables of a formula. From these assignments, information about dependencies between variables is obtained which can aid in determining satisﬁability.

Automatic test pattern generation (ATPG) is another important problem in CAD. Given a combinational circuit, a stuck-at fault causes a wire to have a constant value. The task of ATPG is to generate input patterns that detect such stuck-at faults. It was well known that ATPG is equivalent to propositional satisﬁability. Eﬃcient SAT-based ATPG techniques have been developed[10].

Symbolic model checking [11,12,13] is concerned with verifying sequential systems. The use of BDDs for symbolic model checking was a breakthrough, because it permitted much larger systems to be veriﬁed than was possible before. BDDs permit the state of a system to be represented and manipulated eﬃciently, in many cases. However, the paper [14] gives some Boolean formulae obtained from symbolic model checking problems on which satisﬁability algorithms such as DPLL and Stalmarck’s method are more eﬃcient than BDDs. Other examples are given in [5] in which the smallest BDD for a Boolean function is of exponential size, regardless of the variable ordering used. There is therefore also an interest in seeing how far satisﬁability-based approaches can extend in symbolic model checking applications.

Boolean satisﬁability has been extensively studied. See [15] for an excellent survey of a wide range of satisﬁability techniques. However some important problems in hardware veriﬁcation cannot be expressed with quantiﬁer-free Boolean formulae. Computing ﬁxed points in symbolic model checking is one such example. Therefore there is a need for satisﬁability testers for quantiﬁed Boolean formulae. There has been some work in decision procedures for quantiﬁed boolean formulae [16,17]. Our technique diﬀers from the previous work in that it modiﬁes the quantiﬁed Boolean formula from the inside out, rather from the outside in. That is, Qsat can choose to process a quantiﬁer other than one of the outermost quantiﬁers of the formula.

The same ﬂexibility in the processing of quantiﬁers is inherent in QsatCNF.

This ﬂexibility enables QsatCNF to exploit structures in the hardware veriﬁcation domain. In particular, QsatCNF is very eﬃcient in handling long and thin circuits. Note that the propositional satisﬁability problem without quantiﬁers is a special case of quantiﬁed Boolean formulae where all variables are assumed to be existentially or universally quantiﬁed. Since QsatCNF resembles the behaviors of BDDs, it complements the traditional DPLL style SAT solvers. An interesting future research direction is to combine the two approaches.

Many of the problems mentioned in [18] are “long and thin,” meaning that they have small cut widths. Actually, the deﬁnition of cut width diﬀers somewhat from one paper to another, but all such deﬁnitions capture approximately the same idea. We will show below that many of the problems from [19] are also long and thin, as well as several other benchmark problems we constructed.

In fact all problems we tried from [19] have an average cut width of 19 or less. This suggests that the class of long and thin problems is fairly common in applications. It turns out that the worst-case time bound for QsatCNF on this class of long and thin problems is better than that of BDD’s and Davis and Putnam’s method by an exponential factor. We also have examples where the QsatCNF implementation is faster than BDD’s and Davis and Putnam’s method on this class of problems. This gives empirical and theoretical evidence that QsatCNF will be faster on many problems from this class.

The ﬁrst author has obtained US patent 6,131,078 on Qsat.

1 Terminology

1.1 Boolean quantiﬁers and operators ∃ is used for existential quantiﬁcation and ∀ for universal quantiﬁcation. ∧ is used for logical conjunction (and), ∨ for logical disjunction (or), and ¬ for logical negation. The symbol ↔ is used for equivalence and + for exclusive or.

The constants true and false are called truth values. The Boolean operators are deﬁned on truth values in standard ways, so that x ∧ y is true if and only if x is true and y is true, x ∨ y is true if and only if x is true or y is true, ¬x is true if and only if x is false, x ↔ y is true if and only if x and y have the same truth value, and (x + y) is true if and only if x and y have diﬀerent truth values. Capital letters (like X and Y ) refer to sets or sequences of Boolean variables.

**1.2 Formulae**

A quantiﬁed Boolean formula is a formula built up from Boolean variables and the Boolean operators of conjunction, disjunction, negation, and other Boolean operators. Thus (x ∧ (y ∨ z)) is a quantiﬁed Boolean formula. Boolean quantiﬁers are also allowed to occur in quantiﬁed Boolean formulae. Thus if B is a quantiﬁed Boolean formula and X is a set of Boolean variables, then ∃X[B] and ∀X[B] are also quantiﬁed Boolean formulae, where ∃X is considered an existential quantiﬁer and ∀X is considered a universal quantiﬁer. ∀X[B] is often considered to abbreviate ¬∃X[¬B]. If X is the set or list {x, y, z}, then ∃X[A] abbreviates the quantiﬁed Boolean formula ∃x[∃y[∃z[A]]]. An example of a quantiﬁed Boolean formula is ∃x[x ∧ ¬∃y[y ∨ z]]. Often the term “quantiﬁed” is dropped. A quantiﬁed Boolean formula without any occurrences of quantiﬁers is said to be unquantiﬁed. An occurrence of a variable x in a formula A is called free if this occurrence is not within the scope of a quantiﬁer ∃x or ∀x. Only the occurrence of z is free in the example formula. Variable occurrences that are not free are called bound. If A is a quantiﬁed Boolean formula and X is a set of variables, then A[X] denotes a formula A that contains the free variables X. A formula B having the free variables X is often taken to abbreviate ∃X[B] or ∀X[B]. A literal is a Boolean variable or its negation.

If y is a variable, it is assumed that ¬¬y is identical to y. The literal ¬y is the complement of y, and likewise y is the complement of ¬y. The literals y and ¬y are said to be complementary. A clause is a disjunction of literals, as, x ∨ ¬y ∨ z. A set of clauses, also termed a conjunctive normal form formula, is a conjunction of clauses, such as C ∧ D ∧ E, where C, D, and E are clauses.

1.3 Subformulae Each Boolean formula A is a subformula of itself. Also, if A is of the form B ⊗ C, where ⊗ is a Boolean operator, and D is a subformula of B or C, then D is also a subformula of A. Likewise, if D is a subformula of B, then D is a subformula of ¬B and a subformula of ΩX[B] where Ω is ∃ or ∀.

1.4 Simpliﬁcations For a Boolean formula A, A|y refers to A with all free occurrences of the Boolean variable y replaced by true, and the resulting formula simpliﬁed as many times as possible with respect to usual Boolean simpliﬁcations. These are the following: B ∧ true simpliﬁes to B, B ∧ false simpliﬁes to false, and other standard simpliﬁcations for eliminating true and false from Boolean expressions. Also, ∃x[B] and ∀x[B] simplify to B if there are no free occurrences of the variable x in B. Let A|¬y refers to A with all free occurrences of the variable y replaced by false, and the resulting formula likewise simpliﬁed.