Bdd, Binary Decision Diagrams, Software Verification, Model Checking, Boolean Function.
‘apply’ operation is used to compute the disjunction (logical OR) of these two results. This process effectively evaluates the truth of ϕ under the assumption that the variable x can take on either value, true or false, thereby determining the existence of a satisfying assignment for x in the