Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
algorithm This is a method applied to BDDs for evaluating or simplifying a Boolean function by fixing the value of one of its variables. Essentially, it “restricts” the function to the case where a variable x is either true or false. This operation is closely related to the Shannon expansion; when