If you have any comments or need more instances for the following Max-2-SAT benchmarks, please send me an email.
The Maximum Satisfiability Problem (Max-SAT), an optimization version of SAT, is the problem of finding an assignment that maximizes the number of satisfied clauses. Max-SAT is NP-hard even if every clause contains at most two literals (called the Max-2-SAT problem). Weighted Max-SAT is a generalization of Max-SAT in which every clause has a weight and the goal is to find an optimum assignment maximizing the total weight of satisfied clauses. Finding challenging benchmarks for the (weighted) Max-SAT problem is not only of significance for the experimental evaluation of (weighted) Max-SAT algorithms but also of interest to the theoretical computer science community. The weighted Max-2-SAT benchmarks presented here are transformed from forced satisfiable SAT benchmarks of Model RB. In fact, based on Model RB and this transformation, we can propose a simple model for generating random weighted Max-2-SAT instances as follows (Thanks to Chu-Min Li for discussions):
First generate n disjoint sets of boolean variables, each of which has cardinality nα (where α>0 is a constant), and then for every variable x, generate a unit clause x, and for every two variables x and y in the same set, generate a 2-clause ¬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 rnlnn-1 times (where r>0 is a constant);
For every unit clause, we have a weight equal to 1, and for every 2-cluase, we have a weight equal to i (where i = the total number of unit clauses + 1).
The goal is to maximize the total weight of satisfied clauses. For the random Max-2-SAT model above, since the weight of every 2-clause is greater than the total weight of unit clauses, it is not hard to see that for any optimum assignment, every 2-clause must be satisfied and in such a case, at most n unit clauses can be satisfied (one from each disjoint set). Therefore, the maximum value of the total weight of satisfied clauses is at most n+i*m where m is the number of 2-clauses. Interestingly, determining if such a upper bound can be reached is equivalent to determining the satisfiability of the corresponding CSP and SAT instances of Model RB, and there is a one-to-one mapping between the solutions of these two problems. To hide an optimum assignment in the instances of the Max-2-SAT model above, we first select a boolean 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 optimum assignment. From the results of the paper "Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances", it is expected that Model RB can also be used to generate hard instances for Max-SAT algorithms (by use of the above Max-2-SAT model and the hardness of phase transitions, i.e. choosing appropriate values of a, p and r). Recently, it has been shown (both experimentally and theoretically) that unlike random 3-SAT, it is quite natural and easy to hide solutions in random CSP and SAT instances of Model RB. For more details, please see an IJCAI-05 paper entitled "A Simple Model to Generate Hard Satisfiable Instances".
Note: The following weighted Max-2-SAT benchmarks are expressed in the DIMACS format and the optimum value is given in the first line of each file.
Remark: The feedback from several researchers indicates that the above benchmarks might be too hard for current solvers. So, in what follows, we added some benchmark sets of smaller size. (New!)
List of Papers That Use MAX-SAT Benchmarks Based on Model RB (Updated: Mar. 4, 2009)
Other Benchmarks Based on Model RB
Forced Satisfiable CSP and SAT Benchmarks of 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
Back to Ke Xu's homepage.
Date Created: Aug. 27, 2006. Last Updated: Mar. 4, 2007.