Welcome to CNFgen’s documentation!

The main components of CNFgen are the cnfgen library and the cnfgen command line utility.

The cnfgen library

The cnfgen library is capable to generate Conjunctive Normal Form (CNF) formulas, manipulate them and, when there is a satisfiability (SAT) solver properly installed on your system, test their satisfiability. The CNFs can be saved on file in DIMACS format, which the standard input format for SAT solvers [1], or converted to LaTeX [2] to be included in a document. The library contains many generators for formulas that encode various combinatorial problems or that come from research in Proof Complexity [3].

The main entry point for the library is the cnfgen.CNF object. Let’s see a simple example of its usage.

>>> from pprint import pprint
>>> import cnfgen
>>> F = cnfgen.CNF()
>>> F.add_clause([1,-2])
>>> F.add_clause([-1])
>>> outcome,assignment = F.solve() # outputs a pair
>>> outcome                        # is the formula SAT?
True
>>> pprint(assignment)             # a solution
[-1, -2]
>>> F.add_clause([2])
>>> F.solve()             # no solution
(False, None)
>>> print(F.to_dimacs())
p cnf 2 3
1 -2 0
-1 0
2 0
<BLANKLINE>
>>> print(F.to_latex())
\begin{align}
&       \left(            {x_1} \lor {\overline{x}_2} \right) \\
& \land \left( {\overline{x}_1} \right) \\
& \land \left(            {x_2} \right)
\end{align}

A typical unsatisfiable formula studied in Proof Complexity is the pigeonhole principle formula.

>>> from cnfgen import PigeonholePrinciple
>>> F = PigeonholePrinciple(5,4)
>>> print(F.to_dimacs())
p cnf 20 45
1 2 3 4 0
5 6 7 8 0
...
-16 -20 0
<BLANKLINE>
>>> F.is_satisfiable()
False

The cnfgen command line tool

The command line tool is installed along cnfgen package, and provides a somehow limited interface to the library capabilities. It provides ways to produce formulas in DIMACS and LaTeX format from the command line. To produce a pigeonhole principle from 5 pigeons to 4 holes as in the previous example the command line is

$ cnfgen php 5 4
c description: Pigeonhole principle formula for 5 pigeons and 4 holes
c generator: CNFgen (0.8.5.post1-7-g4e234b7)
c copyright: (C) 2012-2020 Massimo Lauria <massimo.lauria@uniroma1.it>
c url: https://massimolauria.net/cnfgen
c command line: cnfgen php 5 4
c
p cnf 20 45
1 2 3 4 0
5 6 7 8 0
...
-16 -20 0

For a documentation on how to use cnfgen command please type cnfgen  --help and for further documentation about a specific formula generator type cnfgen <generator_name> --help.

Indices and tables