Welcome to python-nnf’s documentation!

python-nnf is a package for working with logical sentences written in the negation normal form.

Contents:

• Installing
• Module reference
  • Module contents
  • Submodules
  • nnf.operators module
  • nnf.dimacs module
  • nnf.dsharp module
  • nnf.amc module
  • nnf.tseitin module
  • nnf.kissat module
  • nnf.pysat module
• Command line interface
  • SAT solving
  • Sentence summary
  • Visualizing sentences
• Caveats
  • Node duplication
  • Decomposability and determinism
  • Other duplication inefficiencies

Introduction

Sentences are made up of nodes. To start with, define some variables:

>>> from nnf import Var
>>> A, B, C = Var('A'), Var('B'), Var('C')

Then, if you want to write the sentence “A or B”:

>>> from nnf import Or
>>> sentence = Or({A, B})
>>> sentence = A | B  # alternative syntax

Or “B and not C”:

>>> from nnf import And
>>> sentence = And({B, ~C})
>>> sentence = B & ~C

Of course you can nest these, for more interesting sentences:

>>> sentence = Or({And({A, B}), And({~B, C})})

You can ask queries, and perform transformations:

>>> sentence.decomposable()
True
>>> sentence.smooth()
False
>>> list(sentence.models())
[{'A': True, 'B': True, 'C': True}, {'A': True, 'B': False, ...
>>> new = sentence.condition({'B': True})
>>> new
Or({And({A, true}), And({false, C})})
>>> list(new.models())
[{'A': True, 'C': True}, {'A': True, 'C': False}]
>>> new.simplify()
A

Indices and tables

• Index
• Module Index
• Search Page