index.md (1131B)
1 +++ 2 title = 'Binary Decision Trees' 3 +++ 4 # Binary Decision Trees 5 used to represent a boolean function 6 7 dashed line to left is 0, solid line to right is 1 8 9 a formula is satisfiable if there is at least 1 leaf with a 1 10 11  12 13 ## Ordered Binary Decision Diagram (OBDD) 14 collapsing and removing nodes in a binary decision tree 15 16 rules: 17 1. leaves with 0 and 1 are collapsed 18 2. repeat: 19 20 - if 0 and 1 edge of non-leaf n lead to same node m: 21 - eliminate n 22 - redirect its incoming edges to m 23 - if non-leaves associated with same bool variable have 0 edge to same node and 1 edge to same node, then collapse 24 25 non-isomorphic reduced OBDDs are never semantically equivalent 26 27 sensitive to order change (which nodes are above which) 28 29 logical operations: 30 31 - negation — swap 0 and 1 in leaf nodes 32 - disjunction: 33 - leaves: O2 if O1 is 0, otherwise O1 34 - non-leaves: draw new nodes with disjunctions of previous Os 35 36  37 38 - conjunction: 39 - leaves: O2 if O1 is 1, otherwise O1 40 - non-leaves: same as disjunction