Installation Link to heading

I am using MacOS, So, I needed to install clang first (from llvm brew).

brew install llvm

Then, we install pyeda but then again, on MacOS, I got compilation error. Asking chatgpt, it said to modify the code or add the following CFLAGS.

export CFLAGS="-Wno-incompatible-function-pointer-types"
pip install pyeda

First example Link to heading

The first example uses truth table to get an expression.

In [2]: from pyeda.inter import *

In [3]: X = exprvars('x', 3)
   ...: f = truthtable(X, "00000001")

In [4]: f
Out[4]:
x[2] x[1] x[0]
   0    0    0 : 0
   0    0    1 : 0
   0    1    0 : 0
   0    1    1 : 0
   1    0    0 : 0
   1    0    1 : 0
   1    1    0 : 0
   1    1    1 : 1

In [5]: truthtable2expr(f)
Out[5]: And(x[0], x[1], x[2])

BDD Link to heading

BDDs are supper important and interesting data structures to handle binary boolean expressions.

In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function.

In [6]: f = expr("a & b | a & c | b & c")

In [7]: f
Out[7]: Or(And(a, b), And(a, c), And(b, c))

In [8]: bdd1 = expr2bdd(f)

In [9]: bdd1
Out[9]: <pyeda.boolalg.bdd.BinaryDecisionDiagram at 0x103536cf0>

Graphviz Link to heading

Generating dot for graphviz

In [10]: f.to_dot()
Out[10]: 'graph EXPR {\', \'rankdir=BT; n105553136975872 [label="a",shape=box]; n105553136975904 [label="b",shape=box]; n105553136976128 [label=and,shape=circle]; n105553136975872 [label="a",shape=box]; n105553136975968 [label="c",shape=box]; n105553136976160 [label=and,shape=circle]; n105553136975904 [label="b",shape=box]; n105553136975968 [label="c",shape=box]; n105553136976192 [label=and,shape=circle]; n105553136976352 [label=or,shape=circle]; n105553136975872 -- n105553136976128; n105553136975904 -- n105553136976128; n105553136975872 -- n105553136976160; n105553136975968 -- n105553136976160; n105553136975904 -- n105553136976192; n105553136975968 -- n105553136976192; n105553136976128 -- n105553136976352; n105553136976160 -- n105553136976352; n105553136976192 -- n105553136976352; }'

SAT Link to heading

From pyEDA docs

Like we mentioned in the introduction, BDDs are a canonical form. That means that all unsatisfiable functions will reduce to zero, and all tautologies will reduce to one. If you simply want to check whether a function is SAT or UNSAT, just construct a BDD, and test whether it is zero/one.

In [11]: a, b = map(bddvar, 'ab')

In [12]:  f = ~a & ~b | ~a & b | a & ~b | a & b

In [13]: f
Out[13]: 1

In [14]: f.is_one()
Out[14]: True

In [15]: f.is_zero()
Out[15]: False