Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
use of shared subtrees and the canonical nature of BDDs can dramatically reduce the number of unique subproblems that need to be solved, leveraging memoization to avoid redundant computation. The implementation of these Boolean operations on BDDs which integrates the principles of Shannon’s