Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
‘restrict’ algorithm is linear to the size of the BDD because it involves a traversal of the BDD and modification of certain paths. This operation is crucial for evaluating BDDs with particular variable assignments and for simplifying BDDs in preparation for Boolean operations. Exists operation The