Forced Satisfiable CSP and SAT Benchmarks of Model RB  A Simple Way for Generating Hard Satisfiable CSP and SAT Formulas
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 NPcomplete 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 kSAT, 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/(ln4ln3). 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=1eα/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:
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 2clause ¬x∨¬y.
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);
Run Step 2 (with repetitions) for another rnlnn1times (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 wellsuited 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.
frb3015cnf.tar.gz ( 254 KB): 450 Boolean variables, 19084 clauses  5 instances, all satisfiable
frb3517cnf.tar.gz ( 398 KB): 595 Boolean variables, 29707 clauses  5 instances, all satisfiable
frb4019cnf.tar.gz ( 589 KB): 760 Boolean variables, 43780 clauses  5 instances, all satisfiable
frb4521cnf.tar.gz ( 848 KB): 945 Boolean variables, 61855 clauses  5 instances, all satisfiable
frb5023cnf.tar.gz (1151 KB): 1150 Boolean variables, 84508 clauses  5 instances, all satisfiable
frb5324cnf.tar.gz (1370 KB): 1272 Boolean variables, 98921 clauses  5 instances, all satisfiable
frb5625cnf.tar.gz (1589 KB): 1400 Boolean variables, 114668 clauses  5 instances, all satisfiable
frb5926cnf.tar.gz (1824 KB): 1534 Boolean variables, 132295 clauses  5 instances, all satisfiable
News
In 2005, according to weblog statistics, this webpage was visited 3938 times (by people from 36 countries) and the above SAT benchmarks were downloaded 655 times. Most visitors were from USA, China, France, Canada, UK, Germany, Australia, Italy, Israel and India (about 1/4 of them came through Google).
Some of the SAT benchmarks above were used for SAT Competition 2004 (55 solvers). The results are summarized as follows (the timeout is 10 minutes):
frb40191.cnf: solved by 28 solvers. frb40192.cnf: solved by 27 solvers.
frb45211.cnf: solved by 8 solvers. frb45212.cnf: solved by 5 solvers.
frb50231.cnf: solved by 1 solver. frb50232.cnf: solved by 1 solver.
frb53241.cnf: unsolved. frb53242.cnf: unsolved.
frb56251.cnf: unsolved. frb56252.cnf: unsolved.
frb59261.cnf: unsolved. frb59262.cnf: unsolved.
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 wellstudied 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/(ln4ln3)=2.7808, then as the number of variables increases, we can get the following tuples of values for Model RB (Note: If noninteger 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=1eα/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 withn 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 treelike resolution proofs of less than exponential size, which means that RB is hard for all CSP algorithms based on treelike resolutions. Another point worth mentioning is that the exact phase transitions of Model RB are established by nonalgorithmic 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 3SAT 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 nontrivial 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 to50% 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 3SAT 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. frb40191.csp and frb40191.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.
frb3015csp.tar.gz ( 130 KB): #variables=30, #values=15, #constraints=284, #nogoods= 56
frb3517csp.tar.gz ( 210 KB): #variables=35, #values=17, #constraints=346, #nogoods= 72
frb4019csp.tar.gz ( 320 KB): #variables=40, #values=19, #constraints=410, #nogoods= 90
frb4521csp.tar.gz ( 465 KB): #variables=45, #values=21, #constraints=476, #nogoods=110
frb5023csp.tar.gz ( 653 KB): #variables=50, #values=23, #constraints=544, #nogoods=132
frb5324csp.tar.gz ( 772 KB): #variables=53, #values=24, #constraints=585, #nogoods=144
frb5625csp.tar.gz ( 902 KB): #variables=56, #values=25, #constraints=627, #nogoods=156
frb5926csp.tar.gz (1051 KB): #variables=59, #values=26, #constraints=669, #nogoods=169
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 followthis link.
News

frb30151.csp 
frb30152.csp 
frb30153.csp 
frb30154.csp 
frb30155.csp 
Solved by 
16solvers 
15solvers 
16 solvers 
16solvers 
16solvers 

frb35171.csp 
frb35172.csp 
frb35173.csp 
frb35174.csp 
frb35175.csp 
Solved by 
13solvers 
13solvers 
15 solvers 
16solvers 
12solvers 

frb40191.csp 
frb40192.csp 
frb40193.csp 
frb40194.csp 
frb40195.csp 
Solved by 
9solvers 
8solvers 
7solvers 
8solvers 
8solvers 

frb45211.csp 
frb45212.csp 
frb45213.csp 
frb45214.csp 
frb45215.csp 
Solved by 
1solvers 
3solvers 
3solvers 
4solvers 
5solvers 

frb50231.csp 
frb50232.csp 
frb50233.csp 
frb50234.csp 
frb50235.csp 
Solved by 
0 solvers 
0 solvers 
0 solvers 
4solvers 
0 solvers 

frb53241.csp 
frb53242.csp 
frb53243.csp 
frb53244.csp 
frb53245.csp 
Solved by 
0 solvers 
0 solvers 
0 solvers 
0 solvers 
0 solvers 

frb56251.csp 
frb56252.csp 
frb56253.csp 
frb56254.csp 
frb56255.csp 
Solved by 
0 solvers 
0 solvers 
0 solvers 
0 solvers 
0 solvers 

frb59261.csp 
frb59262.csp 
frb59263.csp 
frb59264.csp 
frb59265.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 forGraph Problems
PseudoBoolean (01 Integer Programming) Benchmarks with Hidden Optimum Solutions
Benchmarks with Hidden Optimum Solutions for Set Covering, Set Packing and Winner Determination
Weighted Max2SAT Benchmarks with Hidden Optimum Solutions (New!)
References
K. Xu and W. Li. Exact Phase Transitions in Random Constraint Satisfaction Problems. Journal of Artificial Intelligence Research, 12(2000):93103.
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):291302.
K. Xu, F. Boussemart, F. Hemery and C. Lecoutre. Random Constraint Satisfaction: Easy Generation of Hard (Satisfiable) Instances. Artificial Intelligence, 171(2007):514534.Earlier version entitled "A Simple Model to Generate Hard Satisfiable Instances" appeared in Proc. of 19th IJCAI, pp.337342, Scotland, 2005.
Related Links
Fadi Aloul's SAT Benchmarks.
Back to KeXu's homepage.
Date Created: Oct. 23, 2003. Last Updated: June 5, 2007.