Forced Satisfiable CSP and SAT Benchmarks of Model RB------Hiding Solutions with Growing DomainsIf you have any comments or need more instances for the following CSP and SAT benchmarks, please send me an email.

作者: 时间:2017-11-30 点击数:

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 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 &not;x&or;&not;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-1times (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.

  •  frb30-15-cnf.tar.gz (   254 KB):   450 Boolean  variables,   19084  clauses - 5 instances, all satisfiable 

  •  frb35-17-cnf.tar.gz (   398 KB):   595 Boolean  variables,   29707  clauses - 5 instances, all satisfiable 

  •  frb40-19-cnf.tar.gz (  589 KB):   760  Boolean variables,    43780 clauses - 5 instances, all satisfiable 

  •  frb45-21-cnf.tar.gz (   848 KB):   945 Boolean variables,    61855 clauses - 5 instances, all satisfiable 

  •  frb50-23-cnf.tar.gz (1151 KB): 1150  Boolean variables,   84508 clauses - 5  instances, all satisfiable 

  •  frb53-24-cnf.tar.gz (1370 KB): 1272  Boolean variables,    98921 clauses - 5  instances, all satisfiable 

  •  frb56-25-cnf.tar.gz (1589 KB): 1400  Boolean variables, 114668 clauses - 5  instances, all satisfiable 

  •  frb59-26-cnf.tar.gz (1824 KB): 1534  Boolean variables, 132295 clauses - 5 instances,  all satisfiable 



  • 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):

  • frb40-19-1.cnf: solved by 28 solvers.         frb40-19-2.cnf: solved by 27 solvers.  

  • frb45-21-1.cnf: solved by   8  solvers.        frb45-21-2.cnf: solved by      5 solvers.

  • frb50-23-1.cnf: solved by  1  solver.       frb50-23-2.cnf: solved by   1 solver.  

  • frb53-24-1.cnf: unsolved.                         frb53-24-2.cnf: unsolved.

  • frb56-25-1.cnf: unsolved.                         frb56-25-2.cnf: unsolved.

  • frb59-26-1.cnf: unsolved.                         frb59-26-2.cnf: unsolved.  

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 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 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 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 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&egrave;re, R. Dechter and J.C. R&eacute;gin) and are expressed in the same format as theirs.    

  •  frb30-15-csp.tar.gz  (  130 KB): #variables=30,  #values=15,  #constraints=284,  #nogoods=   56 

  •  frb35-17-csp.tar.gz  (  210 KB): #variables=35,  #values=17,  #constraints=346,  #nogoods=   72 

  •  frb40-19-csp.tar.gz  (  320 KB): #variables=40,  #values=19,  #constraints=410,  #nogoods=   90 

  •  frb45-21-csp.tar.gz  (  465 KB): #variables=45,  #values=21,  #constraints=476,  #nogoods=110 

  •  frb50-23-csp.tar.gz  (  653 KB): #variables=50,  #values=23,  #constraints=544,  #nogoods=132 

  •  frb53-24-csp.tar.gz  (  772 KB): #variables=53,  #values=24,  #constraints=585,  #nogoods=144 

  •  frb56-25-csp.tar.gz  (  902 KB): #variables=56,  #values=25,  #constraints=627,  #nogoods=156 

  •  frb59-26-csp.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.


   frb30-15-1.csp    frb30-15-2.csp    frb30-15-3.csp    frb30-15-4.csp    frb30-15-5.csp
   Solved by    16solvers    15solvers    16 solvers    16solvers    16solvers
   frb35-17-1.csp    frb35-17-2.csp    frb35-17-3.csp    frb35-17-4.csp    frb35-17-5.csp
   Solved by    13solvers    13solvers    15 solvers    16solvers    12solvers
   frb40-19-1.csp    frb40-19-2.csp    frb40-19-3.csp    frb40-19-4.csp    frb40-19-5.csp
   Solved by    9solvers    8solvers    7solvers    8solvers    8solvers
   frb45-21-1.csp    frb45-21-2.csp    frb45-21-3.csp    frb45-21-4.csp    frb45-21-5.csp
   Solved by    1solvers    3solvers    3solvers    4solvers    5solvers
   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    4solvers    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 forGraph 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!)


  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 KeXu's homepage.

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

软件开发环境国家重点实验室 地址:北京市海淀区学院路37号北京航空航天大学新主楼G座
邮编:100191 联系电话:010-82338092 邮箱