logicboolean-logicbinary-decision-diagram

convert binary formula to Shannon Normal Form


I would like to know the steps to convert a binary formula to Shannon Normal Form.

a⪯b⪯c⪯d - variable ordering.
F = b&c&!d|c&d&!b|d&!c|!c&!d

How can I convert this to Shannon Normal Form?


Solution

  • You start by calculating F|{a=0} and F|{a=1}. Because F is not dependent on variable a, you will get F for both case:

    F|{a=0} = F
    F|{a=1} = F
    

    You continue by calculating F|{a=0,b=0}, F|{a=0,b=1}, F|{a=1,b=0}, and F|{a=1,b=1}. You will get

    F|{a=0,b=0} = F|{a=1,b=0} = c&d|d&!c|!c&!d = !c|d
    F|{a=0,b=1} = F|{a=1,b=1} = c&!d|d&!c|!c&!d = !c|!d
    

    You continue with variable c and variable d and finally you get:

    F = !a(!b(!c(!d&1+d&1)|c(!d&0+d&1))|b(!c(!d&1+d&1)|c(!d&1+d&0))|
         a(!b(!c(!d&1+d&1)|c(!d&0+d&1))|b(!c(!d&1+d&1)|c(!d&1+d&0))
    

    If you need the opposite ordering, just calculate in revert order of variables, you may get quite different result.

    And here is the screenshot from BDD Scout (http://biddy.meolic.com/), unfortunately this tool does not support BDDs without complemented edges, yet. BDD for function F