Forced Satisfiable CSP and SAT Benchmarks of Model RB

------Hiding Solutions with Large 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 of the generation method and related theoretical results, please see Ref. [2].  Briefly speaking, it has been predicted by theoretical analysis and confirmed by experiments that for Model RB, especially when α is large (i.e. having large domains), 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 format.

Remark: Some of the SAT benchmarks above were used for SAT Competition 2004 (55 solvers). The results are summarized as follows:


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 sparser 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, especially when α is large (i.e. having large domains), 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.    

Recently, 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.

Benchmarks with Hidden Optimum Solutions for Graph Problems

Pseudo-Boolean (0-1 Integer Programming) Benchmarks with Hidden Optimum Solutions (with results from PB 2005)

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.
  3. K. Xu, F. Boussemart, F. Hemery and C. Lecoutre. A Simple Model to Generate Hard Satisfiable Instances.  Proc. of 19th International Joint Conference on Artificial Intelligence (IJCAI-05), to appear.

Related Links

Fadi Aloul's SAT Benchmarks.
 

Back to Ke Xu's homepage.

Date Created: Oct. 23, 2003. Last Updated: Jul. 7, 2005.