Skip to main content

Manipulate NNF (Negation Normal Form) logical sentences

Project description

Build Status Readthedocs Python Versions PyPI License

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})
>>> sentence.satisfied_by({'a': False, 'b': 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()

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

Complete documentation can be found at readthedocs.


At least Python 3.4 is required.


Install with support for a variety of SAT solvers.

pip install nnf[pysat]


pip install nnf


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.


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.

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for nnf, version 0.3.0
Filename, size File type Python version Upload date Hashes
Filename, size nnf-0.3.0-py3-none-any.whl (598.7 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size nnf-0.3.0.tar.gz (594.1 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page