<SYSTEM_TASK:>
Given the following text description, write Python code to implement the functionality described below step by step
<END_TASK>
<USER_TASK:>
Description:
 A binary decision diagram is a directed acyclic graph used to represent a Boolean function.
They were originally introduced by Lee, and later by Akers.
In 1986, Randal Bryant introduced the reduced, ordered BDD (ROBDD).
Let's take a look at some basic BDDs.
Step1:  A BDD is a full tree of Shannon cofactor expansions of the inputs variables from top (first variable) to bottom (last variable).
This is what it would look like if you do not merge isomorphic sub-trees.
Step2:  Join isomorphic 1 nodes
Step3:  Join isomorphic c nodes
Step4:  Join isomorphic b nodes
Step5:  Some examples
Step6:  BDDs are a canonical form.
Given an identical ordering of input variables,
equivalent functions will always produce identical BDDs.
This makes testing for SAT and UNSAT trivial.
A function is SAT if its BDD is not $0$,
and it is UNSAT if its BDD is not $1$.
Step7:  Formal equivalence checking is also trivial.
You can test whether two BDDs are equivalent by using the equivalent method,
or the Python is operator.
Step8:  The downside of BDDs is memory usage.
The size of some functions is heavily dependent on the ordering of the input variables,
but determining an optimal ordering is known to be a hard problem.
Certain functions,
no matter how cleverly you order their input variables,
will result in an exponentially-sized graph.
One example is multiplication.
<ASSISTANT_TASK:>
Python Code:
# Zero and One
%dotobjs pyeda.boolalg.bdd.BDDZERO, pyeda.boolalg.bdd.BDDONE
# Complement and Variable
%dotobjs ~a, a
Explanation: A binary decision diagram is a directed acyclic graph used to represent a Boolean function.
They were originally introduced by Lee, and later by Akers.
In 1986, Randal Bryant introduced the reduced, ordered BDD (ROBDD).
Let's take a look at some basic BDDs.
End of explanation
%%dot graph {
    a   [label=a,shape=circle]
    b0  [label=b,shape=circle]
    b1  [label=b,shape=circle]
    c00 [label=c,shape=circle]
    c01 [label=c,shape=circle]
    c10 [label=c,shape=circle]
    c11 [label=c,shape=circle]
    zero000 [label=0,shape=box]
    one001  [label=1,shape=box]
    one010  [label=1,shape=box]
    one011  [label=1,shape=box]
    one100  [label=1,shape=box]
    one101  [label=1,shape=box]
    one110  [label=1,shape=box]
    one111  [label=1,shape=box]
    a -- b0 [label=0]
    a -- b1 [label=1]
    b0 -- c00 [label=0]
    b0 -- c01 [label=1]
    b1 -- c10 [label=0]
    b1 -- c11 [label=1]
    c00 -- zero000 [label=0]
    c00 -- one001  [label=1]
    c01 -- one010  [label=0]
    c01 -- one011  [label=1]
    c10 -- one100  [label=0]
    c10 -- one101  [label=1]
    c11 -- one110  [label=0]
    c11 -- one111  [label=1]
}
Explanation: A BDD is a full tree of Shannon cofactor expansions of the inputs variables from top (first variable) to bottom (last variable).
This is what it would look like if you do not merge isomorphic sub-trees.
End of explanation
%%dot graph {
    a   [label=a,shape=circle]
    b0  [label=b,shape=circle]
    b1  [label=b,shape=circle]
    c00 [label=c,shape=circle]
    c01 [label=c,shape=circle]
    c10 [label=c,shape=circle]
    c11 [label=c,shape=circle]
    zero [label=0,shape=box]
    one  [label=1,shape=box]
    a -- b0 [label=0,style=dashed]
    a -- b1 [label=1]
    b0 -- c00 [label=0,style=dashed]
    b0 -- c01 [label=1]
    b1 -- c10 [label=0,style=dashed]
    b1 -- c11 [label=1]
    c00 -- zero [label=0,style=dashed]
    c00 -- one  [label=1]
    c01 -- one  [label=0,style=dashed]
    c01 -- one  [label=1]
    c10 -- one  [label=0,style=dashed]
    c10 -- one  [label=1]
    c11 -- one  [label=0,style=dashed]
    c11 -- one  [label=1]
}
Explanation: Join isomorphic 1 nodes:
End of explanation
%%dot graph {
    a   [label=a,shape=circle]
    b0  [label=b,shape=circle]
    b1  [label=b,shape=circle]
    c00 [label=c,shape=circle]
    zero [label=0,shape=box]
    one  [label=1,shape=box]
    a -- b0 [label=0,style=dashed]
    a -- b1 [label=1]
    b0 -- c00 [label=0,style=dashed]
    b0 -- one [label=1]
    b1 -- one [label=0,style=dashed]
    b1 -- one  [label=1]
    c00 -- zero [label=0,style=dashed]
    c00 -- one  [label=1]
}
Explanation: Join isomorphic c nodes:
End of explanation
%%dot graph {
    a   [label=a,shape=circle]
    b0  [label=b,shape=circle]
    c00 [label=c,shape=circle]
    zero [label=0,shape=box]
    one  [label=1,shape=box]
    a -- b0 [label=0,style=dashed]
    a -- one [label=1]
    b0 -- c00 [label=0,style=dashed]
    b0 -- one [label=1]
    c00 -- zero [label=0,style=dashed]
    c00 -- one  [label=1]
}
Explanation: Join isomorphic b nodes:
End of explanation
%dotobj a | b | c
%dotobj a & b & c
%dotobj a ^ b ^ c
# Equal-3
%dotobj ~a & ~b & ~c | a & b & c
# Majority-3
%dotobj a & b | a & c | b & c
# OneHot-3
%dotobj (~a | ~b) & (~a | ~c) & (~b | ~c) & (a | b | c)
Explanation: Some examples:
End of explanation
# A full minterm cover is unity.
~a & ~b | ~a & b | a & ~b | a & b
# a full maxterm cover is empty
(~a | ~b) & (~a | b) & (a | ~b) & (a | b)
Explanation: BDDs are a canonical form.
Given an identical ordering of input variables,
equivalent functions will always produce identical BDDs.
This makes testing for SAT and UNSAT trivial.
A function is SAT if its BDD is not $0$,
and it is UNSAT if its BDD is not $1$.
End of explanation
F1 = a ^ b ^ c
F2 = ~a & ~b & c | ~a & b & ~c | a & ~b & ~c | a & b & c
F1.equivalent(F2)
F1 is F2
Explanation: Formal equivalence checking is also trivial.
You can test whether two BDDs are equivalent by using the equivalent method,
or the Python is operator.
End of explanation
X = bddvars('x', 6)
%dotobj X[0] & X[1] | X[2] & X[3] | X[4] & X[5]
%dotobj X[0] & X[3] | X[1] & X[4] | X[2] & X[5]
Explanation: The downside of BDDs is memory usage.
The size of some functions is heavily dependent on the ordering of the input variables,
but determining an optimal ordering is known to be a hard problem.
Certain functions,
no matter how cleverly you order their input variables,
will result in an exponentially-sized graph.
One example is multiplication.
End of explanation
<END_TASK>