Name
Abstract | ||
|---|---|---|
As a data structure for representing and manipulating Boolean functions, BDDs (Binary Decision Diagrams) are commonly used in many fields such as model-checking, system verification and so on. For saving space and improving operation speed, all the existing packages limit the number of variables to 216. However, such a limitation also restrains its applicability. In this paper, we present TiniBDD, an efficient implementation of a 232 BDD package incorporating sub-allocation of memory and lightweight Garbage Collection as well as a new operator named as Satisfiable Assignment Operator. Compared with the well-known CUDD which is one of the best 216 BDD packages that can be attained publicly, the experiments show TiniBDD has comparable performance. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/TASE.2012.22 | TASE |
Keywords | Field | DocType |
new operator,binary decision diagrams,existing package,efficient implementation,cudd,satisfiable assignment operator,model-checking,data structures,lightweight garbage collection,216 bdd packages,232 bdd package,tinibdd,data structure,boolean functions,garbage collection,bdd package,comparable performance,system verification,memory sub-allocation,formal verification,boolean function,cognition,computer science,model checking,resource management,memory management | Boolean function,Data structure,Boolean circuit,Assignment,Computer science,Binary decision diagram,Theoretical computer science,Garbage collection,Boolean expression,And-inverter graph | Conference |
ISBN | Citations | PageRank |
978-1-4673-2353-6 | 1 | 0.37 |
References | Authors | |
5 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lv Guanfeng | 1 | 35 | 3.60 |
| Yao Chen | 2 | 24 | 4.72 |
| Yachao Feng | 3 | 1 | 0.71 |
| Qingliang Chen | 4 | 52 | 10.93 |
| Kaile Su | 5 | 668 | 60.11 |