Mutual conversions between generalised arithmetic expansions and free binary decision diagrams

1998 ◽  
Vol 145 (4) ◽  
pp. 219 ◽  
Author(s):  
B.J. Falkowski ◽  
C.-H. Chang
Keyword(s):  
Binary Decision Diagrams ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Free Binary Decision Diagrams

scholarly journals Building free Binary Decision Diagrams using SAT solvers

2007 ◽  
Vol 20 (3) ◽  
pp. 381-394 ◽  
Author(s):  
Robert Wille ◽  
Görschwin Fey ◽  
Rolf Drechsler
Keyword(s):  
Boolean Functions ◽  
Binary Decision Diagrams ◽  
Compact Representation ◽  
Decision Diagrams ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
Sat Solvers ◽  
Free Binary Decision Diagrams ◽  
Sat Solver ◽  
Open Question

Free Binary Decision Diagrams (FBDDs) are a data structure for the representation of Boolean functions. In contrast to Ordered Binary Decision Diagrams (OBDDs) FBDDs allow different variable orderings along each path. Thus, FBDDs are the more compact representation while most of the properties of OBDDs are kept. However, how to efficiently build small FBDDs for a given function is still an open question. In this work we propose FBDD construction with the help of SAT solvers. "Recording" the single steps of a SAT solver during the search process leads to an FBDD. Furthermore, by exploiting approaches for identifying isomorphic sub-graphs, i.e. cutlines or cutsets reduced FBDDs are constructed.

Sign in / Sign up

Export Citation Format

Share Document