# 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`

.