Forced Satisfiable CSP and SAT Benchmarks of Model RB

------Hiding Solutions with Growing Domains


If you have any comments or need more instances for the following CSP and SAT benchmarks, please send me an email.


SAT Benchmarks

The Boolean Satisfiability Problem (SAT) is a core of NP-complete problems and is central in the theory of computation. Finding challenging benchmarks for the satisfiability problem is not only of significance for the experimental evaluation of SAT algorithms but also of interest to the theoretical computer science community.  Identifying new challenging SAT benchmarks is also an important purpose of every year's SAT competition where the benchmarks are usually divided into three categories: randomly generated uniform k-SAT, applications and crafted. Although there have been a large number and various types of SAT benchmarks available for testing, the benchmarks which are guaranteed to be satisfiable are still in short supply. Recently, we proposed a new method to generate hard satisfiable problem instances. Following this method, we present here some satisfiable SAT benchmarks which are directly encoded from forced satisfiable CSP instances of Model RB with k=2, α=0.8 and r=0.8/(ln4-ln3). All instances are located in the exact phase transition point of Model RB identified by Theorem 2 in Ref. [1], i.e. the constraint tightness p=pcr=1-e-α/r =0.25.  For the details about how to choose values of these parameters, please see section below about CSP benchmarks. In fact, based on Model RB and the direct encoding of CSP into SAT, we can propose a simple random SAT model as follows:

  1. First generate n disjoint sets of boolean variables, each of which has cardinality nα (where α>0 is a constant), and then for every set, generate a clause which is the disjunction of all variables in this set, and for every two variables x and y in the same set, generate a 2-clause ¬x¬y.

  2. Randomly select two different disjoint sets and then generate without repetitions pn2α clauses of the form ¬x¬z where x and z are two variables selected at random from these two sets respectively (where 0<p<1 is a constant);

  3. Run Step 2 (with repetitions) for another rnlnn-1 times (where r>0 is a constant);

It is easy to see that to satisfy an instance generated by the model above, exactly one variable from every disjoint set can take value 1, and if this is the case and no random clause is violated by this assignment, then the instances is satisfiable. To hide a satisfying assignment, we first select a variable at random from each disjoint set to form a set of n variables which take value 1, and then in the above process of generating random clauses (Step 2), no clause is allowed to violate this hidden assignment. For related theoretical and experimental results, please see Ref. [2] and Ref. [3].  Briefly speaking, it has been predicted by theoretical analysis and confirmed by experiments that for Model RB, when the values of parameters are within the range allowed by theorems of exact phase transitions, forced satisfiable formulas are almost as hard as random satisfiable formulas. Experiments further demonstrate that the hardness of solving such forced formulas (in both SAT and CSP format) grows very rapidly with the problem size in the phase transition region. Based on such an observation, we get a natural and simple method to generate only satisfiable formulas, the hardness of  which can be easily tuned by varying the problem size (or the constraint tightness). Because of the advantages of generating only satisfiable formulas and being easy to implement, this method is well-suited for the study and experimental evaluation of SAT and CSP algorithms, especially those of local search style. Along this line, in what follows, we provide 8 benchmark sets of forced satisfiable SAT formulas, with the problem size growing from 450 Boolean variables to 1534 Boolean variables.

Note: The following SAT benchmarks are expressed in the DIMACS CNF format.

News

List of Papers That Use SAT Benchmarks of Model RB (Updated: Mar. 4, 2009)


CSP Benchmarks

Generating Asymptotically Hard CSPs
A Constraint Satisfaction Problem, or CSP for short, consists of a set of variables, a set of possible values for each variable (its domain) and a set of constraints defining the allowed tuples of values for the variables (a well-studied special case of it is SAT). The CSP is a fundamental problem in Artificial Intelligence, with a distinguished history and many applications, such as in knowledge representation, scheduling and pattern recognition. To compare the efficiency of different CSP algorithms, some standard random CSP models have been widely used experimentally to generate benchmark instances in the past decade. To overcome the trivial asymptotic insolubility of such models, an alternative random CSP model was proposed in Ref. [1] as follows:

Model RB: Given a set V of n variables, first, we select with repetition m=rnlnn random constraints (r>0 is a constant), each of which is formed by selecting  k different variables at random from V, where k>=2 is an integer (k=2 for binary CSPs). Next, for each constraint, we uniformly select without repetition q=pdk incompatible (unallowed) tuples of values (i.e. nogoods), where d=nα is the domain size of each variable (α>0 is a constant).

Please note that  the way of generating random instances for Model RB is almost the same as that for standard Model B except that Model RB allows the repetition of constraints (which can greatly simplify the theoretical analysis but has no effect on the results). The main change of Model RB with respect to Model B is that the domain size of Model RB grows polynomially with the number of variables while the domain size of Model B is fixed. In fact, it is exactly such a change that results in the great differences between Model B and Model RB with respect to the asymptotic phase transition and computational complexity. Specifically, Model B suffers from trivial local inconsistencies and is asymptotically easy to solve while model RB not only has exact phase transitions but also can generate asymptotically hard instances. In what follows, we will give an example to show how Model RB can be used for producing asymptotically hard CSPs.

Example. If we choose α=0.8 and r=0.8/(ln4-ln3)=2.7808, then as the number of variables increases, we can get the following tuples of values for Model RB (Note: If non-integer values occur in the computational results, then we round them to the nearest integers).
 
n d=nα m=rnlnn
n=30 d=15 m=284
n=35 d=17 m=346
n=40 d=19 m=410
n=45 d=21 m=476
n=50 d=23 m=544
n=53 d=24 m=585
n=56 d=25 m=627
n=59 d=26 m=669
... ... ...

By Theorem 2 in Ref. [1], for the values of CSP parameters chosen above, as n approaches infinity, the satisfiability phase transition will occur  when the constraint tightness p equals pcr=1-e-α/r =0.25 (i.e. the exact phase transition point determined by  Theorem 2). Please note that the phase transition is an asymptotic phenomenon. In this sense, only for infinite n, there can, strictly speaking, occur sharp phase transitions (including the exact phase transitions found in Ref. [1]) . Thus, in the case of finite n for Model RB, there usually exists some difference between the phase transition point determined exactly by theorems and the one found in experiments. Generally speaking, this difference converges to zero rapidly with n and, for fixed n, the larger the value of r (i.e. the denser the constraint graph), the smaller the difference. In Ref [2], it was proved that almost all instances of Model RB have no tree-like resolution proofs of less than exponential size, which means that RB is hard for all CSP algorithms based on tree-like resolutions. Another point worth mentioning is that the exact phase transitions of Model RB are established by non-algorithmic methods, which says nothing about, and seems unlikely to be useful for, designing algorithms, and so implies that the phase transitions of Model RB can hopefully provide a reliable source to generate hard instances (For more discussions about this, please see Ref [2]). Experiments further showed that the hardness of solving instances of Model RB grows exponentially in the phase transition region, and such instances appear to be very hard to solve even when the number of variables is only moderately large. Therefore, by generating instances of Model RB in the exact phase transition point (p=0.25 for the values of CSP parameters chosen above), and by varying the number of variables, we get a natural method to generate random hard CSP instances with controllable hardness, almost as convenient as in experimental SAT studies (where it often suffices to generate random 3-SAT instances of n variables and 4.25n clauses with varying n).

From the definitions of Model B and Model RB, it is easy to see that, simply by allowing the repetition of constraints, any generator of Model B can be used to generate random instances of Model RB when the values of CSP parameters (i.e. n, d, m and q) are fixed. In this sense, we can say that Model B is still useful for generating asymptotically hard CSPs in the phase transition region of non-trivial threshold behaviors. However, to achieve this, a natural and convenient way is to vary the values of CSP parameters under the framework of Model RB (like the example above) and make them satisfy the conditions specified by the theorems in Ref. [1] (e.g. the tightness is allowed to be at most and up to 50% for binary CSPs). Remark: As mentioned above, the same results hold for Model RB if the selection of constraints is performed without repetition. The reason for this is that the number of repeated constraints is asymptotically much smaller than the total number of constraints and thus can be neglected in the analysis. Based on this point and by the same way as above, any generator of Model B can also be used directly to generate asymptotically hard CSPs.

Generating Hard Satisfiable CSPs
To evaluate the performance of incomplete algorithms, we need a source to generate only satisfiable instances, especially hard ones. The class of random satisfiable instances is obviously a good candidate. However, to do this, a complete algorithm has to be used as a filter, which unavoidably restricts the hardness of instances that can be obtained in this way. In fact, there is a natural strategy of generating only satisfiable instances: First generate a random assignment t, and then generate a certain number of constraints one by one to form a random instance, where any constraint violating the assignment t will be rejected. In this way, every instance generated will at least have one solution, i.e. the forced assignment t. We call such instances as forced satisfiable instances.

It was recently shown by theoretical analysis in Ref. [2] that for Model RB, the number and distribution of solutions of forced satisfiable instances are almost the same as those of random satisfiable instances. Experiments further confirmed that for Model RB, when the values of parameters are within the range allowed by theorems of exact phase transitions, forced satisfiable instances are almost as hard as random satisfiable instances (Remark: This is very different from random 3-SAT where forced satisfiable formulas are much easier than random satisfiable formulas). Based on such an observation, we get a  natural and convenient method to generate hard satisfiable instances, i.e. generating forced satisfiable instances of Model RB with a large number of variables in the exact phase transition point (identified by Theorem 1 or Theorem 2 in Ref. [1]).  Following this method, which definitely needs to be tested more widely by more researchers, we provide here some forced satisfiable CSPs (with  p=0.25) using the values of CSP parameters chosen above. According to the experimental results of ours and some other researchers, the hardness of solving these instances grows exponentially with n (i.e. the number of variables) and the instances with n=59 appear to be very challenging to solve (for both complete and incomplete algorithms). If you can solve them in a reasonable time, please tell me and, of course, even harder instances with more variables can also be generated as needed by use of the method described above. Please see Ref [3] for more discussions on the theoretical and practical importance of Model RB.

Note: The following CSP benchmarks are essentially the same as the SAT benchmarks above except that they are in CSP format (where benchmarks differing only in the suffix are equivalent, e.g. frb40-19-1.csp and frb40-19-1.cnf). These CSP benchmarks are generated based on the uniform random binary CSP generator of Model B (designed by D. Frost, C. Bessière, R. Dechter and J.C. Régin) and are expressed in the same format as theirs.    

Remark: Christophe Lecoutre proposed a format using XML to represent CSP instances and made available online a lot of instances expressed in this format (including the above ones).  For more information, please follow this link.

News

  frb30-15-1.csp frb30-15-2.csp frb30-15-3.csp frb30-15-4.csp frb30-15-5.csp
Solved by 16 solvers 15 solvers 16 solvers 16 solvers 16 solvers
  frb35-17-1.csp frb35-17-2.csp frb35-17-3.csp frb35-17-4.csp frb35-17-5.csp
Solved by 13 solvers 13 solvers 15 solvers 16 solvers 12 solvers
  frb40-19-1.csp frb40-19-2.csp frb40-19-3.csp frb40-19-4.csp frb40-19-5.csp
Solved by 9 solvers 8 solvers 7 solvers 8 solvers 8 solvers
  frb45-21-1.csp frb45-21-2.csp frb45-21-3.csp frb45-21-4.csp frb45-21-5.csp
Solved by 1 solvers 3 solvers 3 solvers 4 solvers 5 solvers
  frb50-23-1.csp frb50-23-2.csp frb50-23-3.csp frb50-23-4.csp frb50-23-5.csp
Solved by 0 solvers 0 solvers 0 solvers 4 solvers 0 solvers
  frb53-24-1.csp frb53-24-2.csp frb53-24-3.csp frb53-24-4.csp frb53-24-5.csp
Solved by 0 solvers 0 solvers 0 solvers 0 solvers 0 solvers
  frb56-25-1.csp frb56-25-2.csp frb56-25-3.csp frb56-25-4.csp frb56-25-5.csp
Solved by 0 solvers 0 solvers 0 solvers 0 solvers 0 solvers
  frb59-26-1.csp frb59-26-2.csp frb59-26-3.csp frb59-26-4.csp frb59-26-5.csp
Solved by 0 solvers 0 solvers 0 solvers 0 solvers 0 solvers

List of Papers That Use CSP Benchmarks of Model RB (Updated: Mar. 4, 2009)


Other Benchmarks Based on Model RB


Benchmarks with Hidden Optimum Solutions for Graph Problems

Pseudo-Boolean (0-1 Integer Programming) Benchmarks with Hidden Optimum Solutions

Benchmarks with Hidden Optimum Solutions for Set Covering, Set Packing and Winner Determination

Weighted Max-2-SAT Benchmarks with Hidden Optimum Solutions (New!)

References

  1. K. Xu and W. Li. Exact Phase Transitions in Random Constraint Satisfaction Problems. Journal of Artificial Intelligence Research, 12(2000):93-103.
  2. K. Xu and W. Li. Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances. CoRR Report cs.CC/0302001, 2003. Revised version entitled "Many Hard Examples in Exact Phase Transitions" appeared in Theoretical Computer Science, 355(2006):291-302.
  3. K. Xu, F. Boussemart, F. Hemery and C. Lecoutre. Random Constraint Satisfaction: Easy Generation of Hard (Satisfiable) Instances. Artificial Intelligence, 171(2007):514-534. Earlier version entitled "A Simple Model to Generate Hard Satisfiable Instances" appeared in Proc. of 19th IJCAI, pp.337-342, Scotland, 2005.

Related Links

Fadi Aloul's SAT Benchmarks.
 


Back to Ke Xu's homepage.

Date Created: Oct. 23, 2003. Last Updated: June 5, 2007.