We present CNFgen, a generator of CNF formulas in Dimacs format.

There are many examples of combinatorial formulas in the proof complexity literature which are "extremal" in different ways and which are therefore of potential interest in the experimental analysis of SAT solver, but most of these formulas appear not to be well known in the SAT community.

These are not just those formulas that are hard for SAT, also also easy formulas with peculiar properties that highlight the issue with the current proof search techniques, withing resolution and beyond.

CNFgen is intended to serve as a standard resource for crafted formulas, making them readily available for SAT evaluation purposes.

Furthermore, the package includes a python library giving access to the functionality of CNFgen to Python programs.