[Note: Instances are in the sat/benchmarks/cnf directory]

This directory contains several formulas for the DIMACS benchmark.

3 random satisfiable instances: f600.cnf, f1000.cnf, and f2000.cnf

2 Boolean encodings of planning problems: hanoi4.cnf and hanoi5.cnf
  The instances are created by instantiating a set of axioms describing 
  the 4-block and 5-block towers of Hanoi puzzle. Both are satisfiable.
  hanoi4.cnf is fairly difficult, requiring several hours to solve using 
  the best algorithms we have tried (as of 7/6/93). We have not yet found 
  an algorithm that can solve hanoi5.cnf.

4 Boolean encodings of hard graph coloring problems: g125.18.cnf, g125.17.cnf
  g250.15.cnf, and g250.29.cnf. Each instance is satisfiable. (g125.18.cnf and
  g250.15.cnf are the easier ones.)

For further information on these instances and related instances contact
  Bart Selman (selman@research.att.com) or Henry Kautz (kautz@research.att.com).