Hidden Gold in Random Generation of SAT Satisfiable Instances

1 Introduction

A crucial problem in practical AI development is the problem of satisfiability (called SAT) of a finite set of propositional clauses. SAT is a NP-complete problem. Which AI system does not use a satisfiability test or equi~alent (Constraint Satisfaction Problem, Graph colonng, ... )? Formal reasoning is limited because there is no efficient propositional theorem prover. On one hand, the complete methods that solve SAT have not really progressed since the res~lution method and Davis-Putnam procedure, except that 1t has been shown that the choice of the heuristics is central [Dubois et al., 1993]. On the other hand, the incomplete methods have been really developed thanks to the results of GSA T for the random instances [Selman eta/., 1993].

A threshold phenomenom has been brought to light for the generation of random instances [Cheeseman et a/., 1991 ], making possible the generation of random hard !nstances. Satisfiable instances are needed for evaluating the mcomplete methods. But only 50% of the hardest instances are satisfiable. It has been shown [Chv;'ltal and Szemeredi, 1988] that the unsatisfiable instances are hard (for the resolution) but it has not been shown (Cha and Iwama, 1995] that the satisfiable instances are difficult (for the local search for exampl~). In works on evaluation of incomplete methods, [Konohge, 1994] showed the inefficiency of GSA T on random structured instances, compared with Davis-Putnam procedure. But with few changes, GSA T becomes efficient [Kask and Dechter, 1995]. May be it is

Michel Cayrol ·

IRIT - Universite Paul Sabatier 118, route de Narbonne 31062 Toulouse Cedex France

due to the fact that these structured instances are not intrisically har~. But, what is it the definition of intrisically hard? So, a mam problem about SAT is to determine if a set of instances is hard. There are no general definition and determination method of the complexity of a set of instances (except when a polynomial class is recognized). For this reason, empirical methods are used for showing the difficulty of the instances produced by a generator. A hard set of instances is a set of instances which are hard for the best kno~n algorithms, namely the "Davis-Putnam" procedure [Dav1s eta/., 1962], GSAT with random walk [Selman and Kautz, 1993] and the Break Out Method (Morris, 1993].

2 The kSA T Uniform Random Generation

An instance of kSA T is produced by the uniform random ?eneration if e~ch clause of the instance is randomly and mdependently picked out. These instances are generated from two parameters: the number of variables and the ratio. The ratio is defined as the number of clauses divided by the number of variables. The uniform generation of kSA T instances is an interesting theoretical problem. A threshold phe~omenom ha~ been b.rought to light for the probability to p1ck out a satisfiable mstance as a function of the ratio [Cheeseman eta/., 1991] [Crawford and Auton, 1993]. The thr~shold s~ems to ~ppear when the probability to generate a satisfiable mstance IS equal to 112. The value of this critical ratio has been determined (empirically) as 4.25 for 3SAT 9.8 for 4SAT etc [Mitchell et a/., 1992] [Dubois et a/.: 1993] . A problem is to determine theoretically this threshold. Near the threshold, if the ratio decreases the pro?ability to pick out a satisfiable instance quickly tends to 1; .If the ~atio increases, the probability to pick out a satisfiable mstance quickly tends to 0. The more important the number of variables, the more quickly the probability tends to 0 (or 1~. Moreover, it has been shown (empirically) that the hardest mstances are generated for a ratio value equal to the threshold. For other values, the instances are easier.

. This generation method is used for evaluating complete or mcomplete theorem provers. In the hardest region, it has been p~oved that inconsistent instances are difficult (for the resolutiOn) [Chvata! and Szemeredi, 1988]. But there is no theoretical result for the difficulty of the satisfiable i~stances. Futhermore, for generating hard instances, the higher the number of variables, the more the value for the ratio is precise. A little variation on the ratio can produce only satisfiable or only insatisfiable instances.

For example, if the theoretical value of the critical ratio for 1000 variables is equal to 4.255 then the uniform generation would produced, for I 000 variables and with a ratio equal to 4.25, more than 50% of satisfiable instances. In this case, the evaluation of a local search algorithm under the assumption "50% satisfiable" is a big mistake.

With a lot of variables, the complete methods are unusable. Thus it is impossible to know the rate of success of the incomplete methods. The uniform generation is not a good means for evaluating the incomplete methods if the theoretical precise value of the threshold is not known.

3 Satisfiable Instances

The algorithm kSAT_GEN presented in [Cha and Iwama, 1995] produces only random satisfiable instances. The clauses are randomly constructed in order to be satisfied by a given model. There are several generation parameters: number of variables, ratio and literal distribution (i .e. the number of occurrences of each literal in the generated set of clauses). In [Cha and Iwama, 1995], there is no result on the relation between the parameters and the difficulty of the instances. For not producing only easy instances, the studies on the uniform random generation have shown the importance of the value of the parameters. There are a lot of parameters for kSAT_GEN, then it will be difficult to make exhaustive tests.

Two other methods are proposed [Cha and Iwama, 1995] for generating always inconsistent sets of clauses or sets of clauses having one and only one model. The basic steps of these generators are the reversal resolution principle and the reversal subsumption simplification (a clause Cl subsumes a clause C2 iff C I ~ C2). If the generation is reversed, a resolution proof can be easily obtained. The time of the generation of the sets of clauses must be limited. So there is a short proof, by resolution, of the empty clause for the inconsistent sets of clauses. And there is a short proof, by resolution, for each prime implicate for the sets of clauses having only one model. The smaller the generation time, the smaller the resolution proofs! This kind of instances is not intrinsically hard, because the resolution proof of the prime implicates is short. A very good resolution-based theorem prover would be able to solve easily this kind of instances.

Let x be a propositional symbol; x is called a positive literal and ...,x is called a negative literal. One possibility for generating only consistent sets of clauses is to leave out the clauses that have only positive litterals, from a set of clauses generated by uniform random generation (this idea appears in [Morris, 1993] [Rauzy, 1995]). For these instances, a model is obtained by assigning false to all the variables. Unfortunately, this method often produces easy instances. It is due to the fact that the clauses with only positive literals are left out, so there more negative literals than positive literals. Consequently, the Davis-Putnam procedure easily finds a model (with a good heuristic).

Moreover, [Rauzy, 1995] has noticed that only "nearly Hom-renamable" instances are generated. To generate hard instances, new parameters must be introduced.

Each clause has a negative literal. An "intelligent" algorithm would be able to show this property. To solved that problem, some literals of the instances have to be renamed (swap x and ...,x for some x), and then some clauses without negative literal appear.

4 How to be Hard

Let us consider the case where the clauses without negative literals are left out. In order to control the proportion of positive and negative literals, [Rauzy, 1995] introduces parameters for determining the probability to pick out a given sign of a clause. For 3SAT, there are four kinds of sign for a clause: (i) all the literals in the clause are positive, (ii) two literals are positive and one is negative, (iii) one literal is positive and two are negative, (iv) all the literals are negative. So there are four parameters for the generation: 8 the probability to pick out a clause (i), y for a clause (ii), ~ for a clause (iii) and a for a clause (iv).

The probability to pick out each sign of a clause is a=8=l/8 and ~=y=3/8 for the uniform random generation. With a probability equal to 8=0 to pick out a clause which sign is (i), and with given probabilities for the others, [Rauzy, 1995] proposed two equations for generating instances (before renaming) with approximatively the same number of positive and negative literals:

1. a+~+y=l (since clauses with only positive literals are rejected)
2. 3a+~=y (for the equilibrium between positive and negative literals)

For the sake of simplicity, a restrictive strategy is chosen in our work. Only one parameter is introduced: the probability to pick out a positive literal , called posp. The following algorithm is proposed:

function J<Sl\T_satisfiable(k, nbv, ratio, p::sp)

input: k = J:UTb:r of literals per clause, nbv = J:UTb:r of variables, ratio = value for J:UTb:r of variables/J:Ulb:r of clauses, p::sp = prd:abilit:y to pick rut a p:sitive literal (0 ~ p::sp < 1) ·

output: a satisfiable instaoce of kSliT B := 0; n1::c := 0; while (d::c < rbv*ratio) do {xl, ... , XJc} :=a ran:bn IBrt of tre set of tre nbv variables; Clause := 0; for i := 1 to k do let p be a ran:bn J:UTb:r cm::n:)' [0, 1 [; if (p ~ p::sp) then Clause := Clau.seJ{xil; else Clause := Clau.seu{·xil; if a ne:;Jative literal belcnJS to Clause then B : = R.J {Clause} ; d::c : = nl:x::+ 1; ren:rre B; %sl.ap X an:i 'X for tore prq;ositirnal S}fli::ol X %

return B;

5 Hidden Gold

In order to obtain instances of 3SAT consisting of sets of clauses with the same expected total number of positive and negative literals, ip the S~llJe method as [Rauzy, 1995], posp must be equal to ~ .f5 - I) j 2 ~0.61803.

Indeed, with the generator, the values of a,f3,y in function ofposp are: a=(l-posp)3/(1-posp3) , ~=3posp.(l-posp;2!(1posp3) and y=3posp2(1-posp)/(l-posp3).

In order to satisfy e}luatio~s (1) and (2) there is only one solution for posp: ~"{5 - IJ/2 . We've just found the expected gold, this value is equal to

6 Search Algorithms

The generator kSAT_satisfiable has been tested on three classical different methods. This generator has also been used to evaluate two new personal versions of the Break Out method.

6.1 Complete Method

We use the classical "Davis-Putnam" procedure (DP). It is an enumeration of the interpretations. With sophisticated heuristics, it is the most efficient complete algorithm for the uniform random instances of kSAT. For our tests, an implementation with heuristics of C-SA T is used [Dubois et a/., 1993]. C-SAT generally solves in few seconds hard instances (from uniform random generation) having 200 variables. Instances having 300 variables are solved in less than one hour. Instances having more than 500 variables require some days, years or much more ...

6.2 Incomplete Methods

These methods are incomplete because they cannot always find a model. But they can solve very large problems [Selman et a/., 1992]. At the present time, the best algorithms for SAT are based on the hill-climbing algorithm. For a given interpretation, these methods try to decrease, by local changes on the interpretation, the number of falsified clauses. A local change in the interpretation is an inversion of the truth value of a variable, called flip of the variable. For these methods, the crucial problem is to escape from a local minimum.

We used the Break Out Method (BOut) [Morris, 1993] and GSAT with random walk [Selman and Kautz, 1993]. BOut escapes from a local minimum by weigthing the falsified clauses on that local minimum. The results presented in [Cha and Iwama, 1995] show that this method seems to be better than GSA T which is supposed to be the best incomplete method for solving SAT. GSAT [Selman eta/., 1992] is the more popular incomplete algorithm for SAT. There exists some refinements, in particular a notion of weighting [Selman and Kautz, 1993] as for BOut. For the tests, we used the version with random walk. A random walk is an elementary improvement for escaping from local minima: with a given probability, a variable that appears in a falsified clause is flipped.

6.3 Escaping from a Local Maxima

Break Out Method with Jump

Now an improvement of BOut is presented. It is called the Break Out Method with Jump (BOJ). On a local minimum very often the same clauses are falsified. To avoid that, on a local minimum, all the variables that appear in the falsified clauses are flipped. Thus several flips have to be done for falsifying again these clauses.

Another change is introduced. In some cases, the current interpretation tends to the opposite of a model; in order to solve that, the following property is used: when the sum of the weights of the clauses that are totally satisfied (each literal of the clause is satisfied) is lower than the sum of the weights of the falsified clauses, if all the variables are flipped, the new interpretation is better.

The Break Out Method with Jump is represented by the following algorithm:

function IDJ(B) : l:xnle3Il

input : a set B of clauses.

output : true if B is satisfiable.

let I an initial ran::bn :interpretatim;

until (I ~:::€!:ores a ITO:El of B) do

if (tre sun of t:re \\eights of t:re totally satisfied clauses is la.-.er than t:re sun of t:re \\eights of t:re falsified clauses)

then all t:re variables of I are fliw:rl;

if (I is rot a local m:in:irrun) then

R:ss_flips:=tre set of t:re variables th3.t minimize t:re sun of t:re \\eights of t:re falsified clauses;

flip m I a variable fran R:ss_flips;

else ad:l a \\eight to t:re falsified clauses; flip m I all t:re variables th3.t ~ :in t:re falsified clauses;% jurp %

return True;

A Specialized Algorithm: Mirror

This variation of BOut called Mirror is presented because its efficiency is a mystery for us. Its principle is simple. It is BOut with only one new operation. On a local minimum, falsified clauses are normally weigthed and immediately after all the variables are flipped (it is the reason for the name Mirror). In the hardest areas of the other incomplete algorithms, this method is amazingly efficient. But it has a lot of problems on obvious areas. Moreover this method seems to be efficient only with our generator.

7 Empirical Results

The figures appear at the end of the paper.

kSAT_satisfiable has been tested with a lot of values for nbv, ratio and posp, for the 3SAT case. Each point is calculated from a sample of I 00 instances. Only general results for 100 variables are presented (the results are similar for 50, 150 and 200 variables). Here we are interested in the behaviour of the different methods as well as the easy and hard instances of the generator. Comparing the algorithms is outside the scope of the paper.

The complexity of Davis-Putnam procedure is measured in terms of the sum of the average number of calls, the number of unit propagations and the number of pure literal simplifications (a literal is a pure literal for a set of clauses if its complementary literal does not appear in this set). The complexity of the incomplete methods is measured in terms of the average number of tested interpretations. This measurement is more precise than the number of flips . Indeed, in order to choose a best neighbour, a local search method inspects the interpretations in the neighbourhood of the current interpretation (explicitly or implicitly). Therefore, this measurement enables us to differenciate algorithms which do not have the same kind ~f neighbourhood, or which do not explore the search space m the same way.

The most classical parameters are chosen for the incomplete algorithms. The initial weight of the clauses is fixed to one and a unit weight is added on local minima. The probability of the random walk for GSAT is equal to 1/2. In order to avoid a too quick restart, no restart is realized. The programs are stopped after 100 000 flips , but GSA T with random walk is stopped after 200 000 flips . It is a high value compared to values used in experimentations with uniform random generation. Experimentations indicate that GSA T with random walk needs in average 27 654 flips and almost no restart in order to prove the consistency of the instances composed of 200 variables generated at the threshold by the standard model [Selman eta/. , 1994].

7.1 The Hardest Areas

As for the ratio of instances solved (figure I), for DP it is equal to I 00%, which is not surprising since DP is a complete method. The performances of GSA T with ran do~ walk are poor: close to 0% of instances solved for a ratiO equal to 8 and posp = 0.8. BOut behaves better but still have big weaknesses. BOJ behaves quite well, almost . all instances are solved. Moreover, BOJ has the same behavtour of the other algorithms, but the failure starts only at around 200 variables. As for complexity (figure 2), GSAT, BOut and BOJ have similary curves. The complexity of these algorithms grows with the ratio. It is more simple for DP, the form of the complexity is easy-hard-easy. It is like the uniform random generation. The hardest areas are located at a ratio,4.4 and posp,0.64. However, the same "ridge" of hardness is present in DP: when ppos increases with the ratio.

We could conclude that this model for generating consistent instances generates hard instances and that the region of the hardest instances follows a ridge which is common to all methods: when ppos increases with the ratio.

But we are immediately going to check that this conclusion is erroneous.

7.2 Calling the conclusions into question

We must not conclude too quickly, even if some evidences are showed. We are going to show that the presence of a common ridge in the complexity curves is not directly linked with the hardness of instances but with the methods used. To show this, we are going to make again the tests with Mirror, figure 3. Moreover, when describing the DP procedure used in the experimentations, we omitted an important factor: the presence of a heuristics in the choice of the first subtree explored (heuristics of S-SA T [Dubois et at., 1993]). We are also going to make again the tests with DP, but with a choice of the first subtree explored which is opposed to that proposed by the heuristics and which is random, figure 4.

The curves always show the presence of a ridge, but here posp decreases when the ratio increases! For a high posp value and a high ratio, we observe that the generated instances are easy for Mirror: 100% of the instances are solved quickly. And for the hardest area of Mirror (low posp value and a high ratio), the generated instances are easy for BOut, BOJ and GSAT: 100% are solved quickly.

When the first subtree explored by DP is selected randomly then the two ridges appear, figure 4.

8 Conclusion

With the kSA T -consistent function, it is easy to generate hard satisfiable instances. These instances turn out to be practically much harder than instances generated by the standard random model. 50 variables are enough to make GSAT+random walk and the Break Out Method little efficient. The generated instances have no structure and yet they are very hard to solved (by almost the most popular algorithms). As for the efficiency of local search, the results of Mirror bring into light gaps of classical approaches. There exists instances generally simple to solve (byMirror) which may be extremely difficult for methods such as GSAT and the Break Out Method. An important result of our tests is that incomplete algorithms must be evaluated with all the different areas, and not only on the hardest areas of a given algorithm. If Mirror was tested only on the hardest area of BOut or GSAT, a mistake would be made on its efficiency.

New operations must be integrated to local search in order to make it more robust. The flip of the whole set of variables (mirror) is one of our proposals, but up to now this operation gives interesting results on this model of generation only. In order to capture the good characteristics of BOut, GSA T and Mirror, the BOJ algorithm has been developed. On our generator, BOJ improves BOut and seems also better on other kinds of instances.

We venture to conjecture that for the kSA T -consistent function, the generated instances which are the hardest to solve are, independently from the method used, located on a ratio "" 4.4 and posp :::: 0.64. For a given algorithm, the presence of a zone harder than this point brings into light the gaps of the evaluated method. ·

Generally speaking, the kSA T -consistent function shows that, as complete methods, local search has weaknesses and allows for instances that are not solvable in a reasonable amount of time . As for the uniform generation, the simplified model generation of satisfiable instances must be intensively studied.

Acknowledgments

To Elsa, Claudette for helping us with English, Jerome for helping us finishing the paper and the members of RES SAC.