Building Structure into Local Search for SAT

1 Introduction

A fundamental challenge facing local search researchers in the satisfiability (SAT) domain is the increasing scope and performance of complete search methods. While for most of the 1990s it was taken for granted that local search was the most practical method for solving large and complex real world satisfiability problems [Selman et al., 1992; Kautz and Selman, 1996; B´ejar and Many`a, 2000], the latest generation of complete SAT solvers have turned the tables, solving many structured problems that are beyond the reach of local search (e.g. [Zhang et al., 2001; E´en and Biere, 2005]). 1 So it is of basic importance to the area that local search techniques learn from the success of the newer complete methods.

1 More information on the performance of complete search versus local search is available from the SAT competitions (http://www.satcompetition.org)

The current research goes to the core of this problem by modelling problem structure within a local search procedure. This involves a two-part process: firstly problem structure must be recognized within the original problem representation (here we are considering satisfiability problems expressed in conjunctive normal form (CNF)). And secondly this structure must be represented within a local search procedure in such a way that the local neighbourhood of possible moves will only contain structure respecting flips.

The ideas behind this approach come from two sources. Firstly, there is the recent work on modelling constraint satisfaction problems (CSPs) as SAT problems [Pham et al., 2005]. Here the presence of CSP multivalued variables is automatically detected in the clausal structure of a CNF problem. This information is then embedded within a local search in such a way that for each group of binary valued SAT variables corresponding to a single multivalued CSP variable, only one SAT variable will be true at any one time. This enforces that the underlying CSP variable is always instantiated with a single domain value. The SAT-based local search achieves this by doing a two-flip look-ahead whenever it encounters a literal associated with a CSP domain value. In effect this look-ahead turns off the current CSP domain value with one flip and turns on a new value with a second flip. A significant advantage of this approach (when encoding binary CSPs) is that the cost of such a double-flip equals the sum of the costs of the individual flips, because these flip pairs will never appear in the same conflict clause. For this reason, CSP structure exploiting algorithms can be easily embedded within an existing SAT local search architecture and add negligible processing overhead to an individual flip. As we shall see, more general structure exploiting approaches do cause interactions between literals within the same clauses, and so require more sophisticated flip cost calculation procedures.

The second source for the current research comes fromOstrowski et al.'s [2002] work on the extraction of gates from CNF encoded SAT problems. These gates represent relationships between SAT variables of the form y = f(x1, . . . , xn) where f ∈ {⇔, ∧, ∨} and y and xi are Boolean variables from the original problem. If such a gate is recognized, the value of y is determined by x1, . . . , xn, and can be removed. Ostrowski et al. used this method to simplify a range of structured SAT benchmark problems, producing significant performance gains for their systematic DPLL solver. However, to the best of our knowledge, such structure exploiting approaches have not been applied in the local search domain.

The problem facing a local search approach to implementing gates is one of efficiency. Ostrowski et al.'s approach can detect independent variables whose values determine a set of dependent variables via clausal gate connections. Using this information, we can implement a local search that only flips the values of independent variables and then dynamically calculates the effects of these flips on the overall solution cost. However, a local search needs to know the flip cost of all candidate flips in advance of making a move. Generally this is achieved by maintaining a make cost and a break cost for each literal in the problem (i.e. the number of clauses that will become true if a literal is flipped and the number of clauses that will become false). These costs are then updated after each flip. A major advantage of a SAT local search is the speed with which these cost effects can be calculated (this is achieved using clever data structures that exploit the SAT CNF problem structure) [Tompkins and Hoos, 2004]. However, taking an approach that only flips independent variables renders the standard SAT local search architecture redundant. In this case, finding the potential cost of an independent variable flip requires us to solve a mini-SAT problem involving all the affected dependent variables and their associated clauses.

The rest of the paper is organized as follows: we first explain how the cost of flipping an independent variable in a local search can be efficiently calculated using a dependency lattice data structure. This structure models the various dependencies in the original problem and dynamically calculates which independent variables, when flipped, will cause a clause to change its truth value. Details of the construction and operation of this lattice are given in the next two sections. To evaluate the usefulness of this new approach, we conduct an empirical study that examines several of the structured SAT benchmarks that have proved to be the most difficult for local search in the past. Finally, we discuss the significance of our results and indicate some future directions of research.

2 Gates and Dependencies

In the following discussion we shall broadly follow the terminology used in [Ostrowski et al., 2002]. Firstly, consider the following CNF formula:

Here, for the clauses to be satisfied, if b and c and d are all false then a must necessarily be false, otherwise a must necessarily be true. This is an example of an "or" gate, because the value of a is determined by truth value of (b ∨ c ∨ d) and can be represented as

Similarly, if we reverse the signs of the literals we get:

Now for the formula to be satisfied, if b and c and d are all true then a must necessarily be true, otherwise a must necessarily be false. This example of an "and" gate can be represented as

A third commonly occurring clausal structure is the "equivalence" gate (or "xnor" gate), illustrated as follows:

Here, in order to satisfy the formula, a will be true iff b and c are both true or both false, i.e. if they are equivalent, otherwise if b and c differ then a will be false. This can be represented as

Finally, an "xor" gate is the negation of an "equivalence" gate, illustrated as follows:

where a will only be false if b and c are equivalent. This can be represented as

If an "equivalence" or an "xor" gate depends on more than two variables, then equivalence or difference is calculated in a pairwise fashion, i.e. if a =⇔ (b, c, d) and b and c are false, then b ⇔ c is true, and if d is true, then d ⇔ (b ⇔ c) is true and therefore the gate is true. In general, we represent an "xor" gate as y = ⊕(x1, . . . , xn), an "equivalence" gate as y =⇔ (x1, . . . , xn), an "or" gate as y = ∨(x1, . . . , xn) and an "and" gate as y = ∧(x1, . . . , xn). Here y is the dependent variable because its value is determined by the independent variables x1, . . . , xn. For the sake of simplicity, we treat an "xor" gate (e.g. a = ⊕(b, c)) as a special case of an "equivalence" gate (e.g. ¬a =⇔ (b, c)) in the rest of the paper.

3 The Dependency Lattice

As Ostrowski et al. [2002] have already described, the process of recognizing gates in a CNF problem can be reduced to searching for the appropriate clausal structures during a preprocessing phase. This information can then be used to classify the dependent and independent variables. For a complete search method, this means the search space can immediately be reduced to only consider independent variable instantiations, as all dependent variable values can be automatically fixed by propagation.

However, for a local search, there is no built-in propagation mechanism. In fact, a local search strategy precludes propagation because it deliberately allows inconsistent assignments to persist. To exploit the information inherent in dependent variable relationships requires us to remove them from the domain of "free" variables while still including their effect in the overall cost of a particular flip. To achieve this we have developed a dependency lattice data structure. This lattice is formed as a result of analyzing the original CNF problem into independent variables, and relationships between internal and external gates. Firstly, an independent variable is not simply a variable that determines the value of a dependent variable in a gate relationship, because such determining variables can in turn be determined in another gate. An independent variable is a variable that is never determined in any gate relationship. Secondly, an internal gate is any gate that can be recognized within the structure of the original CNF formula, and thirdly, an external gate is a gate where the dependent variable represents a clause from the original CNF formula that is not part of any internal gate. To clarify these concepts, consider the following CNF formula example:

which is equivalent to:

where c1 is an additional variable that depends on the clause (v1 ∨ g1) (i.e. if (v1 ∨ g1) is true, c1 is true, otherwise c1 is false). In general, each original CNF clause that is not subsumed within a gate dependency is represented by an additional variable, that then subsumes the clause in an external "or" gate dependency.

Having translated our original problem into a set of gates, we can now represent it as the dependency lattice in Figure 1:

Here the original variables have become nodes in the lattice, such that nodes v1 . . . v4 correspond to the independent variables, nodes g1 . . . g3 to the internal gates and node c1 to an external gate. In this form, a satisfying assignment to the original CNF formula is equivalent to an assignment of the independent variables such that all the ci external nodes evaluate to true. This result follows trivially from the structure of the lattice, which implements the structure of the internal gates and therefore ensures that all internal gate relationships are necessarily satisfied. When all the external nodes evaluate to true, this means all the remaining CNF clauses that were not subsumed as internal gates are true, and hence that a satisfying assignment has been found.

The purpose of the lattice is to embody the structure of gate dependencies in such a way that the cost of flipping an independent variable can be efficiently calculated. This is analogous to existing local search SAT solvers, except that existing solvers are only equipped to handle "or" gate dependencies.

3.1 Calculating Flip Costs

To illustrate the process of cost calculation, we have instantiated the independent variables in Figure 1 as follows: v1 ← false, v2 ← false, v3 ← true and v4 ← false. Moving down the lattice from v2 and v3 to the "and" gate at node g1 it follows that the values of v2 and v3 make this gate variable false. Similarly, moving down from v3 and v4 to g2 we can see that the corresponding "or" gate variable is true. Then following down from the gates at g1 and g2 to the "equivalence" gate at g3 we can see that this gate variable is false, and so on. In this way, the lattice reflects the necessary consequences of the independent variable instantiations on the rest of the problem.

To calculate the cost of flipping a particular independent variable vi we need to know how many external gate variables will become false and how many will become true as a result of the flip. This is achieved by storing at each gate node the set of independent variables that, if flipped, would cause the gate variable to change its truth value. For example, node g1 stores the independent variable v2, signifying that if v2 was flipped then g1 would change from false to true. Similarly, g2 can only become false if v3 is flipped. Moving down the lattice, we can see that g3 would become true if either g1 or g2 were to change values. As flipping v2 will change the truth value of g1 and flipping v3 will change the truth value of g2, either of these flips will also change the truth value of g3, so g3 inherits v2 and v3 into its variable set. Node c1 similarly inherits v1 and v2, as a change in either variable will make c1 true.

Once we have the correct variable sets for each of the external gates we can read off the make cost and break cost for each independent variable simply by counting the number of times a variable appears in a false external gate (= make cost) and the number of times it appears in a true external gate (= break cost). So, in our example, both v1 and v2 have a make cost of one, with all other make and break costs equal to zero.

3.2 The General Case

In realistic problems it can easily happen that the same independent variable appears in multiple branches leading to the same gate. To handle such cases we require more general definitions of how the variable sets for each gate type are composed.

Firstly, if an "and" gate is true then all its parent nodes must be true, therefore any change in a parent node's truth value will also change the truth value of the gate. This means the gate's variable set (V ) should inherit the union of all the parent variable sets (Psets), as follows:

Alternatively, if an "and" gate is false then only if all its parent nodes become true will the gate become true. This requires that all false parent nodes become true and no true parent node becomes false, as follows:

The rules for an "or" gate can be similarly defined in reverse:

For all "equivalence" gates with no more than two parents, only if the truth value of a single parent changes will the value of the gate change, as follows:

In general, an "equivalence" gate is true iff the count of its true parents has the same parity as the count of all its parents. As we did not discover any "equivalence" gates with more than two parents in our problem set, we did not implement the more-than-two-parent case.

In addition, we did find rare problem instances where a single variable was dependent on more than one gate. In these circumstances, we added an additional dependent variable for each extra gate and connected these variables to the first variable via additional "equivalence" gates.

3.3 Implementation

The motivation behind the dependency lattice is to develop an efficient method to update the make and break costs for the independent variables. Clearly there is a potential for the additional work of calculating flip costs using the lattice to outweigh the benefits of reducing the size of the search space (i.e. by eliminating dependent variables and internal gate clauses from the problem). Therefore it is of significance exactly how the lattice is updated. In our current implementation we do this by representing the total set of independent variables at each node using an nind bit pattern, such that if the ith independent variable is in the variable set of a particular node, then the ith position of the bit pattern for that node will be set. Using this representation we can efficiently implement the set operations necessary to propagate the effects of flipping an independent variable through the lattice. This propagation starts when an independent variable has been selected for flipping. Beginning at the lattice node corresponding to this variable, the update works down the lattice to all the connected internal nodes. For example, if v3 is flipped in Figure 1, then nodes g1 and g2 will be selected for update. The update process then performs the appropriate set operations on the parent variable sets to produce an updated variable set and truth value for the selected gate. If the truth value of a node and the contents of its variable set remain unchanged after an update then no further propagation is required from that node. Otherwise the process continues until it reaches the external nodes. Then, if an external node's variable set is changed, this updates the make and break costs of any affected independent variables and the process terminated.

If we follow the process of flipping v2 in Figure 1, this will alter the variable set at g1 from {v2} to {v2, v3} and change g1 to true. As the variable set at g1 has changed these effects are now propagated to the internal node g3 which becomes true. Now we have a situation where both parents of g3 share the same variable, i.e. g1 now has {v2, v3} and g2 has {v3}. In this case if v3 were flipped then both parents of g3 would change their truth value and still remain equivalent, leaving g3 unchanged. Hence g3 only inherits v2 into its variable set. Finally, the external node c1 changes its truth value to true and changes its variable set from {v1, v2} to {v2, v3}. This change then causes the make costs of v1 and v2 to be reduced by one and the break costs of v2 and v3 to be increased by one. The process terminates with all external nodes set to true, meaning that a satisfying solution has been found. This situation is illustrated in Figure 2:

4 Experimental Validation

In order to validate our approach to handling gate dependencies, we implemented a non-CNF version of AdaptNovelty+ [Hoos, 2002] that operates on the new dependency lattice platform. We then evaluated the performance of this algorithm on a selection of SATLIB ssa7552, parity 16- and 32-bit problems. 2 Table 1 firstly shows the effect of gate detection on the number of variables and clauses in the problem set, detailing the number of independent and dependent gates in the corresponding non-CNF dependency lattices and the total time taken for each conversion.

We then compared the performance of our new non-CNF AdaptNovelty+ algorithm against the original CNF based variant by running the two algorithms 100 times each on the ssa7552 and par16 instances and 10 times each on the par32 instances. Table 2 shows the success rate, the average number of flips and time in seconds taken to solve these instances. Each run was timed out after 1 hour for the ssa7552 and par16 instances and after 24 hours for the par32 instances.

As shown in Table 2, the non-CNF version of AdaptNovelty+ significantly outperforms its original CNF counterpart both in terms of flips and time. Indeed, the new non-CNF approach is at least 100 times better than the original CNF approach on these instances. In addition, this is the first time that a local search solver has managed to find solutions for all the parity 32-bit problems within 24 hours. The only other SLS method that can solve these problems is DLM2005 [Wah and Wu, 2005]. However, DLM could only solve the compacted par32-*-c instances, producing only 1 successful run out of 20 attempts and taking nearly 33 hours to find a solution.

As all else has been left unchanged between the two versions of AdaptNovelty+, we must conclude that the extraordinary performance gains are due to the successful recognition and exploitation of variable dependencies in the new nonCNF approach. As shown in Figure 3, the dependency lattice of the par8-1 instance is highly connected. Access to this extra knowledge enables the new solver to maintain the consistency of the dependent variables and hence to efficiently navigate the search space and find a solution. The structure of the variable dependencies is otherwise flattened out and hidden in the original CNF representation. This means that CNF based SLS solvers must expend considerable extra effort to discover solutions that respect these dependencies.

2 Available from http://www.satlib.org

However, the cost of maintaining consistency between the newly discovered gates in our non-CNF approach is also significant. To measure this, we conducted an additional experiment using a set of bart FPGA problems that exhibit no dependency structure [Aloul et al., 2002]. Table 3 shows our non-CNF AdaptNovelty+ solver to be more than 1, 000 times slower on these problems. However, this performance deficit can be partly explained by the initial cost of searching for gate dependencies in the original CNF representation, and hence will become less significant for problems where the solution time significantly exceeds the preprocessing time. We also used the built-in C++ set class to update the lattice which could be replaced by more efficient, special purpose data structures and operators. Finally, it would be trivial to implement a switch that automatically reverts to using a CNF based solver when the proportion of gate dependencies falls below a given threshold.

5 Conclusion

In conclusion, we have introduced a new dependency lattice platform that effectively maintains the consistency between independent and dependent variables (or gates) during the execution of a local search. Based on this platform, our new non-CNF version of AdaptNovelty+ can solve many hard structured benchmark problems significantly faster than its original CNF based counterpart. In addition, this non-CNF AdaptNovelty+ variant is the first local search solver able to reliably solve all five par32 instances within 24 hours. By exploiting variable dependencies within a local search and by solving the par32 problems we have also successfully addressed two of the "Ten Challenges in Propositional Reasoning and Search" (#2 and #6) presented in [Selman et al., 1997].

In future work, we expect that non-CNF implementations of the latest clause weighting local search solvers (such as PAWS [Thornton et al., 2004] and SAPS [Hutter et al., 2002]) will further extend the state-of-the-art in local search techniques. In fact, the extension of these solvers using our dependency lattice is very straightforward. Instead of counting the number of external dependent gates that will be made or broken if an independent gate is flipped, we simply sum the corresponding weights of the dependent gates.

Another future research direction is to develop new heuristics that further exploit the gate dependencies when selecting the next variable to flip. With these improvements, we expect that local search techniques will be able to match the performance of the state-of-the-art DPLL solvers on the more structured industrial benchmark problems.

Acknowledgments The authors would like to acknowledge the financial support of National ICT Australia (NICTA) and the Queensland government. NICTA is funded through the Australian Government's Backing Australia's Ability initiative and also through the Australian Research Council.