BDD operations Paul Jackson1 University of Edinburgh Automated Reasoning 21st November 2013 1 Diagrams from Huth & Ryan, LiCS, 2nd Ed. reduce algorithm Aim is to construct a ROBDD from an OBDD. I Adds integer labels id(n) to each node n of a BDD in a single bottom-up pass I Key property: if nodes m and n are labelled, then id(m) = id(n) iff m and n represent the same Boolean function. I Rules for adding label to node n: I I I I I remove duplicate terminals: if n terminal, set id(n) to val(n) remove redundant tests: if id(lo(n)) = id(hi(n)), set id(n) to id(lo(n)) remove  duplicate nodes: if there exists  a labelled node m such = var(n)   var(m) id(lo(m)) = id(lo(n)) , set id(n) to id(m) that   id(hi(m)) = id(hi(n)) Use hash table with hvar(n), id(lo(n)), id(hi(n))i keys for O(1) search time otherwise, set id(n) to unused number ROBDD generated by using 1 node from each class of nodes with the same label reduce example #4 #3 #4 x1 #2 x2 #3 x2 x1 x2 Reduce =⇒ #2 #0 0 #2 x3 #1 1 #2 #0 0 #1 x3 x3 1 #0 0 #1 1 apply algorithm I I Let op be a symbol for any binary operation on boolean formulas. (e.g. ∧, ∨, ⊕) Given BDDs Bf and Bg for boolean formulas f and g , apply(op, Bf , Bg ) computes a BDD for f op g . Can also do negation if op is λx. x ⊕ >. I If BDD I I xm B represents a Boolean formula f , @ @ B0 then sub-BDD B represents f [0/x], B 0 represents f [1/x], and have f ≡ x.f [0/x] + x.f [1/x] I This is the Shannon expansion of Boolean formula f with respect to the variable x While Sub-BDDs B and B 0 are drawn as distinct, in general they share structure apply algorithm II I By applying Shannon expansion to f and g in f op g and rearranging terms, we get a recursive characterisation of op. f op g = x.(f [0/x] op g [0/x]) + x.(f [1/x] op g [1/x]) I This motivates a recursive algorithm for apply apply algorithm III xm apply(op, @ @ B B 0 xm apply(op, B ) @ @ C , @ @ B xm , C @ @ 0 C xm = apply(op, B, C ) ) apply(op, B 0 , C 0 ) xm = @ @ 0 apply(op, B, C ) apply(op, B 0 , C ) where C is 1) a terminal node or 2) a non-terminal with var (root(C )) > x apply(op, B xm , ) @ @ C C xm = @ @ 0 apply(op, B, C ) apply(op, B, C 0 ) where B is 1) a terminal node or 2) a non-terminal with var (root(B)) > x apply(op, u , v ) = w where w = u op v apply example Compute apply(+, Bf , Bg ) where Bf and Bg are: R1 R2 S1 x1 x1 x2 x3 R3 x3 S2 + R4 S3 x4 R5 R6 0 1 x4 S4 S5 0 1 Recursive calls of apply (R1 , S1 ) x1 (R2 , S3 ) (R3 , S2 ) x2 x3 (R4 , S3 ) (R3 , S3 ) x4 x3 (R5 , S4 ) (R6 , S5 ) (R5 , S4 ) (R4 , S3 ) (R4 , S3 ) (R6 , S5 ) x4 (R6 , S3 ) x4 x4 (R6 , S5 ) (R6 , S4 ) (R5 , S4 ) (R6 , S5 ) (R6 , S5 ) Final result from apply execution x1 x2 x3 x4 0 1 apply remarks I In general, result will not be an ROBDD, so need to use reduce afterwards I I Or can incorporate aspects of reduce into apply so result is always reduced Many calls can be identical, so calls memoized to improve efficiency Other operations I restrict(0, x, Bf ) computes ROBDD for f [0/x] 1. For each node n labelled with an x, incoming edges are redirected to lo(n) and n is removed. 2. Resulting BDD is reduced. I exists(x, Bf ) computes ROBDD for ∃x. f I Uses identity (∃x. f ) ≡ f [0/x] + f [1/x] and restrict and apply functions Time complexities Algorithm Input OBDD(s) Output OBDD Time-complexity reduce B reduced B O(|B| · log |B|) apply Bf , Bg (reduced) Bf O(|Bf | · |Bg |) op g (reduced) restrict Bf (reduced) Bf [0/x] or Bf [1/x] (reduced) O(|Bf | · log |Bf |) ∃ B∃x1 .∃x2 ....∃xn .f (reduced) NP-complete Bf (reduced) Encoding CTL algorithms using BDDs I I States represented using Boolean vectors hv1 , . . . , vn i, where vi ∈ {0, 1}. I Sets of states represented using BDDs on n variables x1 , . . . xn describing characteristic functions of sets. I Set operations ∪, ∩,¯ made effective using using the apply and the Boolean operations +, ·,¯. Transition relations described using BDDs on 2n variables. I I I If Boolean variables x1 , . . . xn describe initial state and Boolean variables x10 , . . . xn0 describe next state, then good ordering is x1 , x10 , x2 , x20 , . . . xn , xn0 . Translations of Boolean formulas describing state sets and transition relations into BDDs make use of apply algorithm, following structure of formulas I This avoids the intractable exponential blow-up if instead one tried to first construct a binary decision tree. Encoding CTL algorithms using BDDs II I Function application . pre∃ (Y ) = {s ∈ S | ∃s 0 ∈ S. s → s 0 ∧ s 0 ∈ Y } is represented by the BDD exists(x̂ 0 , apply(·, B→ , BY 0 )) , where I I I B→ is the BDD representing the transition relation → BY 0 is the BDD representing set Y with the variables x1 , . . . xn renamed to x10 , . . . xn0 Function application . pre∀ (Y ) = {s ∈ S | ∀s 0 ∈ S. s → s 0 ⇒ s 0 ∈ Y } is represented using the identity pre∀ (Y ) = S − pre∃ (S − Y ) and the representation of pre∃ (S − Y ) and set complement.