Approach 1:
Random Generation of Unique Solution 3SAT Instances

1. Introduction to Approach 1
2. Algorithms
3. Sample SAT Instances
4. MAX-SAT Instances

1. SAT Instance Generation: Main Page
2. Approach 2: Hard Instance Generation Based on Factoring

This page is created by M.Motoki and O.Watanabe. For question and/or comment of this page, please contact mmotoki@is.titech.ac.jp.

1. Introduction to Approach 1

One can easily think of the following algorithm to generate positive instances:

1. Generate one solution t for n Boolean variables randomly.
2. Generate m clauses that are consistent with t.

Our first approach is to use this simple algorithm. We modify it to get a better generation algorithm.

Intuitively, the more clauses a formula has, the less number of assignments satisfy the formula. In fact, for the above simple algorithm, we can show that the algorithm outputs a unique solution formula with high probability if m > 7n/3 ln n + O(n). Furthermore, we can also show that m > 7n/3 ln n is necessary for the algorithm to yield a unique solution formula with high probability.

On the other hand, an interesting m and n ratio is about 4.2 in the case of 3SAT because m = 4.2n is the cross over point and it has been believed that a formula with this or closer ratio is difficult. Thus, we modify the above algorithm so that it yields a unique solution formula with high probability with much smaller m and n ratio. We can prove that our new algorithm outputs unique solution formula with probability, say half, when m > 4.3n. (See our paper in References and Links for further explanation.)

2. Algorithms

2.1 Algorithm G2

We call our unique solution instance generator G2.c. The program are called as

G2 [n] [m] > [outfile]

where [n] is the number of variables, [m] is the number of clauses, and [outfile] is output filename.

Caution: We use rand() as random generator because it is ANSI function. Hence, we recommend that you use other random generator if your rand() is not good. For example, many UNIX systems have random() instead of rand(). We also recommend Mersenne Twister.

The probability that G2.c generates a unique solution instance depends on the number of clauses m. Theoretically, we can give an upper bound on m. That is, we showed that our algorithm outputs a unique solution instance with high probability if m > ?n/? + o(n). We also have some experimental results. What follows is summary of our experiment for the case n = 100. It shows that the probability of getting a unique solution instance is fairly high when n = 100 and m = 500.

2.2 Algorithm G3

3. Sample Instances

In what follows we give some set of instances generated by using our generator.

algorithm	num. of variables	num. of clauses	file of sample
G2	50	275	G2-50-275-1.txt
			G2-50-275-2.txt
			G2-50-275-3.txt
			G2-50-275-4.txt
			G2-50-275-5.txt
		300	G2-50-300-1.txt
			G2-50-300-2.txt
			G2-50-300-3.txt
			G2-50-300-4.txt
			G2-50-300-5.txt
	100	550	G2-100-550-1.txt
			G2-100-550-2.txt
			G2-100-550-3.txt
			G2-100-550-4.txt
			G2-100-550-5.txt
		600	G2-100-600-1.txt
			G2-100-600-2.txt
			G2-100-600-3.txt
			G2-100-600-4.txt
			G2-100-600-5.txt
G3	50	230	G3-50-230-1.txt
			G3-50-230-2.txt
			G3-50-230-3.txt
			G3-50-230-4.txt
			G3-50-230-5.txt
		250	G3-50-250-1.txt
			G3-50-250-2.txt
			G3-50-250-3.txt
			G3-50-250-4.txt
			G3-50-250-5.txt
	100	460	G3-100-460-1.txt
			G3-100-460-2.txt
			G3-100-460-3.txt
			G3-100-460-4.txt
			G3-100-460-5.txt
		500	G3-100-500-1.txt
			G3-100-500-2.txt
			G3-100-500-3.txt
			G3-100-500-4.txt
			G3-100-500-5.txt

4. Random MAX-3SAT Instances

Here we give a program called maxG3.c that generates MAX-3SAT instance based on G3. The program are called as

maxG3 [n] [m] [k] > [outfile]

where [n] is the number of variables, [k] is minimum number of unsatisfiable clauses and [m] means the number of clauses per [k]. Thus total number of clauses is [k]×[m].

Here we give some sets of instances obtained following this idea.