Efficient Symmetry Breaking for Boolean Satisfiability

1 Introduction

Modem Boolean satisfiability (SAT) solvers, based on back­ track search, are now capable of attacking instances with thousands of variables and millions of clauses [Velev and Bryant, 200 I] and are being routinely deployed in a wide range of industrial applications [Biere eta/., 1999], [Nam et a/., 2001], [Stephan eta/. , 1996]. Their success can be cred­ ited to a combinational of recent algorithmic advances and carefully-tuned implementations [Silva and Sakallah, 1999], [Moskewicz et a/., 2001], [Goldberg and Novikov, 2002]. Still, there are problem instances that remain beyond the reach of most SAT solvers.

One aspect of intractability is the presence of symmetry in the conjunctive normal form (CNF) of a SAT instance. Intuitively, a symmetry of a discrete object is a transforma­ tion, e.g., a permutation, of its components that leaves the object intact. The symmetries of a CNF formula are permu­ tations of its literals (variables and their negations) that result in a re-ordering of its clauses (and the literals within clauses) without changing the formula itself. Such symmetries induce an equivalence relation on the set of variable assignments such that two assignments are equivalent if and only if the formula assumes the same truth value (either 0 or 1) at each of these assignments. A search algorithm that is oblivious to the existence of these symmetries may end up, wastefully exploring a set of equivalent unsatisfying assignments before moving on to a more promising region of the search space.

On the other hand, knowledge of the symmetries can be used to significantly prune the search space. Symmetries are stud­ ied in abstract algebra in terms of groups. We assume. the reader to be familiar with the basics of group theory; in par­ ticular, we assume familiarity with permutation groups and their representation in terms of irredundant sets of genera­ tors. A good reference on the subject is [Fraleigh, 2000].

The rest of the paper is organized in five sections. Section 2 provides a brief review of permutations and per­ mutation groups. Section 3 describes pervious work on sym­ metry breaking for SAT. Our main contribution on efficient constructions of symmetry-breaking predicates is detailed in Section 4. These constructions are evaluated empirically in Section 5, and we end with conclusions in Section 6.

2 Notation and Preliminaries

We will be concerned with permutations on the literals of a set of n Boolean variables {x1 , ·. · , xn} which we assume to be totally ordered according to x 1 -< x 2 -< · · · -< x" . We use In to denote the set of integers between I and n inclusive, and denote non-empty subsets of In by upper-case "index variables" I and J as appropriate. Given an index set I and an index i E I, we define the "index selector" functions:

where min and max return, respectively, the least and great­ est element in the given index set. For completeness, we also let min(0) = n +I, and max(0 ) = 0.

A permutation 1r of the set of 2n literals L = {x 1 , xi , ... , xn, x~} (where xj denotes the logical negation of X;) is a function 1r: L ---+ L that is both one-to­ one and onto. We will denote that x 1 is the image of X; under 1r by writing x 1 = x~ . To preserve Boolean consistency, whenever 1r maps X; to x 1 it must simultaneously map xj to xj . Such implied mappings will be assumed whenever not explicitly specified. A permutation 1r is a phase-shift permutation if x~ = xj for some i E In , i.e., 1r maps some literal to its complement.

Permutations will be expressed either in tabular form or in cyclic notation. For example,

denotes a permutation that maps x 1 to x~ etc. The same per­ mutation can be expressed as a set of disjoint cycles such as

Here a cycle (a , b , 00 . , z) is a shortcut for "a maps to b, b maps to c, .. . and z maps to a." The length of a cycle is equal to the number of literals in it; we will refer to a cycle whose length is k as a k-cycle. We define the support of a permutation 1r , supp( 1r) , to be the set of indices appearing in its cyclic representation, i.e.,

The number of cycles in a permutation n will be denoted by cycles(-rr) . We also define phase-shift(-rr) to be the index of the smallest variable (according to the assumed total order­ ing) that is mapped to its complement by n :

We should note that a phase-shift permutation must have one or more phase-shift cycles, i.e. , length-2 cycles that have the form (x;, x j) . Finally, we define ends( -rr) as follows :

A permutation group G is a group whose elements are permutations of some finite set and whose binary operation is function composition, also referred to as permutation mul­ tiplication. The order of a group is the number of its ele­ ments. A subgroup H of a group G, denoted H:::; G is a subset of G that is closed under the group's binary operation. The cyclic subgroup of n E G, denoted by <-rr> , is the sub­ group consisting of n and its integer powers:

and n is said to generate <-rr> . A set of permutations n 1 E G , . .. , n k E G generates G if the subgroup resulting from taking all possible products of the integer powers of these permutations is equal to G. The permutations { n 1 , .. . , n k} are called generators of G. A set of genera­ tors is irredundant if it is not possible to express any of its permutations as a product of powers of its other permuta­ tions. A set of irredundant generators serves as an implicit representation of the group it generates and, in general, guar­ antees exponential compression in the size of the representa­ tion. Note that a set of irredundant generators is not a group since it is not closed under multiplication and taking inverse. In the sequel, a set of permutations G that is not necessarily closed will be indicated _by placing a "hat" on the variable denoting the set, i.e., G . Additionally, and with a slight abuse of !lotation, we will indi.cate that G is the group gener­ ated by G by writing G = < G > .

3 Previous Work

The basic framework for utilizing the symmetries in a CNF instance to prune the search space explored by a SAT solver was laid out in [Crawford et al., 1996]. This framework was extended later, in [Aloul et al., 2002], to account for phase­ shift symmetries, take advantage of the cycle structure of permutations, and consider only generators of the group of symmetries. In outline, the procedure consists of the follow­ ing steps:

1. Convert a CNF formula <p to a colored graph whose sym­ metries are isomorphic to the symmetries of the formula.
2. Find the symmetries of the graph in terms of a set of irredundant generators (; = {-rr 00. n } using a suitable graph )' ' k automorphism program [McKay, 1981 ], [Spitznagel, 1994].
3. Map the graph symmetries back to symmetries of the formula.
4. Construct an appropriate symmetry-breaking predicate (SBP) p and conjoint it to the formula.
5. Solve <pA p using a suitable SAT solver [Moskewicz et a/.,2001].

Our concern in this paper is step 4. Noting that the group of symmetries induces an equivalence relation on the set of assignments in the n-dimensional Boolean space, the basic idea is to construct a "filter" that picks out a single represen­ tative from each equivalence class. In particular, choosing the lexicographically smallest representative-according to the assumed total ordering on the variables-leads to the fol­ lowing Lex-Leader SBP [Crawford et al., 1996]:

where the index set I in (9) and (10) is equal to In . In these equations, the Lex-Leader SBP is expressed as a conjunction of permutation predicates o/Ps) each of which is a conjunc­ tion of bit predicates (BPs) . Introducing n auxiliary "equal­ ity" variables e; = (x; = x; ) makes it possible to express the ith BP as an (i + I)-literal CNF clause. This leads to a CNF representation of the PP in (9) that has n clauses with a total literal count of 0.5(n 2 + 3n). Additionally, each of the intro­ duced equality constraints yields 4 3-literal clauses bringing the total CNF size of (9) to:

In its present form, the lex-leader SBP in (8)-(1 0) can lead to an exponentially large CNF formula because the order of the symmetry group can be exponential in the number of variables. Thus, its value in pruning the search space is negated by the need of the SAT solver to process a much larger CNF formula. To remedy this problem [Crawford et al., 1996] suggested the construction of a symmetry tree to eliminate some redundant permutations. However, in the worst case the number of symmetries in the tree remains exponential. Empirical evidence in [Aloul et al. , 2002]

1 Note that x ~ y in the bit predicate means "x implies y".

(a) Permutation in tabular and cyclic notation

( BP(7r , 4) = (x 1 = x4)(x 2 = x 2 )(x 3 = x 8 )-+ (x4 ::; x 1 ) )

BP( 1r , 5) = (x 1 = x4)(x 2 = x 2 )(x 3 = x 8 )(x4 = x 1 ) -+ (x 5 ::; x5)

I BP( 1r , 10) = (x 1 = x4)(x2 = x 2 )(x 3 = x8)(x4 = x 1 )(x5 = x5 )(x6 = x] )(x1 = x1 )(x 8 = x6 )(x9 = x9) -+ (x 10 < x 10 ) I

(c) Btt predicates accordmg to (10). BPs enclosed m boxes with square comers are tautologous because 1r maps the corre­ sponding bits to themselves. BPs enclosed in boxes with rounded comers are tautologous because they correspond to cycle "ends." The BPs for bits 6 to 10 are tautologous because 1r maps bit 5 to its complement.

Figure I: Illustration of different formulations of the permutation predicate.

showed that full symmetry breaking, i.e., insuring that the whose size is linear, rather than quadratic, in m. Figure 1

SBP selects only the lex-leader from each equivalence class, provides an example illustrating these refinements. is not necessary to obtain significant pruning of the search space. An SBP that breaks some, but not necessarily all, the symmetries of the formula can, in fact, provide a much better space/time trade-off during the search. This is accomplished by replacing the group of symmetries in (8) by a suitable, and much smaller, set of permutations iJ ~ < G > :

In particular, [J\loul eta!., 2002] advocated the use of the set of generators G returned by the graph automorphism pro­ gram in step 2.

4 Efficient Formulation of Permutation Predicate

Even when only a small number of permutations is used in constructing an SBP as in (12), the corresponding CNF for­ mula may still be too large because each PP requires a CNF formula whose size is quadratic in the number of variables n. In this section we introduce two refinements that lead to much smaller PPs. The first refinement utilizes the cycle structure of a permutation to eliminate redundant bit predi­ cates and can be viewed as replacing n in ( 11) by a much smaller number m and represents a more comprehensive and systematic treatment of cycles than that in [Aloul et a!. , 2002]. The second refinement takes advantage of the recur­ sive bit-by-bit structure in (1 0) to yield a CNF formula Elimination of redundant BPs. Careful analysis of (10) reveals three cases in which a BP is tautologous, and hence redundant. The first corresponds to bits that are mapped to themselves by the permutation, i.e., x7 =X;. This makes the consequent of the implication in ( 1 0), and hence the whole bit predicate, unconditionally true. Removal of such BPs is easily accomplished by setting the index set I in (9) and (10) to supp( 1r) rather than In. For sparse permutations, i.e. , per­ mutations for which lsupp(1r)l « n, this change alone can account for most of the reduction in the CNF size of the PP.

The second case corresponds to the BP of the last bit in each cycle of 1r . "Last" here refers to the assumed total ordering on the variables. Assume a cycle involving the vari­ ables {x 1 v E J} for some index set J and let i = max(J). Then

causing the corresponding bit predicate BP( 1r , i) to be tau­ tologous. Elimination of these BPs is accomplished by restricting the index set I in (9) and (10) further to just supp(1r) "- ends(1r) and corresponds to a reduction in the number of BPs from n to m = lsupp( 1r)l- cycles( 1r).

The third and last case corresponds to the BPs of those bits that occur after the first "phase-shifted variable." Let i be the index of the first variable for which x7 = xj . Thus, e; = 0 and all BPs for j > i have the form 0 ~ (x 1 S:: x;) making them unconditionally true.

Taken together, the redundant BPs corresponding to these three cases can be easily eliminated by setting the index set in (9) and (10) to:

In the sequel we will refer to the bits in the above index set as "irredundant bits." Note that the presence of a phase­ shifted variable early in the total order can lead to a drastic reduction in the number of irredundant bits. For example, if 1r = (x 1 , x' 1 ) . . · then PP( 7r) is simply ( x~ ) regardless of how many other variables are moved by 1r .

Linear construction of PPs through chaining. The PP in (9) and (10) has a recursive structure that can be utilized to produce a CNF formula whose size is linear, rather than qua­ dratic, in the cardinality of the index set I. Specifically, we introduce the "ordering" predicates I;= (x;::::; x7) and g; = (x; ~ x7) and, after algebraic manipulation, write the following equivalent expressions for the permutation predi­ cate:

where g 0 = I, k = next(O , I) and K = succ(k, I). Noting that, except for the index set used, the parenthesized expres­ sion on the second line of the above equation is identical to the expression on the first line, we introduce a sequence of chaining predicates {p;li E I} defined according to:

where K = { i} U succ(i, I)= {k E II k ~ i}. The recursive structure of (15), now, makes it possible to express each chaining predicate in terms of the one that follows it

and yields the following alternative representation of the per­ mutation predicate:

which can be simplified further by replacing the equalities by one-way implications leading, finally, to:

The CNF representation of each conjunct in (18) is obtained by substituting the definitions of the I and g variables and using the distributive law. Thus, using this construction the permutation predicate requires Ill additional variables (the chaining predicates) and consists of 2111 3-literal and 2111 4literal clauses for a total of 14111 literals.

5 Experimental Evaluation

We conducted a number of experiments to evaluate the effec­ tiveness of the symmetry breaking constructions described above in reducing search times. We ran the experiments on representative CNF instances from the following seven benchmark families:

1. Hole-n: Unsatisfiable pigeon-hole instances [DIMACS]
2. Urq: Unsatisfiable randomized instances based on expander graphs [Urquhart, 1987]
3. GRoute: Difficult satisfiable instances that model global wire routing in integrated circuits [Aloul eta/., 2002]
4. FPGARoute and ChniRoute: Large satisfiable and unsat­ isfiable, instances that model the routing of wires in the channels of field-programmable integrated circuits [Nam eta/., 2001]
5. XOR: Various exclusive-or chains [SAT 2002]
6. 2pipe: Difficult unsatisfiable instances that model the functional correctness requirements of modern out-of­ order microprocessor CPUs [Velev and Bryant, 2001]

Each of the benchmarks was converted to a colored graph as described in [Aloul eta/., 2002] and processed by the graph automorphism program Nauty (version 2) [McKay, 1981] using the GAP package (version 4, release 3) [Spitznagel, 1994]. The symmetries returned by Nauty were then mapped back to symmetries of the benchmark and appropriate SBPs constructed and added. The mChaff SAT solver [Moskewicz et a/., 2001] was then run on the original and SBP-aug­ mented versions of each benchmark. All experiments were run on a Linux workstation with a 1.2Ghz AMD Athlon pro­ cessor and 1GB of RAM. A time-out limit of 1000 seconds was set for all runs, and run time results represent averages over 10 to 200 independent runs.

Table I lists, for each benchmark family, the number of instances tested (col. 2), their total CNF sizes (cols. 3 and 4), the order of their symmetry groups (col. 5), the total number of generators returned by Nauty (col. 6), and the number of those that include phase shifts (col. 7). Columns 8 and 9 list the cardinality of the generators' support and the degree of sparsity present in these generators. The remaining columns in the table list the CNF sizes of three SBP constructions based on generators:

• The quadratic construction (using extra equality variables) based on all bits; this represents the previous state-of-the­ art
• The quadratic construction based only on irredundant bits
• The linear construction (using extra chanining variables) based only on irredundant bits

Several observations can be made about the data in Table I. The number of symmetries in these benchmarks is large, but all symmetries, including phase shifts in bench­ mark families Urq, XOR and 2pipe, can be represented by fairly small sets of generators. The generators returned by Nauty appear very sparse on average, i.e., a typical generator affects only a small number of variables. 2 This explains the reduction, by 1-2 orders-of-magnitude, in the size of symme­ try-breaking predicates in column 13 (our first construction) versus column II ([Crawford eta/., 1996]). Both the number of variables and the number of literals are reduced. While our construction in column 13 only slightly extends the quadratic-size construction in [Aloul et a/., 2002], our more advanced linear-size construction (column 15) offers an additional reduction by up to an order of magnitude. Note, however, that the number of variables is unchanged-the extra variables added by the two constructions have different function, but can be mapped to each other one-to-one.

Table 2: Comparison of search run times for various choices of SBP constructions and symmetries to break.

Table 2 empirically compares the effectiveness of the symmetry-breaking predicates described in Table 1. First, in most cases it takes much less time to find symmetries of a CNF instance than to solve it. The 2pipe instances are an exception, but we believe that further advances in symmetry­ finding can rectify this exception. Second, the all-bits qua­ dratic construction due to [Crawford eta/., 1996] is dramati­ cally slower than our variants based on the cycle structure. Our linear-sized construction provides a further speed-up. Exceptions are the Hole-n benchmarks, where the difference between our two constructions is small, and the 2pipe bench­ marks where the quadratic-sized SBPs led to shorter run times despite being almost thirteen times larger. Further investigation showed that this was a side-effect of mChaff's VSIDS decision heuristic which tended to choose the auxil­ iary variables first because they occur in many more clauses than the original instance variables. Using BerkMin [Goldberg and Novikov, 2002] or GRASP [Silva and Sakallah, 1999] in the same experiment yielded opposite results as expected. _

2 While our experiments clearly confirm that such generators exist, finding them is a function of the graph automorphism program. Since we used Nauty as a black box, we do not have a clear expla­ nation of what causes Nauty to find such sparse generators, whether even sparser generators can be found and whether Nauty will in some cases return less sparse generators.

Table 2 offers additional data to evaluate symmetry­ breaking by generators, which may not be complete. We added symmetry-breaking predicates built for pairwise prod­ ucts of generators, but the overall runtimes increased. While additional SBPs may break more symmetries, their overhead does not justify their use.

Table 3 describes experiments with generators that have long cycles in which we evaluated extensions to symmetry­ breaking by generators. Namely, we tried adding powers of all generators and, alternatively, adding pairwise products of generators. Neither extension proved useful, which supports our main symmetry-breaking approach.

6 Conclusions

The main contribution of our work is a better construction of symmetry-breaking predicates for Boolean satisfiability. We empirically demonstrate improvements both in the size of predicates and the run time of SAT solvers after these predi­ cates are added to the original CNF instances. We also show that (I) symmetry-breaking by generators is difficult to improve upon, and that (2) the efficiency of symmetry­ breaking does not improve when larger cycles are found in generators.

Our work articulates that better symmetry finding algo­ rithms would be useful, especially if tailored to CNF formu­ las and, perhaps, the kinds of symmetry groups commonly found in structured CNF instances.

Acknowledgments

This work was funded by the DARPA/MARCO Gigascale Silicon Research Center and by an Agere Systems/SRC Research fellowship.