<jupyter_start><jupyter_text>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, <NAME> introduced the reduced, ordered BDD (ROBDD).Let's take a look at some basic BDDs.<jupyter_code># Zero and One
%dotobjs pyeda.boolalg.bdd.BDDZERO, pyeda.boolalg.bdd.BDDONE
# Complement and Variable
%dotobjs ~a, a<jupyter_output><empty_output><jupyter_text>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.<jupyter_code>%%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]
}<jupyter_output><empty_output><jupyter_text>Join isomorphic `1` nodes:<jupyter_code>%%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]
}<jupyter_output><empty_output><jupyter_text>Join isomorphic `c` nodes:<jupyter_code>%%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]
}<jupyter_output><empty_output><jupyter_text>Join isomorphic `b` nodes:<jupyter_code>%%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]
}<jupyter_output><empty_output><jupyter_text>Some examples:<jupyter_code>%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)<jupyter_output><empty_output><jupyter_text>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$.<jupyter_code># 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)<jupyter_output><empty_output><jupyter_text>Formal equivalence checking is also trivial.You can test whether two BDDs are equivalent by using the `equivalent` method,or the Python `is` operator.<jupyter_code>F1 = a ^ b ^ c
F2 = ~a & ~b & c | ~a & b & ~c | a & ~b & ~c | a & b & c
F1.equivalent(F2)
F1 is F2<jupyter_output><empty_output><jupyter_text>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.<jupyter_code>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]<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.14805725971370143, 'fraction_numerical': 0.049284253578732104, 'mean_word_length': 3.4262443438914025, 'pattern_counts': {'":': 0, '<': 38, '<?xml version=': 0, '>': 38, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '9', 'dir': 'jupyter-structured-clean-dedup', 'id': '614815', 'license': 'MIT', 'n_tokens_mistral': 2073, 'n_tokens_neox': 1938, 'n_words': 511, 'path': 'ipynb/BDDs.ipynb', 'repo_name': 'mikiec84/pyeda', 'size': '4897'}