Solving Non-Boolean Satisfiability Problems with Stochastic Local Search

1 Introduction

Much excitement has been generated by the recent success of stochastic local search (SLS) procedures at finding satisfying truth assignments to large formulas of propositional logic. These procedures stochasticly search a space of all assignments for one that satisfies the given formula. Many of the problems on which these methods have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. To tackle a non-Boolean problem with a Boolean procedure, the problem is first reformulated as an equivalent Boolean problem in which multiple Boolean variables are used in place of each non-Boolean variable.

This encode-and-solve approach often results in comparable, if not superior, performance to solving the problem directly. Because Boolean satisfiability is conceptually simple, algorithms for it are often easier to design, implement and evaluate. And because SLS algorithms for Boolean satisfiability have been studied intensively for more than a decade, highly-optimised implementations are publicly available.

This paper proposes and studies a new approach to solving non-Boolean satisfaction problems: that of generalising a Boolean SLS procedure to operate directly on a non-Boolean formula by searching through a space of assignments to nonBoolean variables. In particular, we have generalised Walksat [Selman et al., 1994], a highly-successful SLS procedure for Boolean satisfiability problems, to a new procedure, NBWalksat [Peugniez, 1998; Frisch and Peugniez, 1998], that works on formulas whose variables have domains of any finite size. 1

In this way we are able to apply highly-refined SLS technology directly to non-Boolean problems without having to encode non-Boolean variables as Boolean variables.

The main question addressed by this paper is how the performance of the direct approach compares to that of the transformational (or encode and solve) approach. In particular we compare one direct method, NB-Walksat, and three transformational methods by empirically testing their ability to solve large graph colouring problems and large random nonBoolean formulas. Our three transformation methods consist of applyingWalksat to the results of three transforms.

Boolean variables are merely a special case of non-Boolean variables, and, intuitively, the difference between the nonBoolean and Boolean variables grows as the domain size of the non-Boolean variable increases. Consequently, one would expect that in a comparison of encodings for non-Boolean problems that domain size would be the most important parameter to consider and that one would find that any difference in performance between the encodings would increase when domain size is increased. Ours is the first study to consider this.

Our experimental results show NB-Walksat to be highly effective, demonstrating that the effectiveness of the Walksat strategies can be transferred from the Boolean case to the non-Boolean case. On problems with large domain sizes our direct method is often superior to the transformation methods, which, in some cases, are ineffective.

In the course of studying this new method of solving nonBoolean problems with SLS, we make several other new contributions. Most naturally, we have had to generalise the notion of a Boolean formula to that of a non-Boolean formula. Of the three transformations we use, one is new and one is an enhanced version of a transformation used by others. In order to test the effect of domain size on problem solving performance we want a method for generating random formulas that vary in domain size but are similar in other respects. We propose such a method and use it in our experiments.

1 NB-Walksat and a suite of supporting programs are available at http://www.cs.york.ac.uk/∼frisch/NB.

2 Non-Boolean Formulas

Non-Boolean formulas are constructed from propositional variables, each of which is associated with a finite, non-empty domain. A non-Boolean assignment maps every variable to a member of its domain. Atomic non-Boolean formulas (or nb-atoms) are of the form X/d, where X is a variable and d is a member of its domain. This formula is assigned TRUE by an assignment if the assignment maps X to d; otherwise it is assigned FALSE. Molecular non-Boolean formulas are constructed from atomic non-Boolean formulas and truthfunctional connectives with the usual syntax and Boolean semantics. Observe that though non-Boolean variables can take on values from a domain of arbitrary size, the semantics is still two-valued in that every formula is assigned either TRUE or FALSE. As usual, we say that an assignment satisfies a nonBoolean formula if it maps it to TRUE.

Walksat, and many other Boolean SLS procedures, operate on Boolean formulas in conjunctive normal form (CNF), and NB-Walksat, our generalisation of Walksat, operates on non-Boolean formulas in CNF. A formula, Boolean or nonBoolean, is in CNF if it is a conjunction of disjunctions of literals. A literal is either an atomic formula (called a positive literal) or its negation (called a negative literal). We say that a CNF formula is positive if all its literals are positive and negative if all its literals are negative.

Non-Boolean formulas generalise Boolean formulas since a Boolean formula can be transformed to a non-Boolean formula by replacing every atom P with P ′ /TRUE, where P ′ is a variable whose domain is {TRUE, FALSE}.

We sometimes use terms such as "nb-atom" or "nbformula" to emphasise that these syntactic objects are part of the non-Boolean language. Similar use is made of terms such as "b-atom" and "b-formula".

3 NB-Walksat

Walksat is a highly successful SLS procedure for finding satisfying assignments to Boolean formulas in CNF. We have generalised Walksat to a new system, NB-Walksat, that operates similarly on non-Boolean formulas. Indeed when handling a Boolean formula the two procedures perform the same search. 2 This paper is concerned with version 4 of NBWalksat, which we derived from Walksat version 19. This section describes the operation of NB-Walksat and, since on Boolean formulas NB-Walksat and Walksat perform the same search, this section implicitly describes the operation of Walksat.

The simplest way to understand the operation of NBWalksat is to consider it as working on positive CNF nbformulas. This can be achieved by considering NB-Walksat's first step to be the replacement of every negative literal ¬X/di with X/d1 ∨ · · · ∨ X/di-1 ∨ X/di+1 ∨ · · · ∨ X/dn, where X is a variable with domain {d1, . . . , dn}.

2 We used this property to help test that NB-Walksat was correctly implemented.

NB-Walksat operates by choosing a random assignment and then, until a satisfying assignment is found, repeatedly selecting a literal from an unsatisfied clause and modifying the assignment so as to satisfy that literal. Since the selected literal, X/d, occurs in an unsatisfied clause, the present assignment must map X to a value other than d. The present assignment is modified so that it maps X to d, and its mapping of all other variable is unmodified. We say that the literal X/d has been flipped.

What distinguishes NB-Walksat and Walksat from other procedures is the heuristic employed for selecting which literal to flip. Though Walksat provides a range of such heuristics, the greedy heuristic is generally the most effective [Selman et al., 1994] and many reported experiments have used it. Consequently, it is the greedy version of Walksat that forms the basis for NB-Walksat and only the greedy heuristic is considered in this paper.

NB-Walksat with the greedy heuristic chooses a literal to flip by first randomly selecting a clause with uniform distribution from among all the clauses that are not satisfied by the current assignment. We say that flipping a literal breaks a clause if the clause is satisfied by the assignment before the flip but not after the flip. If the selected clause contains a literal such that flipping it would break no clauses, then the literal to flip is chosen randomly with uniform distribution from among all such literals. If the selected clause contains no such literals, then a literal is chosen either (i) randomly with uniform distribution from the set of all literals in the clause or (ii) randomly with uniform distribution from among the literals in that clause that if flipped would break the fewest clauses. The decision to do (i) or (ii) is made randomly; with a user-specified probability, Pnoise, the "noisy" choice (i) is taken.

4 Transforming Non-Boolean Formulas

To transform nb-satisfaction problems to b-satisfaction problems we map each nb-formula to a b-formula such that the satisfying assignments of the two formulas correspond. This paper presents three such transforms, called the unary/unary, unary/binary and binary transforms. Each operates on an arbitrary formula, though our experiments only apply the transforms to CNF formulas. Each transform operates by replacing each atom in the nb-formula with a b-formula that, in a sense, encodes the nb-atom it replaces. The resulting formula is known as the kernel of the transformation. The transforms employ two ways of producing a kernel; we call these two encodings "unary" and "binary".

If the unary encoding of the kernel is used, the transform also needs to conjoin two additional formulas to the kernel, known as the at-least-one formula (or ALO formula) and the at-most-one formula (or AMO formula). As with the kernel, two encodings can be used for the ALO and AMO formulas: unary and binary. The three transforms we use in this paper are binary (which uses a binary encoding for the kernel and no ALO or AMO formula), unary/unary (which uses unary encodings for the kernel and for the ALO and AMO formulas) and unary/binary (which uses a unary encoding for the kernel and a binary encoding for the ALO and AMO formulas).

The longer version of this paper analyses the sizes of the formulas produced by all the encodings.

The Unary/Unary Transform The unary/unary transform produces a kernel by transforming each nb-atom X/d to a distinct propositional variable, which we shall call X:d. The idea is that a Boolean assignment maps X:d to TRUE if and only if the corresponding non-Boolean assignment maps X to d. Thus, the role of an nb-variable with domain {d1, . . . dn} is played by n b-variables.

Furthermore, one must generally add additional formulas to the Boolean encoding to represent the constraint that a satisfying assignment must satisfy exactly one of X:d1, . . . ,X:dn. This constraint is expressed as a conjunction of an ALO formula (asserting that at least one of the variables is true) and an AMO formula (asserting that at most one of the variables is true). To state that at least one of X:d1, . . . ,X:dn must be satisfied we simply use the clause X:d1 ∨ · · · ∨ X:dn. The entire ALO formula is a conjunction of such clauses, one clause for each nb-variable. To say that at most one of X:d1, . . . ,X:dn must be satisfied we add ¬X:di ∨ ¬X:dj, for all i and j such that 1 ≤ i < j ≤ n. The entire AMO formula is a conjunction of all such clauses produced by all nb-variables.

Notice that these ALO and AMO formulas are in CNF. And since the transform produces a kernel whose form is identical to that of the original formula, the entire b-formula produced by the unary/unary transform is in CNF if and only if the original nb-formula is.

The Binary Transform The unary/unary transform uses D b-variables to encode a single nb-variable of domain size D and, hence, uses a base 1 encoding. By using a base 2 encoding, the binary transformation requires only ⌈log2 D⌉ bvariables to encode the same nb-variable. 3 If X is a variable of domain size D then the binary transform maps an nb-literal of the formX/di by taking the binary representation of i -1 and encoding this in ⌈log2 D⌉ Boolean variables. For example, if X has domain {d1, d2, d3, d4} then

X/d1 is mapped to ¬X2 ∧ ¬X1 , X/d2 is mapped to ¬X2 ∧X1 , X/d3 is mapped to X2 ∧¬X1 and X/d4 is mapped to X2 ∧X1 .

To see what happens when the domain size is not a power of two, reconsider X to have the domain {d1, d2, d3}. If we map X/d1, X/d2 and X/d3 as above then there is a problem in that the Boolean assignment that satisfies X2 ∧ X1 does not correspond to an assignment of a domain value to X. One solution to this problem, which has been employed by Hoos [1998], is to add an ALO formula to ensure that the extraneous binary combination X2 ∧ X1 cannot be satisfied in any solution.

Here we introduce and use a new and better solution to this problem in which no extraneous combinations are produced and therefore no ALO formula is required. In this example the extraneous combination is eliminated if

3 We write ⌈x⌉ to denote the smallest integer that is greater than or equal to x.

X/d1 is mapped to ¬X2, X/d2 is mapped to X2 ∧ ¬X1 and X/d3 is mapped to X2 ∧X1.

Here, the transform of X/d1 covers two binary combinations: (¬X2 ∧ X1) and (¬X2 ∧ ¬X1).

To see what happens in general let X be a variable with domain {d1, . . . , dn} and let k be 2⌈log2 n⌉ - n. Then X/d1, . . . ,X/dk are each mapped to cover two binary combinations and X/dk+1, . . . ,X/dn are each mapped to cover a single binary combination.

Notice that this transform generates no extraneous binary combinations. Also notice that, as a special case, if n is a power of two then each X/di (1 ≤ i ≤ n) is mapped to cover a single binary combination. Finally, to confirm that this binary transform requires no AMO formula and no ALO formula, observe that every Boolean assignment must satisfy the binary transform of exactly one of X/d1, . . . , X/dn.

Notice that the binary transformation of a CNF formula is not necessarily in CNF. However, the binary transformation of a negative CNF formula is almost in CNF; it is a conjunction of disjunctions of negated conjunctions of literals. By using DeMorgan's law, the negations can be moved inside of the innermost conjunctions, resulting in a CNF formula of the same size. At the other extreme, the binary transformation of a positive CNF formula is a conjunction of disjunctions of conjunctions of literals. One way of transforming this to CNF is to distribute the disjunctions over the conjunctions. Unfortunately applying this distribution process to the binary transform of a positive nb-clause produces a CNF formula that can be exponentially larger than the original clause.

The Unary/Binary Transform The unary/binary transform produces the same kernel as the unary/unary transform. The ALO and AMO formulas it produces achieve their effect by introducing the binary encodings of nb-atoms and linking each to the unary encoding of the same nb-atom. Since the binary encoding requires no ALO or AMO formulas, the unary/binary encoding requires no ALO or AMO formulas beyond these linking formulas.

The links provided by the AMO formula state that for each nb-atom, X/di, its unary encoding, X:di, implies its binary encoding. For example, if the nb-variable X has domain {d1, d2, d3, d4} then the AMO linking formula for X is

The entire AMO formula is a conjunction of such linking formulas, one for each nb-variable.

The links provided by the ALO formula state that for each nb-atom, X/di, its unary encoding X:di is implied by its binary encoding. For example, if the nb-variable X has domain {d1, d2, d3, d4} then the ALO-linking formula for X is

The entire ALO formula is a conjunction of linking formulas, one linking formula for each nb-variable. Observe that both the AMO and ALO linking formulas can be put easily into CNF with at most linear expansion.

5 Experimental Results

This section presents experiments on graph colouring problems and random nb-formulas that compare the performance of the four methods, which we shall refer to as NB (nonBoolean encoding), BB (binary encoding) UU (unary/unary encoding) and UB (unary/binary encoding). In all experiments, Walksat version 35 was used to solve the Boolean encodings and NB-Walksat version 4 was used to solve the non-Boolean encodings, even in cases where the domain size is 2. Both programs provide the user the option of either compiling the program with fixed size data structures or allocating the data structures when the formula is input at runtime; the latter option was used in all experiments. All experiments were run on a 600 MHz Pentium III with 126 megabytes of memory.

Considerable care must be taken in setting the Pnoise parameter for the experiments. Much work in this area has been reported without giving the value used for Pnoise, and thus is irreproducible. Setting the parameter to any fixed value over all formulas is not acceptable; we have observed that a parameter setting that is optimal for one formula can be suboptimal by several orders of magnitude for another formula. The best option is to report performance at the optimal setting for Pnoise, which-in the absence of any known method to determine this a priori-we have determined experimentally. This is also the route followed by Hoos [1998] in his extremely careful work.

In using SLS procedures it is often considered advantageous to restart the search at a new, randomly-selected assignment if the procedure has not found a solution after a prescribed number of flips. This issue is not relevant for the current study. Since the optimal restart point and the amount gained by restarting are functions of the procedure's performance without restarts, this study need only be concerned with the performance without restarts.

Graph Colouring Our experiments used 6 instances of the graph colouring problem that are publicly available at the Rutgers Univ. DIMACS FTP site. 4

Each problem instance was encoded as a CNF nb-formula. For each node in the graph the formula uses a distinct variable whose domain is the set of colours. The formula itself is a conjunction of all clauses of the form ¬X/c ∨ ¬Y/c, such that X and Y are nodes connected by an arc and c is a colour.

Three Boolean CNF representations of each problem instance were produced by applying the three transforms of Section 4 to the non-Boolean representation. The longer version of this paper proves that a negative CNF nb-formula can be transformed to a b-formula without the AMO formulas. So the two unary encodings used here contain only kernels and ALO clauses. Also because the nb-clauses representing instances of the graph colouring problem are negative, the binary transform maps each nb-clause to a single b-clause (as discussed in Section 4).

4 ftp://dimacs.rutgers.edu/pub/challenge/graph/benchmarks/color/

Figure 1 shows the results obtained for solving each problem instance 101 times with each of the four methods. The formula size column shows the size (in terms of atom occurrences) of the formula input to Walksat or NB-Walksat. All experiments were run with Pnoise set to its optimal value, which is recored in the Pnoise column. The flip rate column gives the mean flip rate over all 101 runs. The median flips and median time column gives the sample median of the number of flips and amount of cpu time taken to solve the problem.

Examination of these results reveals that over the range of problems NB and UU have roughly comparable (within a factor of 2 to 3) solution times. 5 With increasing domain size (number of colours) the NB fliprate drops sharply but the advantage that NB has in terms of number of flips increases. These two opposing factors cancel each other, resulting in the roughly comparable solution times.

On the two problems with small domain size (5 colours) BB and UB produce solution times that are competitive with the other methods. However, on three problems with larger domain size-le450 15a with 15 colours and DSJC125.5.col with 17 and 18 colours-BB and UB do not compete well with the other methods. On le450 25a, a very easy problem with a domain size of 25, BB has competitive performance but UB is totally ineffective. We conjecture that UB cannot solve this very easy problem because the method is highly sensitive to domain size.

RandomNon-Boolean CNF Formulas Since we can control certain parameters in the generation of random CNF nbformulas, they provide a good testbed. In particular, since this paper is a study of solving problems with domain sizes greater than two, we would like to know how problem solving performance varies with domain size. To measure this we need to select problem instances that have different domain sizes but are otherwise similar. Formulating a notion of "otherwise similar" has been one of the most challenging problems faced by this research.

We have developed a program that generates random, positive CNF nb-formulas using five parameters: N, D, C, V and L. Each generated formula consists of exactly C clauses. Using a fixed set of N variables each with a domain size of D, each clause is generated by randomly choosing V distinct variables and then, for each variable, randomly choosing L distinct values from its domain. Each of the chosen variables is coupled with each of its L chosen values to form L · V positive literals, which are disjoined together to form a clause.

The simplest conjecture on how to study varying domain size is to fix the values of N, C, V , and L and then to systematically vary D. One can easily see that performance on this task would just exhibit typical phase-transition behaviour [Mitchell et al., 1992]: small values of D would produce underconstrained problems, which would become criticallyconstrained and then over-constrained as D increases. The problem instances generated by this method would not be similar in terms of their location relative the phase transition.

5 We caution the reader against taking solution time too seriously as we have found that the ratio of solution times between computers varies greatly from formula to formula.

Our solution to this shortcoming is to vary D and to adjust the other four parameters so as to put the problem class at the phase transition-that is, at the point where half the instances in the class are satisfiable. But for any given value of D many combinations of values for N, C, V and L put the problem class at the phase transition. We determine the values of these parameters by keeping DV , the size of the search space, at a fixed value for all problem instances and then requiring all clauses to have the same "constrainedness", as measured by (L/D)V . Mimicking Boolean 3CNF, we set V to three and aim to keep (L/D)V at 1/8, which is achieved by setting L to .5D. This follows the constant length model advocated by Mitchell, Selman and Levesque [1992]. Finally C is set to whatever value puts the problem class at the phase transition, which we determined experimentally. Thus, while varying D, the parameters that we are holding constant are search space size, the number of variables constrained by each clause and the amount of constraint placed on each, and the proportion of instances with that parameter setting that are solvable.

Our experiments were conducted on domain sizes of 2, 4, 8, 16 and 32. Following the model above we kept DV at a constant value, 260 . Then for each domain size, we experimentally located the point of the phase transition. The leftmost column of Figure 2 shows the value of C (number of clauses) at which these experiments located the phase transitions.

With the parameters of the random formulas determined, at each domain size we generated a series of random formulas according to the above method and, using a non-Boolean version of the Davis-Putnam procedure, kept the first 25 satisfiable ones. 6 At each domain size 101 attempts were made to solve the suite of 25 formulas with the NB, UU and UB methods. The longer version of this paper proves that a positive CNF nb-formula can be transformed to a b-formula without the ALO formulas. Since our randomly-generated formulas are positive, the two unary encodings that are used here contain only kernels and AMO formulas.

6 A Boolean Davis-Putnam procedure is incapable of solving Boolean encodings of the instances with larger domain sizes!

The BB method was not attempted since the binary transformation of these random nb-formulas is unreasonably long. As discussed at the end of Section 4, if the binary transform is used to produce a CNF b-formula from a positive CNF nbformula, the size of the resulting b-formula is exponential in the clause length of the original nb-formula-which in this case is 3 2 D.

The results of these experiments, shown in Figure 2, consistently follow a clear pattern. In terms of both time and number of flips, all methods show a decline in performance as domain size grows. However, the decline of UU and UB is so sharp that UB is ineffective on domain size 16 and UU is two orders of magnitude slower than NB on domain size 32. On these random formulas, as on the graph colouring problems, the fliprates of all methods decrease as the domain size increases. However, on the random problems, unlike the colouring problems, NB's fliprate suffers the least from increasing domain size. Indeed, by the time domain size reaches 8, NB has a higher fliprate than UU, and this advantage grows as domain size increases. The sharp decline in the UU fliprate results from the rapid increase in the size of the UU formulas, which occurs because the size of their AMO component grows quadratically with domain size.

6 Discussion and Conclusions

The literature reports a number of cases where the transformation approach has been used to attack a non-Boolean problem with Boolean SLS. Such problems include the n-queens problem [Selman et al., 1992], graph colouring [Selman et al., 1992; Hoos, 1998, Chp. 4], the all-interval-series problem [Hoos, 1998, Chp. 4], the Hamiltonian circuit problem

Figure 1: Results, given to three significant figures, for 101 sample runs on each graph colouring problem. On those rows missing entries, 11 attempts, each of 10,000,000 flips, were made at each of four Pnoise settings (.083, .167, .25 and .33); no solutions were found.

[Hoos, 1999; 1998, Chp. 7], random instances of the (finite, discrete) constraint satisfaction problem [Hoos, 1999; 1998, Chp. 7], and STRIPS-style planning [Kautz and Selman, 1992; Kautz et al., 1996; Kautz and Selman, 1996; Ernst et al., 1997; Hoos, 1998, Chp. 4]. Yet, in spite of this widespread use of the transformation approach, only two previous studies have compared the performance of SLS on different encodings of non-Boolean variables: Ernst, Millstein and Weld [1997] compare unary/unary and binary encodings of STRIPS-style planing problems and Hoos [1999; 1998, Chapter 7] compares the unary/unary and binary encodings of random constraint satisfaction problems and of Hamiltonian circuit problems. Other than these two comparative studies, we know of no work that uses Boolean encodings other than unary/unary.

Although Hoos' experiments use a clever methodology designed to provide insight into the structure of SLS search spaces, his study examines only problem instances whose non-Boolean formulation involves variables with domain size 10. And though the work of Ernst, Millstein and Weld is also enlightening in many respects, one cannot determine the domain sizes of the non-Boolean variables in their encodings since they do not report the identity of their suite of planning instances. In contrast to all previous studies, ours considers the effect of varying domain size and hence is able to confirm the expectation that domain size is generally a critical parameter. In particular, our study suggests that Hoos' conclusion-which also appears to be the dominant view in the community- that UU is a viable alternative to NB is generally true only for problems with smaller domain sizes. On problems that require AMO formulas and have large domain sizes our study shows that NB tends to be the best choice and is sometimes the only feasible choice.

In almost all work, when non-Boolean problems are encoded as Boolean formulas the encoding is done in a single stage, directly mapping the problem to a Boolean formula. In some cases this is done manually and in others it is done automatically. In contrast, we advocate a two-stage approach in which the problem is first mapped (manually or automatically) to a non-Boolean formula which is then systematically (and, in our case, automatically) transformed to a Boolean formula. We conjecture that all Boolean encodings that have so far been produced by the single stage approach could be produced by the two stage approach.

It has recently come to our attention that work by B´ejar and Many`a [1999] in the area of multi-valued logic has independently led to the development of another generalisation of Walksat, called Regular-WSAT, that appears to be almost identical to NB-Walksat. Regular-WSAT operates on a special class of signed clauses called regular signed clauses. A signed clause is a syntactic variant of an NB-clause except that every variable must be associated with the same domain. To define regular signed clauses, the domain values first must be totally ordered. (In certain other settings, the order is only required to be a lattice.) A signed clause is said to be regular if, in effect, it is positive and for each literal X/d it contains it also contains either every literal X/d′ such that d′ < d or every literal X/d′ such that d < d′ .

Though Regular-WSAT is presented as a procedure for regular signed clauses, it appears that it would work on any signed clause and thus is akin to NB-Walksat. Nor does there appear to be anything inherent in the presentation of RegularWSAT that prevents it from handling variables with different domain sizes. However, when operating on a clause containing variables with differing domain sizes it appears that Regular-WSAT and NB-Walksat use different distributions in choosing which literal to flip. Regular-WSAT first chooses a variable from among those in the clause and then chooses one of the values that appear with that variable, whereas NBWalksat simply chooses from among all the literals in the clause.

Though regular signed clauses are a special class of NBclauses, they can be used effectively to encode a range of problems including graph colouring problems and roundrobin scheduling problems [B´ejar and Many`a, 1999]. The extra restrictions placed on regular signed clauses can be exploited to translate them to Boolean clauses more compactly than can NB-clauses [B´ejar et al., 2001]. However, we are not aware of any attempt to exploit these translations to solve problems encoded as regular signed clauses.

It would be worthwhile to extend the comparisons made in this paper to include additional solution methods employing SLS. As just suggested, the comparisons could include Boolean translations of regular signed clauses. It would be especially worthwhile to consider SLS methods, such as minconflicts [Minton et al., 1992], that operate directly on the original problem or on a constraint satisfaction encoding of the problem. 7

Of the many questions remaining to be addressed by future work the biggest challenge facing the study of problem encodings-including all encoding issues, not just the handling of non-Boolean variables-is the quest for generality. What can we say about about encoding issues that can guide us in producing effective encodings of new problems? This challenge must be decomposed if progress is to be made. This paper's biggest contribution towards this end is separating out the issue of non-Boolean variables and identifying domain size as a critical parameter.

Finally we claim that, in addition to developing new problem encodings, the applicability of SLS technology can be extended by enriching the language on which the SLS operates. This claim is supported by recent results on pseudoBoolean constraints [Walser, 1997] and non-CNF formulas [Sebastiani, 1994]. Our success with NB-Walksat adds further weight to the claim.

Acknowledgements

We are grateful to Henry Kautz and Bram Cohen for providing their Walksat code, from which the NB-Walksat implementation was developed. We also thank Peter Stock, who used his non-Boolean Davis-Putnam program to filter out the unsatisfiable instances from our suite of randomly-generated nb-formulas. Thanks to Toby Walsh for many illuminating discussions and to Steve Minton, Bart Selman and the anonymous referees for useful suggestions.