Randomly generated instances - constant density model

Random instances of the constant density model are generated in the following way: For an instance with n variables and k clauses, clauses are generated by including a variable with a fixed probability p, and then negating the variable with probability 0.5. Because formulas generated in this way may contain empty clauses or unit clauses. Hence, empty clauses and unit clauses are rejected in the generation process. The resulting problem distribution is called Random P-SAT in [SML96].

It should be noted here that empirical as well as theoretical results indicate that instances generated by this model tend to be much easier than Uniform Random-3-SAT instances and therefore the latter appear to be much better suited for a set of hard benchmark instances. We refer to [SML96] and [ML96] for a more detailed discussion.

Benchmark instances

There is a total of 50 benchmark instances of this class of different sizes in this class; there are 40 instances with 100 variables and 800 clauses, the other 10 instances have 100 variables and 900 clauses.

Of the 50 instances 16 instances are satisfiable, all others are unsatisfiable. The satisfiable instances are the following:

jnh201.cnf, jnh204.cnf, jnh205.cnf, jnh207.cnf, jnh209.cnf, jnh210.cnf, jnh212.cnf, jnh213.cnf, jnh217.cnf, jnh218.cnf, jnh220.cnf, jnh301.cnf, jnh212.cnf

All other instances are unsatisfiable.

Acknowledgements

The instances have originally been contributed by John Hooker and are also contained in a collection of SAT instances at the Forschungsinstitut für anwendungsorientierte Wissensverarbeitung in Ulm, Germany.

[SML96]	B. Selman, D.G. Mitchell, and H.J. Levesque. Generating Hard Satisfiability Instances. Artificial Intelligence, Vol. 81, pages 17-29, 1996.
[SML96]	D.G. Mitchell, and H.J. Levesque. Some Pitfalls for Experiments with Random SAT. Artificial Intelligence, Vol. 81, pages 111-125, 1996.