Metadata-Version: 2.1
Name: nnf
Version: 0.0.2
Summary: Manipulate NNF (Negation Normal Form) logical sentences
Home-page: https://github.com/blyxxyz/python-nnf
Author: Jan Verbeek
Author-email: jan.verbeek@posteo.nl
License: ISC
Platform: UNKNOWN
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Development Status :: 2 - Pre-Alpha
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: License :: OSI Approved :: ISC License (ISCL)
Description-Content-Type: text/markdown

[![Build Status](https://travis-ci.org/blyxxyz/python-nnf.svg?branch=master)](https://travis-ci.org/blyxxyz/python-nnf)

`nnf` is a Python package for creating and manipulating logical sentences
written in the
[negation normal form](https://en.wikipedia.org/wiki/Negation_normal_form)
(NNF).

NNF sentences make statements about any number of variables. Here's an example:

```pycon
>>> 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:

```pycon
>>> 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:

```pycon
>>> sentence.condition({'b': True})
Or({And({a, true}), And({a, false})})
```

And then reduce the sentence:

```pycon
>>> _.simplify()
a
```

This package takes much of its data model and terminology from
[*A Knowledge Compilation Map*](https://jair.org/index.php/jair/article/view/10311).

# Installing

```sh
pip install nnf
```

Only Python 3.7 or higher is currently supported.

# Serialization

A parser and serializer for the
[DIMACS sat format](https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html) 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](https://arxiv.org/abs/1211.4475).


