Command line interface¶
Some of python-nnf
’s functionality is exposed through a command line tool. It can be invoked as pynnf
or python3 -m nnf
.
SAT solving¶
pynnf sat
tests whether a sentence is satisfiable, while pynnf sharpsat
counts how many solutions it has.
Add -v
to get extra information about the sentence and the running time.
Example:
$ pynnf sat uf20-01.cnf
SATISFIABLE
Beware that it’s much slower than dedicated solvers like MiniSat.
Sentence summary¶
pynnf info
shows basic information about a sentence.
Examples:
$ pynnf info uf20-01.cnf
Sentence is in CNF.
Variables: 20
Size: 360
Clauses: 90
Clause size: 3
$ pynnf info uf100-016.cnf.nnf
Sentence is decomposable.
Variables: 97
Size: 109
Visualizing sentences¶
pynnf draw
converts sentences to a DOT representation, and either outputs that or feeds it to dot
to immediately output an image.
Immediately outputting an image requires having dot
installed. It’s done when the output file has an image extension, or when a format is passed with the -f
flag.
Examples:
$ pynnf draw uf20-01.nnf out.png # Create a PNG image
$ pynnf draw uf20-01.nnf out.gv # Create a DOT representation
$ pynnf draw uf20-01.nnf out.pdf # Create a PDF vector image
$ pynnf draw -f png uf20-01.nnf - | convert -flip - out.png # Output a PNG image to be processed by imagemagick
See pynnf draw --help
for more information.