Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
function using Shannon’s expansion is efficient because it systematically breaks down the function into simpler parts. However, the efficiency of the resulting BDD strongly depends on the variable ordering chosen during the expansion. The Shannon expansion and the ‘restrict’ algorithm are integral