• cnfgen generator for CNF formula benchmarks,
• several formula families (a list here)
• several formula transformations (a list here)
• output in DIMACS and LaTeX formats,
• behind-the-scene integration with many SAT solvers,
• the cnfgen python library (read the docs) for more flexible CNF generation and manipulation,
• CNF based on graph structures (see the supported graph formats).

You can install CNFgen from Python Package Index, together with all its dependencies, typing either

pip3 install [--user] cnfgen

or

python3 -m pip install  [--user] cnfgen

if pip3 is not a program on your path. Otherwise it is possible to install from source, assuming the requirements are already installed, using

python3 setup.py install [--user]

The --user option allows to install the package in the user home directory. If you do that please check that the target location for the command line utilities are in your $PATH.

In most cases it is sufficient to invoke cnfgen giving the name of the formula family and the corresponding parameters.

cnfgen <formula> <param1> <param2> ...

For example

cnfgen php 10 7

gives the Pigeonhole Principle from 10 pigeons and 7 holes. To get more help you can type

cnfgen --help                # available formulas / help for the tool
cnfgen <formula> --help      # help about a specific formula
cnfgen --tutorial            # a quick tutorial 

Here's how to generate a formula encoding the Graph ordering principle on a random regular graph with 10 vertices and degree 3.

cnfgen op 10 3

or a formula claiming the 3-colorability formula of a 15 by 15 grid graph.

cnfgen kcolor 3 grid 15 15

In the next example we generate the formula that claims the graph isomorphism between (1) the bidimensional torus of 3x1 and (2) the complete graph over three vertices. This formula is clearly satisfiable.

cnfgen iso torus 3 1 -e complete 3

Some formulas require input graph(s), and the cnfgen tool supports several graph file formats. For example

cnfgen kclique 5 largegraph.gml

encodes in DIMACS the problem of searching a clique of size 5 in the graph encoded in file largegraph.gml. In general there are various formulas generator that need either a simple graph, a directed acyclic graph, or a bipartite graph specified on the command line. See

cnfgen --help-graph
cnfgen --help-dag
cnfgen --help-bipartite

CNFgen can apply one or more transformations to the formula by appending one or more transformation descriptions to the command line. For example

cnfgen op 15 -T shuffle

produces the ordering principle formula on 15 elements, with a random shuffle of variables, polarities and clauses. Or for example

cnfgen php 5 4 -T xor 2 

substitute all variables in the pigeohole principle formula with the XOR of 2 fresh variable.

cnfgen --help

For more information check out transformations.

The CNFgen project is by Massimo Lauria (massimo.lauria@uniroma1.it), with helps and contributions by Marc Vinyals, Jan Elffers, Mladen Mikša and Jakob Nordström. Special thanks to Adam Lugowski who helped updateing the codebase to work on Python 3 and NetworkX 2.

A large part of the initial work has been funded by

• [2016-2017] The European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement ERC-2014-CoG 648276 AUTAR)
• [2012-2015] The European Research Council under the European Union's Seventh Framework Programme (FP7/2007–2013) ERC grant agreement no. 279611.