The sgen generator was developed to generate small, difficult benchmarks for the satisfiability problem. Specifically, it was written to be be entered in the annual SAT Competition and satisfies the input requirements of that competition. The most recent version is known as sgen1 and the source code is here. On unix systems it can be compiled by: gcc -o sgen1 sgen1.c -lm
A description of the generator is available here.
Some generated benchmarks are available in the files sgen1-unsat.tar
and sgen1-sat.tar.
The file sgen1-unsat.tar includes the benchmark sgen1-unsat-121-100.cnf
which was the smallest (with 756 literals) benchmark which was not solved during the
SAT Competition 2009.
The author can be contacted at i.spence@qub.ac.uk.