nnf

nnf is a Python package for creating and manipulating logical sentences written in the negation normal form (NNF).

NNF sentences make statements about any number of variables. Here's an example:

>>> from nnf import Var
>>> a, b = Var('a'), Var('b')
>>> sentence = (a & b) | (a & ~b)
>>> sentence
Or({And({a, b}), And({a, ~b})})

This sentence says that either a is true and b is true, or a is true and b is false.

You can do a number of things with such a sentence. For example, you can ask whether a particular set of values for the variables makes the sentence true:

>>> sentence.satisfied_by({'a': True, 'b': False})
True
>>> sentence.satisfied_by({'a': False, 'b': False})
False

You can also fill in a value for some of the variables:

>>> sentence.condition({'b': True})
Or({And({a, true}), And({a, false})})

And then reduce the sentence:

>>> _.simplify()
a

This package takes much of its data model and terminology from A Knowledge Compilation Map.

Complete documentation can be found at readthedocs.

Installing

At least Python 3.4 is required.

Recommended

Install with support for a variety of SAT solvers.

pip install nnf[pysat]

Vanilla

pip install nnf

Serialization

A parser and serializer for the DIMACS sat format are implemented in nnf.dimacs, with a standard load/loads/dump/dumps interface.

DSHARP interoperability

DSHARP is a program that compiles CNF sentences to (s)d-DNNF sentences. The nnf.dsharp module contains tools for parsing its output format and for invoking the compiler.

Algebraic Model Counting

nnf.amc has a basic implementation of Algebraic Model Counting.

Command line interface

Some functionality is available through a command line tool, pynnf, including a (slow) SAT solver and a sentence visualizer. For more information, see the documentation.

Credits

python-nnf up to version 0.2.1 was created by Jan Verbeek under mentorship of Ronald de Haan at the University of Amsterdam. It was the subject of an undergraduate thesis, Developing a Python Package for Reasoning with NNF Sentences.