# 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.is_satisfiable()
(True, {'Y':False, 'X':False})
>>> 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.