Binary Decision Diagrams

libmc.BDD offers a class for generating binary decision diagrams.

Constants

The two constant nodes representing True and False can be accessed through the static class methods true() and false() respectively.

true  = BDD.true()
false = BDD.false()

Variables

Variable nodes are defined by having an index greater or equal to zero.

a = BDD(0)
b = BDD(1)

Since they have to be unique, a repeated call to the constructor using the same index will return a reference to the specific node instead of allocating a new one.

assert a is BDD(0)
assert b is BDD(1)

Operators

Operations are carried out using the logical connectives ~, |, & and ^

~a
a & b
a | b
a ^ b

Visualization

The toDot() method can be used generate the DOT language string for a given BDD:

dot = (~(a ^ b)).toDot()

Write it to a file:

with open("xnor.dot", 'w') as f:
    f.write(dot)

Generate a PDF:

with open("xnor.pdf", 'w') as f:
    import subprocess
    subprocess.run(["dot", "-Tpdf", "xnor.dot"], stdout=f)

Enjoy :)