Welcome to python-nnf’s documentation!

python-nnf is a package for working with logical sentences written in the negation normal form.


Sentences are made up of nodes. To start with, define some variables:

>>> from nnf import Var
>>> A, B, C = Var('A'), Var('B'), Var('C')

Then, if you want to write the sentence “A or B”:

>>> from nnf import Or
>>> sentence = Or({A, B})
>>> sentence = A | B  # alternative syntax

Or “B and not C”:

>>> from nnf import And
>>> sentence = And({B, ~C})
>>> sentence = B & ~C

Of course you can nest these, for more interesting sentences:

>>> sentence = Or({And({A, B}), And({~B, C})})

You can ask queries, and perform transformations:

>>> sentence.decomposable()
>>> sentence.smooth()
>>> list(sentence.models())
[{'A': True, 'B': True, 'C': True}, {'A': True, 'B': False, ...
>>> new = sentence.condition({'B': True})
>>> new
Or({And({A, true}), And({false, C})})
>>> list(new.models())
[{'A': True, 'C': True}, {'A': True, 'C': False}]
>>> new.simplify()

Indices and tables