Manipulate NNF (Negation Normal Form) logical sentences
Project description
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.5 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.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.