# «Abstract. State-of-the-art solvers for Quantiﬁed Boolean Formulas (QBF) have employed many techniques from the ﬁeld of Boolean Satisﬁability ...»

Beyond CNF: A Circuit-Based QBF Solver

Alexandra Goultiaeva, Vicki Iverson, and Fahiem Bacchus

Department of Computer Science

University of Toronto

{alexia,viverson,fbacchus}@cs.toronto.edu

Abstract. State-of-the-art solvers for Quantiﬁed Boolean Formulas (QBF) have

employed many techniques from the ﬁeld of Boolean Satisﬁability (SAT) includ-

ing the use of Conjunctive Normal Form (CNF) in representing the QBF formula.

Although CNF has worked well for SAT solvers, recent work has pointed out some inherent problems with using CNF in QBF solvers.

In this paper, we describe a QBF solver, called CirQit (Cir-Q-it) that utilizes a circuit representation rather than CNF. The solver can exploit its circuit repre- sentation to avoid many of the problems of CNF. For example, we show how this approach generalizes some previously proposed techniques for overcoming the disadvantages of CNF for QBF solvers. We also show how important techniques like clause and cube learning can be made to work with a circuit representation.

Finally, we empirically compare the resulting solver against other state-of-the-art QBF solvers, demonstrating that our approach can often outperform these solvers.

1 Introduction QBF is a powerful generalization of SAT in which the variables can be universally or existentially quantiﬁed. While any problem in NP can be encoded in SAT, QBF allows us to encode any problem in PSPACE. This opens a much wider range of poten- tial application areas for a QBF solver, including problems from areas like automated planning (particularly conformant and conditional planning), non-monotonic reasoning, electronic design automation, scheduling, model checking and veriﬁcation, strategic de- cision making, and multi-agent scenarios, see for, e.g., [1,2,3].

State-of-the-art QBF solvers have utilized a number of techniques inherited from SAT solving technology. This has included the use of DPLL search augmented with clause learning along with additional QBF-speciﬁc techniques like solution backtrack- ing and cube learning. Besides DPLL the original Davis-Putnam SAT solving technique [4] of ordered resolution has also been utilized [5], as well as methods involving the use of Skolemization to convert the QBF formula to SAT [6]. One constant in almost all of this work, however, has been the utilization of conjunctive normal form (CNF) in representing the QBF formula.

It has long been noted that conversion to CNF can lead to losing structure that could potentially be exploited computationally. As a result there has been some work on non- CNF SAT solvers, e.g., [7,8]. This work has shown that non-clausal representations can be effective for solving SAT. Nevertheless, the allure of CNF is that it can lead to very high performance implementations since it is a very simple and uniform representation.

Hence, the extra structure that can be exploited in a non-clausal representation has not been able to signiﬁcantly outweigh the practical advantages of CNF in SAT solvers, and most SAT solvers continue to utilize CNF.

In QBF however the situation is different. In particular, for a similarly sized problem the search space explored by a QBF solver tends to be much larger than that explored by a SAT solver. Hence, there is much more potential for savings from exploiting the extra structure contained in non-clausal representations. In fact, there have been a number of papers that have identiﬁed various inadequacies of the CNF representation for QBF and proposed alternate representations aimed at addressing these problems, e.g., [9,10].

One of the most general and structure laden non-clausal representations is a circuit representation. Circuit representations have been used before in SAT solvers, e.g., [7,8], and in this paper we explore the use of this representation in a QBF solver.

One advantage of circuits is that they are more compatible with real problems— typically CNFs are generated from more structured representations like circuits. We also investigate ways of exploiting within our solver some of the extra structural information contained in the circuit. One particular example is the exploitation of don’t care reasoning. We explain why don’t care reasoning has more potential for efﬁciency gains when solving a QBF than when solving SAT. We also demonstrate how the essential techniques of unit propagation, clause learning, and cube learning used in CNF solvers can be adapted to a circuit representation. Finally, we explain how a circuit representation generalizes some of the key previously proposed techniques for addressing the inadequacies of CNF in the context of QBF.

We have implemented a solver we call CirQit (pronounced Cir-Q-it) that is based on our approach of utilizing a circuit representation. We are able to show empirically that it is very competitive with current state-of-the-art QBF solvers, and that on some problem suites it exhibits superior performance.

In the rest of the paper we ﬁrst provide some essential background on QBF and the circuit representation of a QBF. We present some of the details of our circuit-based solver. Our solver utilizes a DPLL search procedure running on a circuit representation rather than on a CNF representation. We describe how propagation can be performed, and how clause and cube learning can be implemented. We discuss related work on QBF solvers based on non-clausal representations. Finally, we present various experimental results demonstrating the merit of our approach, and close with some conclusions.

2 Background

2.1 QBF A QBF has the form Q.φ, where φ is an arbitrary propositional formula and Q is a sequence of quantiﬁed variables (∀x or ∃x). We require that the set of variables in φ be contained in Q so that Q.φ has no free variables, and that φ contain only the connectives AND (∧), OR (∨), and NOT (¬).

A quantiﬁer block qb of Q is a maximal contiguous subsequence of Q where every variable in qb has the same quantiﬁer type. The quantiﬁer blocks are ordered by their appearance in Q: qb 1 ≤ qb2 iff qb 1 is equal to or appears before qb 2 in Q. Each variable 414 A. Goultiaeva, V. Iverson, and F. Bacchus x in φ appears in some quantiﬁer block qb(x). For two variables x and y we say that y is downstream of x (x is upstream of y) if qb(y) qb(x) (qb(x) qb(y)). We also say that x is universal (existential) if its quantiﬁer in Q is ∀ (∃).

A QBF instance can be reduced by a literal (i.e., an assignment to one of its variables). The reduction of a formula Q.φ by is denoted by Q.φ|. The reduction is the new formula Q.φ where φ is φ with v replaced by the constant TRUE (if = v) or FALSE (if = ¬v), and optionally simpliﬁed according to standard logical rules: e.g., for any formula ψ, FALSE ∧ ψ is equivalent to FALSE and ∀x.ψ is equivalent to ψ if the variable x does not appear in ψ. A speciﬁc example is ∀xz.∃y.(¬y ∨ (x ∧ z)) ∧ ¬(x ∨ z)|¬x which is equal to ∀xz.∃y.(¬y ∨ (FALSE ∧ z)) ∧ ¬(FALSE ∨ z) which simpliﬁes to ∀z.∃y.¬y ∧ ¬z.

Semantically, the truth or falsity of a QBF formula (with no free variables) can be dened recursively: (1) ∀xQ.φ is true iff both Q.φ|x and Q.φ|¬x are true, and (2) ∃xQ.φ is true iff at least one of Q.φ|x or Q.φ|¬x is true. By instantiating the quantiﬁed variables one by one, following the quantiﬁer ordering, and substituting true or false into φ we arrive at either a QBF where φ simpliﬁes to FALSE (which is a false QBF) or a QBF where φ simpliﬁes to TRUE (which is a true QBF).

A circuit is a directed acyclic graph with a single sink where the nodes are logical gates and the edges are signal lines connecting the gates. Each gate is either an AND, OR, or NOT gate, has a single outgoing output line, and one or more incoming input lines. The output line of the sink gate is the circuit output, and the lines that are not outputs of any gate are the circuit inputs. A circuit representation Q.C for the QBF formula Q.φ is a circuit C where the variables in Q are in 1-1 correspondence with the circuit inputs. C can be constructed recursively as follows. If φ is a variable x, then C has only one line labeled by the variable x and no gates. If φ = ¬ψ, then C consists of the circuit representing ψ with the output of this circuit connected to the input of a NOT gate. If φ = ψ1 ∧ · · · ∧ ψi (ψ1 ∨ · · · ∨ ψi ), then C consists of the outputs of the circuits representing ψ1 to ψi connected as inputs of an AND (OR) gate. One key feature of the circuit representation is that duplicated sub-formulas in φ can be represented by a single subcircuit—the output line of that subcircuit can be used as an input in all places the sub-formula appears.

The lines of a circuit can take on the values TRUE or FALSE, and these values can be propagated to other lines of the circuit using standard rules of Boolean logic.

For example, if an input line of an AND gate has value FALSE then FALSE can be propagated to the output line of the gate. A circuit Q.C represents a formula Q.φ when for any setting of the variables in φ, φ will simplify to TRUE (FALSE) if and only if TRUE (FALSE) is propagated to the output of C given the same setting for its corresponding input lines. The construction described above yields a circuit C that represents φ.

Hence, we can evaluate a QBF formula Q.φ by constructing a circuit Q.C representing it, and then evaluating the previously given deﬁnition of truth for a QBF formula by propagating values in C. That is, we can detect when φ simpliﬁes to TRUE or FALSE by detecting when TRUE or FALSE is propagated to the output line of C.

Beyond CNF: A Circuit-Based QBF Solver 415 3 A Circuit-Based Solver Similar to previous circuit based SAT solvers, e.g., [7,8], our solver utilizes DPLL search to determine the truth or falsity of the QBF Q.φ. Speciﬁcally, φ is represented as a circuit C with the variables in Q being the inputs to C. During DPLL search, these variables are branched on in an order respecting the quantiﬁer ordering (i.e., if x is upstream of y then the search must branch on x before y). Each branch sets a variable of φ and hence a corresponding input line of C. The input line values are propagated through C, and the search veriﬁes that at least one side each existential branch and both sides of each universal branch lead to a true circuit output (i.e., satisﬁes φ).

However, to make this process more efﬁcient, e.g., to detect when certain input lines must take on a particular value for the circuit output to be TRUE, the solver initially sets the circuit output line to TRUE and propagates values backwards in the circuit as well as forwards. Backwards propagation, like forward propagation, follows the rules of Boolean logic, e.g., if an OR gate’s output line is set to FALSE then FALSE can be propagated to all of its input lines. With backward propagation from a TRUE output we can detect when φ is falsiﬁed (i.e., when a setting of the input lines would lead to FALSE being propagated to the output line) by the occurrence of a conﬂict where both TRUE and FALSE is propagated to some line in the circuit. Such conﬂicts also allow us to employ 1UIP clause learning techniques on the circuit representation.

One negative aspect of ﬁxing the circuit output line to TRUE, however, is that we can no longer use the propagation of TRUE to the circuit output to detect when the formula φ has become satisﬁed by the current setting of its variables—the output line always has that value. We discuss below how this problem is resolved in our solver by utilizing information gathered during don’t care propagation.

3.1 Propagation Our implementation of forward and backward propagation in the circuit is based on a previous circuit based SAT solver described in [7]. In that paper Thiffault et al. showed that this kind of propagation in the circuit corresponds in a precise way to Unit Propagation (UP) on an equivalent CNF encoding of the formula. In particular, if the circuit was converted to CNF using the standard Tseitin encoding [11], then corresponding to each circuit line l there would be a new variable v in the CNF encoding such that a value would be propagated to the line l in the circuit if and only if UP in the CNF forces v to take the same value. Besides this basic mechanism, however, our QBF solver differs from previous circuit based SAT solvers in a number of ways.

Representing internal lines. The CNF encoding of a formula introduces additional variables that correspond to the sub-formulas of the formula. These additional variables are very useful in a SAT solver as they can be branched on in a DPLL search (implicitly positing a truth value for an entire sub-formula), and they can be included in learnt clauses increasing the effectiveness of clause learning.

A key feature of our circuit based QBF solver is that it also utilizes the learning techniques common in DPLL based QBF solvers that employ CNF [12] i.e., clause and cube learning. Hence, to facilitate the power of the learnt clauses we introduce additional variables to label the internal lines of the circuit, as is done in circuit based SAT solvers. (The 416 A. Goultiaeva, V. Iverson, and F. Bacchus input lines are all labeled with a variable of the original formula Q.φ). Formally, all of these new variables are existential, and we place them as early in the quantiﬁer ordering as possible. Speciﬁcally, each internal line l in the circuit is the output line of a sub-circuit c that has some set of input lines representing a set of variables V of φ. We place the new variable representing l in the quantiﬁer preﬁx immediately after the last variable of V in the preﬁx. By placing these new variables as early as possible in the quantiﬁer preﬁx we enable more effective universal reduction during clause learning and propagation.

Note however that in QBF, unlike SAT, these new variables are never branched on during the DPLL search. The DPLL search must respect the quantiﬁcation order when selecting variables to branch on, so by the time it can select a variable v representing the output of sub-circuit c all of the inputs to c must have already been assigned, and hence v would already be assigned by propagation.