Generator of benchmarks for the satisfiability problem (sgen)

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