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.