Balance and Filtering in Structured Satisfiable Problems

1 Introduction

The discovery of methods to generate hard random problem instances has driven progress on algorithms for propositional deduction and satisfiability testing. Gomes & Selman (1997) introduced a generation model based on the quasigroup (or Latin square) completion problem (QCP). The task is to determine if a partially colored square can be completed so that no color is repeated in any row or any column. QCP is an NP-complete problem, and random instances exhibit a peak in problem hardness in the area of the phase transition in the percentage of satisfiable instances generated as the ratio of the number of uncolored cells to the total number of cells is varied. The structure implicit in a QCP problem is similar to that found in real-world domains: indeed, many problems in scheduling and experimental design take the form of a QCP. Thus, QCP complements earlier simpler generation models, such as random CZ-cnf (Mitchell et al. 1992). Like them QCP generates a mix of satisfiable and unsatisfiable instances.

In order to measure the performance of incomplete solvers, it is necessary to have benchmark instances that are known to be satisfiable. This requirement is problematic in domains where incomplete methods can solve larger instances than complete methods: it is not possible to use a complete method to filter out the unsatisfiable instances. It has proven difficult to create generators for satisfiable CZ-sat. Achlioptas et

Carla Gomes Bart Selman

Dept. of Comp. Sci. Cornell Univ. Ithaca, NY 14853 gomes@cs.cornell.edu

selman@cs.cornell.edu

Mark Stickel

Artificial Intelligence Center SRI International Menlo Park, California 94025

stickel@ai.sri.com

al. (2000) described a generation model for satisfiable quasigroup completion problems called "quasigroups with holes" (QWH). The QWH generation procedure basically inverts the completion task: it begins with a randomly-generated completed Latin square, and then erases colors or "pokes holes". The backbone of a satisfiable problem is the set of variables that receive the same value in all solutions to that problem. Achlioptas et al. (2000) showed that the hardest QWH problems arise in the vicinity of a threshold in the average size of the backbone.

Despite the similarities between the filtered QCP and QWH models the problem distributions they generate are quite different. As noted by Achlioptas et al. (AAAI 2000), the threshold for QCP is at a higher ratio of holes than is the threshold for QWH. But even more significantly, we discovered that the hardest problems obtained using the filtered QCP

model are about an order of magnitude more difficult to solve than the hardest one obtained using the QWH model. Figure 1 illustrates the difference for the incomplete local search solver Walksat (Selman et al. 1992). (The critical parameter for a fixed order D2 is the percentage of holes (uncolored squares) in the problem. In all of the graphs in this paper the DCA0axis is re-parameterized as the number of holes divided by D2 BDBMBHBH . Achlioptas et al. (2000) demonstrates that this re-parameterization adjusts for different problem sizes.) The first two lines of Table 1 compare the peak hardness of QWH and filtered QCP for Walksat and two complete systematic solvers, Satz (Li & Anbulagan 1997) and Sato (Zhang 1997). These solvers are running on Boolean CNF encodings of the problem instances. The performance of such modern SAT solvers on these problems is competitive with or superior to the performance of optimized CSP solvers running on the direct CSP encoding of the instances (Achlioptas et al. 2000). (Note that the number of backtracks performed by Satz is usually much lower than the number performed by other systematic algorithms because of its use of lookahead.)

We begin by explaining this difference in hardness by showing how each generation model is biased away from the uniform distribution of all satisfiable quasigroup completion problems. Next, we introduce a new satisfiable problem model, balanced QWH, which creates problems that are even harder than those found by filtered QCP, as summarized in the last line of Table 1. This new model provides a tool for creating hard structured instances for testing incomplete solvers. In addition, its simplicity and elegance suggests that it will provide a good model to use for theoretical analysis of structured problems.

In the final section of the paper we turn to the issue of how we encode the quasigroup problems as Boolean satisfiability problems. For systematic methods the best encoding is based on a view of a quasigroup as a 3-dimensional cube, rather than as a 2-dimensional object. As shown below, the 2-D encodings are almost impossible to solve by systematic methods for larger orders. This difference is not unexpected, in that the 3D encodings include more redundant constraints, which are known to help backtracking algorithms. For Walksat, however, a more complex picture emerges: the hardest instances can be solved more quickly under the 2-D encoding, while under-constrained instances are easier under the 3-D encoding.

2 The QWH and Filtered QCPModels

In order to better understand the QWH and filtered QCP models we begin by considering the problem of choosing a member uniformly at random from the set of all satisfiable quasigroup completion problems of order D2 with CW uncolored cells. It is easy to define a generator for the uniform model: (1) Color D2 BE A0CW cells of an order D2 square randomly; (2) Apply a complete solver to test if the square can be completed; if not, return to step (1). This generator for the uniform model is, however, impractical for all but largest values of CW. The problem is that the probability of creating a satisfiable instance in step (1) is vanishingly small, and so the generator will loop for an exponentially long time. In other words, the set of satisfiable quasigroup completion problems, although large, is small relative to the set of all completion problems.

Because the instances generated by placing down random colors are almost certainly unsatisfiable, the quasigroup completion generator from Gomes & Selman (1997) tries to filter out as many unsatisfiable configurations while incrementally partially coloring a square. The formulation is in terms of a CSP, with a variable for each cell, where the domain of the variable is initialized to the set of D2 colors. The generator repeatedly selects an uncolored cell at random, and assigns it a value from its domain. Then, forward-checking is performed to reduce the domains of cells that share a row or column with it. If forward-checking reaches an inconsistency (an empty domain) the entire square is erased and the process begins anew. Otherwise, once a sufficient number of cells have been colored arc consistency is checked; if the square passes this test, then it is output. The hardest mix of sat and unsat instances is generated when the number of holes is such that about 50% of the resulting squares are satisfiable. Because of it's popularity in the literature, we simply call the distribution generated by the process the QCP model. Adding a final complete solver to check satisfiability and eliminating those square which are unsatisfiable results in the filtered QCP model. 1

The hardest hole ratio for the filtered QCP model is shifted toward the more constrained side. We discovered that hardest satisfiable instances occur when the filtering step eliminates about 90% of the partial Latin squares.

While the use of incremental forward checking successfully biases QCP away from unsatisfiable problems, it also has the unintended effect of introducing a bias between different satisfiable instances. For a simple example, consider generating order 2 problems with 2 holes, where the colors are R and G. Without loss of generality, suppose the first step of the algorithm is to color the top left square R. As shown in Figure 2, forward-checking reduces the domains of two of the remaining cells. The next step is to pick one of the three remaining cells at random, and then choose a color in its domain at random. As a result, one of the four partial Latin squares shown in the figure is created, but with different probabilities: the first two with probability BDBPBF each, and the last two with probability BDBPBI each. The fourth square is immediately eliminated by the final forward checking step. Because our choice of initial square and color was arbitrary, we see that each of the partial Latin squares where the two colored cells are in the same row or column is twice as like to be generated as one in which the two colored cells appear on a diagonal.

The QWH model introduced by Achlioptas et al. (2000) works as follows: (1) A random complete Latin square is created by a Markov-chain process; (2) CW random cells are uncolored. Does this generate the uniform model? Again the answer is no. Because all patterns of CW holes are equally likely to be generated in step (2), we can without loss of generality consider both the number and pattern of holes to be fixed. The probability of creating a particular completion problem is proportional to the number of different complete Latin squares that yield that problem under the fixed pattern of holes. Therefore, we can show that QWH does not generate the uniform model by simply presenting two partial Latin squares with the same pattern of holes but a different number of solutions.

1 The QCP generator used in Gomes & Selman (1997) did not perform the final arc-consistency test. Thus, it generated a higher percentage of unsatisfiable instances. The filtered (satisfiable) distribution from that generator and ours are identical.

Such a counterexample appears in Figure 3: The square on the left has two solutions while the one on the right has only a single solution. In other words, the left square is twice as likely to be generated as the right square. In general, the QWH model is biased towards problems that have many solutions.

3 Patterns and ProblemHardness

We now consider different models of QCP and QWH, corresponding to different patterns. As we will see, the complexity of the models is dependent not only on the number of uncolored cells but also on the underlying pattern.

3.1 Rectangular and AlignedModels

In order to establish a baseline, we first consider two tractable models for QCP and QWH, which we refer to as rectangular and aligned models. Figure 4 (left and middle) illustrates such instances. In the rectangular QWH model, a set of columns (or rows) is selected and all the cells in these columns are uncolored. Moreover, one additional column (row) can be selected and be partially uncolored. The aligned QWH model is a generalization of the rectangular model in that we can pick both a set of rows and a set of columns and treat them as the chosen rows/columns in the rectangular model. Put differently, in the aligned model, the rows and columns can be permuted so that all cells in BV BP CUBDBN BM BM BM BN D6 A0 BDCV A2 CUBDBN BM BM BM BN D7 A0 BDCV are colored, some cells of CUBDBN BM BM BM BN D6CV A2 CUBDBN BM BM BM BN D7CV D2 BV are colored and all other cells are uncolored. We note that one could also naturally generate rectangular and aligned QCP instances.

In order to show that both the rectangular and aligned models are tractable, let us consider a Latin rectangle R on symbols BDBN A1 A1 A1 BN D2. Let R(i) denote the number of occurrences of the symbol CX in R, BD AK CX AK D2BM We first introduce the following theorem from combinatorics.

Theorem: (Ryser 1951) An D6 x D7 Latin rectangle R on symbols BDBN A1 A1 A1 BN D2 can be embedded in a Latin square of side D2 if and only if

Theorem: Completing a rectangular QCP or QWH is in P.

Proof: We can complete the rectangular QCP or QWH instance column by column (or row by row), starting with the column (or row) partially uncolored. (If there is no partially uncolored columns or rows, consider an arbitrary fully uncolored column or row.) We construct a bipartite graph BZ, with parts CD BP CUD9 BD BN D9 BE BN BM BM BM BN D9 D1 CV, and CF BP CUDB BD BN DB BE BN BM BM BM BN DB D1 CV in the following way: CD represents the uncolored cells of the column (row) that needs to be colors; CF represents the colors not used in that column (row). An edge (D9 CX ,DB CY ) denotes that node D9 CX can be colored with color DB CY . To complete the first column (row) we find a perfect matching in BZ. If there is no such matching we know that the instance is unsatisfiable. After completing the first column (row), we can complete the remaining columns (rows) in the same way. BXBW

Theorem: Completing an aligned QCP or QWH is in P.

Proof: We start by noting that an aligned instance can be trivially rearranged into an D6 x D7 rectangle, D7 AK D2, by permutating rows and columns (with possibly a row or column partially uncolored). So, if we show that we can complete an D6 x D7 rectangle into an D6 x D2 rectangle, we have proved our theorem, since we obtain an instance of the rectangular model. To complete an D6 x D7 rectangle into an D6 x D2, again we complete a column (or row) at a time, until we obtain a rectangle of side D2. For the completion of each column (or row), again, we solve a matching on the bipartite graph. The only difference resides in the way we build the graph: CF only contains colors for which the condition in Ryser's theorem is satisfied. BXBW

3.2 Balance

While the rectangular and aligned models cluster holes, we now turn to a model that attempts to increase problem hardness by minimizing clustering. Let us start by reviewing the role of balance in the two most studied combinatorial optimization problems over random structures: random satisfiability and random graph coloring. It is particularly interesting to note the features shared by algorithms performing well on these problems.

Random CZ-SAT. A random formula is formed by selecting uniformly and independently D1 clauses from the set of all BE CZ A0 D2 CZ A1 CZ-clauses on a given set of D2 variables. The first algorithm to be analyzed on random CZ-SAT employs the pure literal heuristic repeatedly: a literal CO is satisfied only if AM CO does not appear in the formula. Thus, a pure variable has all its occurrences appear with the same sign - a rather dramatic form of sign imbalance. The next key idea is unit-clause propagation, i.e., immediately satisfying all clauses of length 1. More generally, dealing with shortest clauses first has turned out to be very useful. Subsequent improvements also come from exploiting imbalances in the formula: using degree information to determine which variable to set next and considering the number of positive and negative occurrences to determine value assignment.

Bayardo & Schrag (1996) gave experimental results on the role of balance, by considering random CZ-SAT formulas in which all literals occur in the same number of clauses. In such formulas, an algorithm has to first set a non-trivial fraction of all variables (essentially blindly) before any of the ideas mentioned above can start being of use. This suggests the potential of performing many more backtracks and indeed, balanced random CZ-SAT formulas are an order of magnitude harder than standard ones.

Random graph coloring. A random graph on D2 vertices is formed by including each of the A0 D2 BE A1 edges with probability D4. For graph coloring the most interesting range is D4 BP CSBPD2, where CS is a constant. One can also consider list-coloring, where each vertex has a prescribed list of available colors. Analogously to the pure literal heuristic, a first idea is to exploit the advantage offered by low degree vertices. In particular, if we are using CZ colors then we can safely remove from the graph all vertices having degree smaller than CZ: if we can color the remaining graph then we can certainly complete the coloring on these vertices since each one of them will have at least one available color (as it has at most CZ A0 BD neighbors). Upon potentially reaching a CZ-core, where every vertex has degree at least CZ, it becomes useful to consider vertices having fewest available colors remaining and, among them, those of highest degree. Conversely, random graphs that are degree-regular and with all lists having the same size tend to be harder to color.

3.3 Balance in RandomQuasigroups

In the standard QWH model we pick a random quasigroup and then randomly turn a number of its entries to holes. Fixing the quasigroup choice and the number of holes, let us consider the effect that different hole-patterns have on the hardness of the resulting completion problem. (For brevity, we only refer to rows below but naturally all our comments apply to columns just as well.)

Two extreme cases are rows with just one hole and rows with D2 holes. In the first case, the row can be immediately completed, while in the second case it turns out that given any consistent completion of the remaining D2 A2 B4D2 A0 BDB5 squares one can always complete the quasigroup. More generally, it seems like a good idea for any algorithm to attempt to complete rows having a smallest number of holes first, thus minimizing the branching factor in the search tree. Equivalently, having an equal number of holes in each row and column should tend to make things harder for algorithms.

Even upon deciding to have an equal number of holes in each row and column, the exact placement of the holes remains highly influential. Consider for example a pair of rows having holes only in columns CXBN CY and further assume that there are no other holes in columns CXBN CY. Then, by permuting rows and columns it is clear that we can move these four holes to, say, the top left corner of the matrix. Note now that in this new (isomorphic) problem the choices we make for these four holes are independent of all other choices we make in solving the problem, giving us a natural partition to two independent subproblems.

More generally, given the 0/1 matrix BT where zeros correspond to colored entries and ones correspond to holes, one can attempt to permute the rows and columns to minimize the bandwidth of BT (the maximum absolute difference between CX and CY for which BTB4CXBN CYB5 is 1). Having done so, the completion problem can be solved in time exponential in the bandwidth.

We were surprised to discover that even though Satz contains no code that explicitly computes or makes use of bandwidth (indeed, exactly computing the bandwidth of a problem is NP-complete), it is extremely efficient for boundedbandwidth problems. We generated bounded-bandwidth instances by first punching holes in a band along the diagonal of a Latin square, and then shuffling the rows and columns 1,000 times to hide the band. Satz solved all instances of this type for all problem sizes (up to the largest tested, order 33) and hole ratios in either 0 or 1 backtrack! Satz's strategy is Davis-Putnam augmented with one-step lookahead: this combination is sufficient to uncover limited-bandwidth instances.

When the holes are placed randomly then with high probability the resulting matrix BT will have high bandwidth. Alternatively, we can view BT as a random D2 A2 D2 bipartite graph in which vertex CX is connected to vertex CY iff there is a hole in position B4CXBN CYB5. The high bandwidth of BT then follows from relatively standard results from random graph theory (Fernandez de la V´ ega 1981). Moreover, having an equal number of holes in each row/column makes the random graph regular, which guarantees that BT has large bandwidth. Intuitively, small balanced instances should exhibit properties that hold of large random instances in the asymptotic limit.

Viewing the hole pattern as a regular random bipartite graph readily suggests a way for generating a uniformly random hole pattern with precisely D5 holes in each row and column for any D5 (i.e., D5 BP CWBPD2) by the following algorithm:

Set  BP BN. Repeat D5 times: Set CC to CUBDBN BM BM BM BN D2CV A2 CUBDBN BM BM BM BN D2CV D2 . Repeat D2 times: Pick a uniformly random B4CXBN CYB5 BE CC ; Add B4CXBN CYB5 to ;

Remove all elements in row CX and column CY from CC .

Balancing can be applied to either the QWH or QCP models: in the former, the pattern is used to uncolor cells; in the latter, the pattern is used to determine the cells that are not colored incrementally.

3.4 Empirical Results

We measured the difficulty of solving problem distributions generated under each of the models using three different algorithms. As a preliminary step problems were simplified by arc consistency and then translated into SAT problems in conjunctive normal form, as described in Sec. 4 below. For each data point for a range of percentage of holes 100 problems were generated and solved by three different algorithms: Walksat, which performs local search over the space of truth assignments, using 30% noise and no cutoff; Satz, which implements the backtracking Davis-Putnam algorithm augmented with 1-step lookahead; and Sato (Zhang 1997), another Davis-Putnam type solver that uses dependencydirected backtracking and clause learning. In this paper we present the data for order 33, a size which clearly distinguishes problem difficulty but still allows sufficient data to be gathered. For reasons of space, we will omit detailed results for Sato, which are qualitatively similar to those for Satz.

Figure 5 displays the results for Walksat: note the log scale, so that each major division indicates an order of magnitude increase in difficulty. Less constrained problems appear to the right in the graphs: note that is the opposite of the convention for presenting results on random CZ-cnf (but is consistent with Achlioptas et al. (2000)). On the log scale we see that the most constrained instances are truly easy, because they are solved by forward-checking alone. The underconstrained problems are of moderate difficulty. This is due to the fact that the underconstrained problem are simply much larger after forward-checking. Again note that this situation is different from that of random CZ-cnf, where it is the overconstrained problems that are of moderate difficulty (Cook and Mitchell 1997).

At the peak the balanced QWH problems are much harder than the filtered QCP problems, showing that we have achieved the goal of creating a better benchmark for testing incomplete solvers. Balancing can be added to the filtered QCP model; the resulting balanced QCP model are yet more difficult. This indicates that balancing does not make QWH

and QCP equivalent: the biases of the two approaches remain distinct. Both of the QWH models are harder than the QCP models in the under-constrained region to the right; we do not yet have an explanation for this phenomena.

Both the aligned and rectangle models are easy for Walksat, and show no hardness peak. In the over-constrained area (to the left) they require more flips to solve than the others. This is because clustering all the holes prevents arc consistency from completely solving the problems in the overconstrained region (there are more than one solutions), as it usually does for the other models.

Figure 6 shows the same ordering of hardness peaks for Satz. The behavior of Satz on the rectangle case is an interesting anomaly: it quickly becomes lost on the underconstrained problems and resorts to exhaustive search. This is because Satz gains its power from lookahead, and on under-constrained rectangular problems lookahead provides no pruning. Sato, which employs look-back rather than lookahead, does not exhibit this anomaly: it solves the rectangular problems as easily as the aligned ones.

We also measured the variance in the number of holes per row or column and the bandwidth of the balanced and randommodels. As expected, the variance was very low for the balanced case, averaging between 0.0 and 0.2 over the rage of ratios, compared with a range of 5.4 to 8.2 for the random case. Thus non-balanced problems will often have rows or columns that contain only a few, highly-constrained holes that can be easily filled in.

4 3-D and 2-D Encodings

Up to this point of the paper we have been concerned with understanding what makes a problem intrinsically hard. In practice, the difficulty of solving a particular instance using a particular algorithm is also dependent upon the details of the representation of the problem.

Although quasigroup completion problems are most naturally represented as a CSP using multi-valued variables, encoding the problems using only Boolean variables in clausal form turns out to be surprisingly effective. Each Boolean variable represents a color assigned to a cell, so where D2 is the order there are D2 BF variables. The most basic encoding, which we call the "2-dimensional" encoding, includes clauses that represent the following constraints:

1. Some color must be assigned to each cell;
2. No color is repeated in the same row;
3. No color is repeated in the same column. Constraint (1) becomes a clause of length D2 for each cell, and

(2) and (3) become sets of negative binary clauses. The total number of clauses is B4D2 BG B5.

The binary representation of a Latin square can be viewed as a cube, where the dimensions are the row, column, and color. This view reveals an alternative way of stating the Latin square property: any set of variables determined by holding two of the dimensions fixed must contain exactly one true variable. The "3-dimensional" encoding captures this condition by also including the following constraints:

1. Each color much appear at least once in each row;
2. Each color much appear at least once in each column;
3. No two colors are assigned to the same cell.

As before, the total size of the 3-D encoding is B4D2 BG B5.

As reported in Achlioptas et al. (2000), state of the art backtracking and local search SAT solvers using the 3-D encoding are competitive with specialized CSP algorithms. This is particularly surprising in light of the fact that the best CSP algorithms take explicit advantage of the structure of the problem, while the SAT algorithms are generic. Previous researchers have noted that the performance of backtracking CSP solvers on quasigroup problems is enhanced by using a dual representation (Slaney et al. 1995, Shaw et al. 1998, Zhang and Stickel 2000). This suggests a reason for the success of Davis-Putnam type SAT solvers: In the CSP dual encoding, there are variables for color/row pairs, where the domain is the set of columns, and similarly for color/column pairs, where the domain is the set of rows. The 3-D SAT encoding essentially gives us these dual variables and constraints for free.

This explanation is supported by the extremely poor performance of SAT solvers on the 2-D encodings of the problems. Neither Satz nor Sato can solve any instances at the hardness peak for orders larger than 28; using the 3-D encoding, by contrast, either could solve all instances with one backtrack on average. As shown in Figure 7, the work required by Satz explodes as the problem becomes underconstrained , requiring over 100,000 backtracks for order 28.

An explanation for the difference in performance of Satz on the different encodings can be found by examining the number of unit propagations triggered by each split in the search trees. Table 2 compares the number of unit propagations around the point at which the 2-D encodes become hard for Satz (in bold). Note that at this point each split sets about 5 times more variables for the 3-D encoding than for the 2-D encodings.

Are the 2-D encodings inherently hard? Consider the performance of Walksat, on even larger orders (30 and 33), shown on in Figure 8. Walksat shows an unusual pattern: the 2-D encodings are somewhat easier than the 3-D encodings at the peak, and somewhat harder than then 3-D encodings in the under-constrained region to the right. Thus the 2-D and 3-D are in fact incomparable in terms of any general notion of hardness.

A significant difference between the 3-D and 2-D encodings is that for bothWalksat and Satz it is difficult to see any hardness peak at the threshhold: the problems become hard and then stay at least as hard as they become more and more under-constrained. Note that the most underconstrained instances are inherently easy, since they correspond to a empty completion problem. This reinforces our argument that the 3-D encoding more accurately reflects the underlying computational properties of the quasigroup problem.

In summary, it is important to distinguish properties of a problem instance that make it inherently hard for all methods of attack and properties that make it accidently hard for particular methods. While the encoding style is such an accidental property, the main conjecture we present in this paper is that balance is an inherent property. The evidence for the conjecture is that increasing balance increases solution time for a variety of solvers.

5 Conclusions

Models of random problem generation serve two roles in AI: first, to provide tools for testing search and reasoning algorithms, and second, to further our understanding of what makes particular problems hard or easy to solve, as distinct from the fact that they fall in a class that is worst-case intractable. In this paper we introduced a range of new models of the quasigroup completion problem that serve these roles. We showed how a new notion of balance is an important factor in problem hardness. While previous work on balancing formulas considered the roles of positive and negative literals, our notion of balance is purely structural. Balancing improves the usefulness of the QWH model - one of the best models known for testing incomplete solvers -while retaining its formal simplicity and elegance.