Heuristics Based on Unit Propagation for Satisfiability Problems

1 Introduction

Consider a propositional formula F in Conjunctive Normal Form (CNF) on a set of Boolean variables { x1, x2, ... , xn}, the satisfiability (SAT) problem consists in testing whether clauses in F can all be satisfied by some consistent assignment of truth values (1 or 0) to the variables. If it is the case, F is said satisfiable; oth­ erwise, F is said unsatisfiable. If each clause exactly contains r literals, the subproblem is called r-SAT prob­ lem.

SAT problem is fundamental in many fields of com­ puter science, electrical engineering and mathematics . It is the first NP-Complete problem [Cook, 1971) with 3-SAT as the smallest NP-Complete subproblem.

The Davis-Putnam-Loveland procedure (DPL) [Davis et al., 1962) is a well known complete method to solve SAT problems, roughly sketched in Figure 1.

DPL procedure essentially constructs a binary search tree, each recursive call constituting a node of the tree. Recall that all leaves (except eventually one for a sat­ isfiable problem) of a search tree represent a dead end where an empty clause is found . The branching vari­ ables are generally selected to allow to reach as early as possible a dead end, i.e. to minimize the length of the current path in the search tree.

The most popular SAT heuristic actually is Mom's heuristic, which involves branching next on the variable having Maximum Occurrences in clauses of Minimum Size [Dubois et al., 1993; Freeman, 1995; Pretolani, 1993; Crawford and Auton, 1996; Jeroslow and Wang, 1990). Intuitively these variables allow to well exploit the power of unit propagation and to augment the chance to reach an empty clause. Recently another heuristic based on Unit Propagation (UP heuristic) has proven useful and allows to exploit yet more the power of unit prop­ agation [Freeman, 1995; Crawford and Auton, 1996; Li, 1996). Given a variable x, a UP heuristic examines x by respectively adding the unit clause x and x to F and independently makes two unit propagations. The real effect of the unit propagations is then ti_Sed to weigh x.

procedure DPL(F) Begin

if F is empty, return "satisfiable";

F:=UnitPropagation(F); If F contains an empty clause, return "unsatisfiable".

I· branching rule ·I

select a variable x in F according to a heuristic H, if the calling of DPL(FU{x}) returns

"satisfiable" then return "satisfiable", otherwise return the result of calling DPL(FU {x}).

End.

procedure UnitPropagation(F)

Begin

While there is no empty clause and a unit clause l exists in F, assign a truth value to the variable contained in l to satisfy l and simplify F. Return F.

End.

Figure 1: DPL Procedure

However, since examining a variable by two unit prop­ agations is time consuming, two major problems remain open: should one examine all free variables by unit prop­ agation at every node of a search tree? if not, what are the variables to be examined at a search tree node?

In this paper we try to experimentally solve these two problems to obtain an optimal exploitation of UP heuris­ tic. We define a PROP predicate at a search tree node whose denotational semantics is the set of variables to be examined at a search tree node, i.e. x is to be examined if and only if P ROP(x) is true. By appropriately chang­ ing PROP, we experimentally analyse the behaviour of different UP heuristics. We write 12 DPL procedures which are different only in PROP and run these pro­ cedures on a very large sample of hard random 3-SAT problems.

We begin in section 2 by describing the 12 DPL proce­ dures and summarizing the experimental results on these programs. In section 3 we compare a pure UP heuris­ tic and a pure Mom's heuristic and show the superiority of UP heuristics. In section 4 we study different restric­ tions of UP heuristics. In section 5 we discuss the related work and compare the best DPL procedure in our exper­ imentation with three state-of-the-art DPL procedures. Section 6 concludes the paper.

2 UP Heuristics Driven by PROP

Let dif f(F1 , F2) be a function which gives the number of clauses of minimum size in F1 but not in F2, we show a generic branching rule in Figure 2, where the equation defining H(x) is suggested in [Freeman, 1995] and the weight 5 for uniformizing clauses of different length is empirically optimal.

For each free variable x such that PROP(x) is true do let F' and F" be two copies of F Begin F' : = Uni tPropagat ion (F' U { x}) ; F" := UnitPropagation(F" U {x}); return 11 F is unsat isf iable 11 · If F' contains an empty clause then x := 0, F := F" else if F" contains an empty clause then x := 1, F := F'; If neither F' nor F" contains an empty clause then let w(x) denote the weight of x w(x) :=diff(F',F) and w(x) :=diff(F",F)

If both F' and F" contain an empty clause then End; If all variables examined above are valued or PROP(x) is false for every x then For each free variable X in F do let r; be the length of the clause C; w(x) := I:%EC;5-r; and w(x) := I:xec;s-r; For each variable x do H(x) := w(x) * w(x) * 1024 + w(x) + w(x)

Branching on the free variable x such that H(x) is the greatest.

Figure 2: A Generic Branching Rule Driven by PROP

The essential reason to use UP heuristics instead of Mom's one is that Mom's heuristic may not maximize the effectiveness of unit propagation, because it only takes binary clauses (if any) into account to weigh a variable, although some extensions try to also take longer clauses into account with exponentially smaller weights (e.g. 5 ternary clauses are counted as 1 binary clauses). A UP heuristic allows to take all clauses containing a variable and their relations into account in a very effective way to weigh the variable. As a secondary effect, it allows to detect the so-called failed literals in F which when satisfied falsify F in a single unit propagation. However since examining a variable by two unit propagations is time consuming, it is natural to try to restrict the vari­ ables to be examined. For this purpose we use PROP predicate defined at a search tree node.

The success of Mom's heuristic suggests that the larger the number of binary occurrences of a variable is, the higher its probability of being a good branching vari­ able is, implying that if one should restrict UP heuris­ tics by means of PROP, he should restrict UP heuristics to those variables having a sufficient number of binary occurrences. For this reason, all restrictions on PROP studied in this paper are defined according to the number of binary occurrences of a variable, so that the resulted UP heuristics rely on combinations of unit propagation and Mom's heuristics.

Figure 3: PROP predicate hierarchy by inclusion relation. PRO P;j ( x) is true iff x has i binary occurrences of which at least j negative and j positive.

The first PROP predicate in our experimentation is called P ROPa and has empty denotational semantics, the resulted branching rule using a pure Mom's heuris­ tic, and the second is called P ROP0 whose denotational semantics is the set of all free variables, the resulted UP heuristic is in its pure form and plays its full role:

PROPa: PROPa(x) is false for every free variable x; PRO Po: PRO Po ( x) is true for every free variable x.

Between PROPa and PROP0 , there are many other possible PROP predicates. Figure 3 defines 8 predicates constituting a hierarchy by inclusion relation of their de­ notational semantics.

PROP3141 is defined to be PROPa1, but for nodes under a fixed depth of a search tree, it is defined to be PRO P41· Let T be a constant, the last PROP predicate is named PRO Pz and is defined to be the first of the three predicates P ROP41, P ROPa1 and P ROPo (in this order) which has at least T variables in its denotational semantics.

Each PROP predicate results in a DPL procedure, P ROPa, P ROPo, P ROP3141 and P ROPz respectively giving Sat a, SatO, Sat3141 and Sat z , and PRO P;j giv­ ing Sat;j. These programs are different only in PROP predicate, except SatO which need not count the occur­ rences of variables.

We run the 12 programs (compiled using gee with op­ timization) on a PC with a 133 Mhz Pentium CPU under Linux operating system on a very large sample of ran­ dom 3-SAT problems generated by using the method of Mitchell et al.[Mitchell et al., 1992] . Given a set V of n Boolean variables { x1, x2, ... , Xn} , we randomly generate m clauses of length 3. Each clause is produced by ran­ domly choosing 3 variables from V and negating each with probability 0.5. Empirically, when the ratio m/n is near 4.25 for a 3-SAT formula F, F is unsatisfiable with a probability 0.5 and is the most difficult to solve. We vary n from 140 variables to 340 variables incrementing by 20, for each n the ratio clauses-to-variables (m/n) is set to 4.0, 4.1, 4.2, 4.25, 4.3, 4.4, 4.5. At each ratio and by each program, if n < 280 then 1000 problems are solved, if 280 :::; n :::; 300 then 500 problems are solved, if n = 320 then 300 problems are solved, and if n = 340 then 100 problems are solved. A problem is solved suc­ cessively by all the 12 DPL procedures before another to ensure the same environment to all programs. Due to the lack of space, we only present the experimental results for the ratio mjn = 4.25 in Figures 4, 5, and 6, where the DPL procedures corresponding to the curves are listed in the same order from top to bottom. The experimental results on the other ratios give exactly the same conclusions.

3 A Pure UP Heuristic Versus a Pure Mom's Heuristics: SatO vs Sata

SatO systematically examines all the variables by unit propagation at all nodes, using a pure UP heuristic, while Sata does not examine any variable so and em­ ploys a pure Mom's heuristic. One might believe that SatO would be simply too slow, but it is not the case. SatO is much faster than Sata. In fact from Figures 4 and 5, all DPL procedures using a UP heuristic in our experimentation are substantially better than Sata in terms of search tree size and real run time.

Note that Mom's heuristic used in Sata is similar to the so-called two-sided Jeroslow-Wang rule [Hooker and Vinay, 1995], with the only difference that a clause of length i is counted as 5 clauses of length i+1 instead of 2. Our experiments suggest that 5 is better than 2. 5 is also similar to the exponential factors in C-SAT [Dubois et al., 1993] where 5.71 ternary clauses are counted as 1 binary clause.

SatO actually is slower than five other programs based on balanced restrictions of variables to be examined by unit propagation, but not substantially so (except Sat z ). The surprisingly good performance of SatO confirms the power of UP heuristics for selecting the next branching variable and suggests that its effect for detecting failed literals is only secondary.

4 Restricted UP Heuristics

Figure 6 illustrates the number of variables examined by different restricted UP heuristics at a node.

searCh tree depth

Figure 6: Average number of variables examined at a search tree node in a given depth when solving hard random 3-SAT problems of 300 variables and 1275 clauses (500 problems are solved) for 9 programs

4.1 Restriction by total number of binary occurrences of a variable

Four programs Sat10, Sat2o , Satao and Sat4o realize this type of restrictions. While a classical Mom's heuristic selects the next branching variable having maximum bi­ nary occurrences, the restricted UP heuristics examine a set of variables having more binary occurrences than others, including the variable having maximum binary occurrences. From Figure 4, it is clear that the more variables are examined, the smaller the search tree size IS.

4.2 Balanced restriction by total number of binary occurrences of a variable

Four programs Sat21, Sata1, Sat41 and Sat42 realize this type of restrictions. The PROP predicates require that a variable occurs both positively and negatively in bi­ nary clauses to balance the search tree. We compare the duet Sat;o and Satil (i=2, 3, 4) and observe that Sat;1 examines strictly fewer variables than Sat;o and is faster than it in spite of a slightly larger search tree. In partic­ ular, Sat41 and Sat40 examine almost the same number of variables (see Figure 6), but the balanced restriction gives a faster .DPL procedure.

We pay special attention to PRO Pal and PRO P41 since they seem to be the best balanced restrictions.

4.3 Dynamic restriction as a function of search tree depth

Sat3141 realizes this restriction. A general observation when solving 3-SAT problems using a DPL procedure is that there are more and more binary clauses when descending from the search tree root and the denotationa! semantics of a PROP predicate such as P ROPa1 becomes larger and larger. Furthermore, the nodes are more numerous near the leaves and the branching vari­ ables play a less important role there. It appeared that one could restrict more the variables to be examined by unit propagation near the leaves without important loss on the search tree size so as to obtain some gain in terms of real run time.

POSIT's UP heuristic (called BCP-based heuristic) [Freeman, 1995) realizes this idea: under the level 9 of a search tree, at most 10 variables are examined by unit propagation .

Sat3141 uses P ROPa1 from the top of a search tree, but under the depth empirically fixed to n * 4/70, it uses PRO P4 ~, where n is the number of variables in the initial input 3-SAT problem. Note that if n 2:: 160, n * 4/70 2:: 9, so Sata141 generally strengthens the restriction later than POSIT.

From Figures 4 and 5 Sat3141 is not better than Sata1 , although it makes many fewer unit propagations to ex­ amine variables (see Figure 6), suggesting that the search tree depth is rather irrelevant to the restriction of UP heuristics.

4.4 Dynamic restriction by number of variables to be examined

The relatively poor performance of Sat42 seems due to the small number of variables examined at each node (see Figure 6) , though these variables have many binary occurrences. A careful analysis shows that even Sata1 , the best one up to now, examines few or no variables at some nodes, especially near the root where there are few binary clauses, although these nodes are more de­ terminant for the final search tree size. PRO Pz is then introduced to ensure that at least T variables are exam­ ined at each node, T being empirically fixed to 10. Near the root , all free variables are examined to exploit the full power of UP heuristic. As soon as the number of variables occurring both negatively and positively in bi­ nary clauses and having at least 4 (3) binary occurrences is larger than T, only these variables are examined to se­ lect the next branching variable.

5 Related Work

C-SAT [Dubois et al. , 1993) examines some variables by unit propagations (called local processing) near the bot­ tom of a search tree to rapidly detect failed literals there. Pretolani also uses a similar approach (called pruning method) based on hypergraphs in H2R [Pretolani, 1993) . But the local processing and the pruning method as are respectively presented in [Dubois et al., 1993) and [Pre­ tolani , 1993) do not contribute to the heuristic to select the next branching variable. We find the first effective exploitation of UP heuristic in POSIT [Freeman, 1995)

and Tableau [Crawford and Auton, 1996] which use a similar idea as in C-SAT to determine the variables to be examined at a node by unit propagation: x is to be examined iff x is among the k most weighted variables by a Mom's heuristic.

The main difference of Satz with Tableau and POSIT is that Satz does not specify a upper bound k of the number of variables to be examined at a node by unit propagation. Instead, Satz specifies a lower bound. In fact, Satz examines many more variables by an optimal combination of unit propagation and Mom's heuristics.

Given the depth of a node, Table 1 illustrates the aver­ age number of variables examined ( #examined_vars) at the node by Satz, with the depth of the root being 0. In order to compare with C-SAT, Tableau and POSIT we also give the theoretical value of kc (for C-SAT), kT (for Tableau) and kp (for POSIT) at the node, respectively according to the definitions of k in [Dubois et al., 1993; Crawford and Auton, 1996; Freeman, 1995].

It is clear that Satz examines many more variables at each node than any of C-SAT, Tableau or POSIT. Near the root, Satz examines all free variables. Elsewhere Satz examines a sufficient number (T) of variables.

We compare C-SAT, Tableau, POSIT and Satz on a large sample of hard random 3-SAT problems on a SUN Spare 20 workstation with a 125 MHz CPU. The 3-SAT problems are generated from 3 sets of n variables and m clauses at the ratio m/n = 4.25, n steping from 300 variables to 400 variables by 50.

We use an executable of C-SAT dated July 1996. The version of Tableau used here is called 3tab and is the same used for the experimentation presented in [Craw­ ford and Auton, 1996]. POSIT is compiled using the provided make command on the SUN Spare 20 workstation from the sources named posit-l.O.tar.gz 1 . Table 2 shows the performances of the 4 DPL procedures on problems of 300, 350, and 400 variables, where time standing for the real mean run time is reported by the unix com­ mand fusr/bin/time and Lsize standing for search tree size (number of nodes) is reported (or computed from number of branches reported) by the DPL procedures.

Table 2 shows that Satz is faster than the above cited versions of C-SAT, Tableau and POSIT, Satz's search tree size is the smallest, and Satz's run time and search tree size grow more slowly. Table 3 shows the gain of Satz compared with the cited version ofC-SAT, Tableau and POSIT at the ratio m/n=4.25. Each item is com­ puted from Table 2 using the following equation:

where value is real mean run time or real mean search tree size and system is C-SAT, Tableau or POSIT. From Table 3, it is clear that the gain of Satz grows with the size of the input formula.

The central strategy of Satz is to try to reach an empty clause as early as possible. Further along the line, we make two relatively small resolvents-driven improve­ ments in Sat z. The first improvement is the preprocess­ ing of the input formula by adding some resolvents of length :S: 3, The second improvement consists in refin­ ing yet more the heuristic H in the nodes where all free variables are examined by unit propagation. Refer to Figure 2, when PROPz is equal to PROPo we define w(x) as the number of resolvents the newly produced binary clauses would result in in F' by a single step of resolution. w(x) is similarly defined.

1 publicly available via anonymous ftp to ftp.cis .upenn .edu in pub/freeman/ directory

Satz improved in this way solves many real-world or structured SAT problems where previous heuristics were not successful. For example, Table 4 shows the perfor­ mance of the 4 DPL procedures on the well-known Bei­ jing challenging problems 2 , where a problem that can not be solved in less than 2 hours is marked by "> 7200" and the version of Tableau is called ntab 3 . It is clear that Satz is much more efficient and solves many more problems in less than two hours.

6 Conclusion

We found that UP heuristic is substantially better than Mom's one even in its pure form realized by P ROPo where all free variables are examined at all nodes. In its restricted forms based on combinations of unit prop­ agation and Mom's heuristics, the more variables are examined, the smaller the search tree is , confirming the advantages of UP heuristic, but too many unit propaga­ tions slow the execution. The combinations realized by PROP41 and PROP31 represent good compromises.

A dynamic restriction such as P ROP3141 which strengthens the restriction under a fixed depth of a search tree fails to work better than the static restric­ tion PRO P31 . We design the dynamic restriction along another line: P ROPz ensures that at least T candidates are examined by unit propagation at every node of a search tree by successively using P ROP41 , P ROP31 and PROPo, giving the very efficient and very simple DPL procedure called Satz.

Satz is favorably compared with several current state­ of-the-art DPL implementations (C-SAT, Tableau and POSIT) on a large sample of hard random 3-SAT prob­ lems and the recent Beijing SAT benchmarks. The good performance of Satz on the structured or real-world SAT problems shows that UP heuristic can tackle new prob­ lems or problem domains where Mom's heuristics were not successful and enhances the belief that if a DPL pro­ cedure is efficient for random SAT problems, it should be also efficient for a lot of structured ones.

2 available from http:/ fwww.cirl.uoregon .edu/crawford/beijing

3 available from http:/ fwww.cirl.uoregon.edu/crawford/

Acknowledgments

We thank Olivier Dubois, James M. Crawford and Jon W. Freeman for kindly providing us their DPL proce­ dures and anonymous referees for their comments which helped improve this paper.