[](https://travis-ci.org/qumulab/python-nnf)
[](https://python-nnf.readthedocs.io)
[](https://pypi.org/project/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).
Complete documentation can be found at [readthedocs](https://python-nnf.readthedocs.io).
# Installing
At least Python 3.4 is required.
## Recommended
Install with support for a variety of SAT solvers.
```sh
pip install nnf[pysat]
```
## Vanilla
```sh
pip install nnf
```
# 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.
# DSHARP interoperability
[DSHARP](https://github.com/QuMuLab/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](https://arxiv.org/abs/1211.4475).
# 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](https://python-nnf.readthedocs.io/en/stable/cli.html).
# Credits
`python-nnf` up to version 0.2.1 was created by [Jan Verbeek](https://github.com/blyxxyz)
under mentorship of [Ronald de Haan](https://staff.science.uva.nl/r.dehaan/)
at the [University of Amsterdam](https://www.uva.nl/). It was the subject of an
undergraduate thesis, [*Developing a Python Package for Reasoning with NNF Sentences*](https://scripties.uba.uva.nl/scriptie/691650).
Raw data
{
"_id": null,
"home_page": "https://github.com/QuMuLab/python-nnf",
"name": "nnf",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.4",
"maintainer_email": "",
"keywords": "logic nnf dimacs dsharp",
"author": "Jan Verbeek, Christian Muise",
"author_email": "jan.verbeek@posteo.nl, christian.muise@queensu.ca",
"download_url": "https://files.pythonhosted.org/packages/82/16/12221f3c9d21340ca8378df5c047545e3e01ffb088b5177620e5bc8dd128/nnf-0.4.1.tar.gz",
"platform": null,
"description": "[](https://travis-ci.org/qumulab/python-nnf)\n[](https://python-nnf.readthedocs.io)\n\n[](https://pypi.org/project/nnf/)\n\n\n`nnf` is a Python package for creating and manipulating logical sentences\nwritten in the\n[negation normal form](https://en.wikipedia.org/wiki/Negation_normal_form)\n(NNF).\n\nNNF sentences make statements about any number of variables. Here's an example:\n\n```pycon\n>>> from nnf import Var\n>>> a, b = Var('a'), Var('b')\n>>> sentence = (a & b) | (a & ~b)\n>>> sentence\nOr({And({a, b}), And({a, ~b})})\n```\n\nThis sentence says that either a is true and b is true, or a is true and b\nis false.\n\nYou can do a number of things with such a sentence. For example, you can ask\n whether a particular set of values for the variables makes the sentence true:\n\n```pycon\n>>> sentence.satisfied_by({'a': True, 'b': False})\nTrue\n>>> sentence.satisfied_by({'a': False, 'b': False})\nFalse\n```\n\nYou can also fill in a value for some of the variables:\n\n```pycon\n>>> sentence.condition({'b': True})\nOr({And({a, true}), And({a, false})})\n```\n\nAnd then reduce the sentence:\n\n```pycon\n>>> _.simplify()\na\n```\n\nThis package takes much of its data model and terminology from\n[*A Knowledge Compilation Map*](https://jair.org/index.php/jair/article/view/10311).\n\nComplete documentation can be found at [readthedocs](https://python-nnf.readthedocs.io).\n\n# Installing\n\nAt least Python 3.4 is required.\n\n## Recommended\n\nInstall with support for a variety of SAT solvers.\n\n```sh\npip install nnf[pysat]\n```\n\n## Vanilla\n\n```sh\npip install nnf\n```\n\n# Serialization\n\nA parser and serializer for the\n[DIMACS sat format](https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html) are\nimplemented in `nnf.dimacs`, with a standard `load`/`loads`/`dump`/`dumps`\ninterface.\n\n# DSHARP interoperability\n\n[DSHARP](https://github.com/QuMuLab/dsharp) is a program that compiles CNF\nsentences to (s)d-DNNF sentences. The `nnf.dsharp` module contains tools for\nparsing its output format and for invoking the compiler.\n\n# Algebraic Model Counting\n\n`nnf.amc` has a basic implementation of\n[Algebraic Model Counting](https://arxiv.org/abs/1211.4475).\n\n# Command line interface\n\nSome functionality is available through a command line tool, `pynnf`, including a\n(slow) SAT solver and a sentence visualizer. For more information, see\n[the documentation](https://python-nnf.readthedocs.io/en/stable/cli.html).\n\n# Credits\n\n`python-nnf` up to version 0.2.1 was created by [Jan Verbeek](https://github.com/blyxxyz)\nunder mentorship of [Ronald de Haan](https://staff.science.uva.nl/r.dehaan/)\nat the [University of Amsterdam](https://www.uva.nl/). It was the subject of an\nundergraduate thesis, [*Developing a Python Package for Reasoning with NNF Sentences*](https://scripties.uba.uva.nl/scriptie/691650).\n",
"bugtrack_url": null,
"license": "ISC",
"summary": "Manipulate NNF (Negation Normal Form) logical sentences",
"version": "0.4.1",
"split_keywords": [
"logic",
"nnf",
"dimacs",
"dsharp"
],
"urls": [
{
"comment_text": "",
"digests": {
"md5": "6c72abb1179adc5fa73c51aa4d9f067c",
"sha256": "96d0d5797b829941cbbb816304690849cbfefd5361b4d78b378a6bd989c66ba2"
},
"downloads": -1,
"filename": "nnf-0.4.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "6c72abb1179adc5fa73c51aa4d9f067c",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.4",
"size": 598774,
"upload_time": "2022-12-13T05:01:11",
"upload_time_iso_8601": "2022-12-13T05:01:11.632430Z",
"url": "https://files.pythonhosted.org/packages/66/01/e82d4848bc67cd02b11cd274dbe352f3f4490149361d83456ee63a766959/nnf-0.4.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"md5": "60c0163496e128d2980ec4c3086bf4cf",
"sha256": "e972e7c1130d9e457241c8096e45ad3f16311c66e810e8c227deb3a43b4a3537"
},
"downloads": -1,
"filename": "nnf-0.4.1.tar.gz",
"has_sig": false,
"md5_digest": "60c0163496e128d2980ec4c3086bf4cf",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.4",
"size": 593887,
"upload_time": "2022-12-13T05:01:13",
"upload_time_iso_8601": "2022-12-13T05:01:13.810371Z",
"url": "https://files.pythonhosted.org/packages/82/16/12221f3c9d21340ca8378df5c047545e3e01ffb088b5177620e5bc8dd128/nnf-0.4.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2022-12-13 05:01:13",
"github": true,
"gitlab": false,
"bitbucket": false,
"github_user": "QuMuLab",
"github_project": "python-nnf",
"travis_ci": true,
"coveralls": true,
"github_actions": true,
"tox": true,
"lcname": "nnf"
}
JSON
