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})
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.

Project details


Download files

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

Source Distribution

nnf-0.3.0.tar.gz (594.1 kB view hashes)

Uploaded source

Built Distribution

nnf-0.3.0-py3-none-any.whl (598.7 kB view hashes)

Uploaded py3

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page