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