SATLIB - Benchmark Problems

All instances provided here are cnf formulae encoded in DIMACS cnf format. This format is supported by most of the solvers provided in the SATLIB Solvers Collection. For a description of the DIMACS cnf format, see DIMACS Challenge - Satisfiability: Suggested Format (ps file, 108k) (taken from the DIMACS FTP site).

Please help us to extend our benchmark set by submitting new benchmark instances or suggesting existing benchmarks we should include. We are especially interested in SAT-encoded problems from other domains, for example, encodings of problems available from CSPLIB.

At the moment, we provide mainly satisfiable instances, as many popular SAT algorithms are incomplete. However, we will extend our collection of unsatisfiable benchmark instances in the near future, to further facilitate comparative studies of complete algorithms.

© hh, last update 00/08/11.