Logic Lecture 5 Flashcards
What is a binary decision tree?
A tree structure representing a Boolean function with variables ordered in a hierarchy.
What do non-leaf nodes in a binary decision tree represent?
Boolean variables that determine branching.
What do leaf nodes in a binary decision tree contain?
Either 0 or 1, representing the function’s output.
What does a dashed line in a binary decision tree represent?
The path taken when the variable is 0.
What does a solid line in a binary decision tree represent?
The path taken when the variable is 1.
What is an ordered binary decision diagram (OBDD)?
A binary decision tree with nodes collapsed using specific rules to reduce redundancy.
What are the three rules for reducing an OBDD?
C1: Collapse identical leaves, C2: Eliminate redundant nodes, C3: Merge identical non-leaf nodes.
What happens in Rule C1 for reducing OBDDs?
Identical leaf nodes (0s and 1s) are collapsed.
What happens in Rule C2 for reducing OBDDs?
A node is eliminated if both of its outgoing edges lead to the same node.
What happens in Rule C3 for reducing OBDDs?
Two or more non-leaf nodes are merged if they have the same variable and identical children.
What is a reduced OBDD?
An OBDD where none of the reduction rules (C1, C2, C3) can be further applied.
What is the key property of a reduced OBDD?
It provides a unique representation of a Boolean function for a given variable order.
What is the effect of variable order in OBDDs?
The size of the OBDD can vary significantly depending on the chosen order.
What is the worst-case scenario for an OBDD?
An exponential-sized representation if variables are ordered poorly.
What is an application of reduced OBDDs?
They are used in logic synthesis for hardware circuit design.
How do reduced OBDDs help in symbolic state-space representation?
They efficiently encode large state spaces in formal methods.
What is a parity function?
A Boolean function that outputs 1 if an even number of input bits are 1.
What is the size of the reduced OBDD for an n-variable parity function?
It has 2n + 1 nodes.
Why are OBDD representations sensitive to variable order?
Different orders can drastically change the size of the OBDD.
What is an NP-hard problem in OBDDs?
Finding the optimal variable order to minimize the OBDD size.
What are logical operations on OBDDs?
Operations such as conjunction (AND), disjunction (OR), and negation applied to Boolean functions.
How is negation applied to an OBDD?
By swapping 0 and 1 in the leaf nodes.
How is disjunction applied to OBDDs?
By recursively computing OR operations while maintaining variable order.
How is conjunction applied to OBDDs?
By recursively computing AND operations while maintaining variable order.
What is universal quantification in Boolean logic?
∀x φ is true if φ remains true for both x = 0 and x = 1.
What is existential quantification in Boolean logic?
∃x φ is true if φ is true for at least one value of x.
How is universal quantification applied to an OBDD?
By computing the conjunction of OBDDs with x substituted as 0 and 1.
How is existential quantification applied to an OBDD?
By computing the disjunction of OBDDs with x substituted as 0 and 1.
What is an example of a universally quantified formula?
∀x (x → y) is equivalent to y.
What is an example of an existentially quantified formula?
∃x x is a tautology since x can be 1.
