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
.