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