CNFgen

CNFgen is produces combinatorial benchmarks in DIMACS format, ready to be fed to SAT solvers. These benchmarks come mostly from research in Proof Complexity (e.g. pigeonhole principle, ordering principle, k-clique, …). Many of these formulas encode structured combinatorial problems well known to be challenging for certain SAT solvers.