Welcome to CNFgen’s documentation!

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

The cnfformula library

The cnfformula 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 cnfformula.CNF object. Let’s see a simple example of its usage.

>>> import cnfformula
>>> F = cnfformula.CNF()
>>> F.add_clause([(True,"X"),(False,"Y")])
>>> F.add_clause([(False,"X")])
>>> F.is_satisfiable()
(True, {'Y':False, 'X':False})
>>> F.add_clause([(True,"Y")])
>>> F.is_satisfiable()
(False, None)
>>> print F.dimacs()
c Generated with `cnfgen` (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>
c https://github.com/MassimoLauria/cnfgen.git
c
p cnf 2 3
1 -2 0
-1 0
2 0
>>> print F.latex()
% Generated with `cnfgen` (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>
% https://github.com/MassimoLauria/cnfgen.git
%
\begin{align}
&       \left(     {X} \lor \neg{Y} \right) \\
& \land \left( \neg{X} \right) \\
& \land \left(     {Y} \right)
\end{align}

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

>>> from cnfformula import PigeonholePrinciple
>>> F = PigeonholePrinciple(5,4)
>>> print F.dimacs()
c Pigeonhole principle formula for 5 pigeons and 4 holes
c Generated with `cnfgen` (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>
c https://github.com/MassimoLauria/cnfgen.git
c
p cnf 20 45
1 2 3 4 0
5 6 7 8 0
...
-16 -20 0
>>> F.is_satisfiable()
(False, None)

The cnfgen command line tool

The command line tool is installed along cnfformula 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 Pigeonhole principle formula for 5 pigeons and 4 holes
c Generated with `cnfgen` (C) Massimo Lauria <lauria.massimo@gmail.com>
c https://github.com/MassimoLauria/cnfgen.git
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