nnf 0.1.2

Manipulate NNF (Negation Normal Form) logical sentences

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

pip install nnf

At least Python 3.4 is required.

Serialization

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

Algebraic Model Counting

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