Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
This expansion allows a Boolean function to be broken down recursively until it is fully represented as a BDD, where each decision node represents the choice of setting a variable x to 0 or 1, leading to different subfunctions (subtrees in the BDD). The process of constructing a BDD from a Boolean