Difference between revisions of "Publications/newton.18.tocl"
From LRDE
| Line 5: | Line 5: | ||
| title = A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams |
| title = A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams |
||
| journal = ACM Transactions on Computational Logic |
| journal = ACM Transactions on Computational Logic |
||
| + | | volume = 20 |
||
| + | | number = 1 |
||
| + | | pages = [1 to 36 |
||
| lrdeprojects = Climb |
| lrdeprojects = Climb |
||
| abstract = Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean expressions, integrated circuit design, type inferencers, model checkers, and many other applications. Although the ROBDD is a lightweight data structure to implement, the behavior, in terms of memory allocation, may not be obvious to the program architect. We explore experimentally, numerically, and theoretically the typical and worst-case ROBDD sizes in terms of number of nodes and residual compression ratios, as compared to unreduced BDDs. While our theoretical results are not surprising, as they are in keeping with previously known results, we believe our method contributes to the current body of research by our experimental and statistical treatment of ROBDD sizes. In addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code. |
| abstract = Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean expressions, integrated circuit design, type inferencers, model checkers, and many other applications. Although the ROBDD is a lightweight data structure to implement, the behavior, in terms of memory allocation, may not be obvious to the program architect. We explore experimentally, numerically, and theoretically the typical and worst-case ROBDD sizes in terms of number of nodes and residual compression ratios, as compared to unreduced BDDs. While our theoretical results are not surprising, as they are in keeping with previously known results, we believe our method contributes to the current body of research by our experimental and statistical treatment of ROBDD sizes. In addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code. |
||
| Line 18: | Line 21: | ||
Size of Reduced Ordered Binary Decision Diagrams<nowiki>}</nowiki>, |
Size of Reduced Ordered Binary Decision Diagrams<nowiki>}</nowiki>, |
||
journal = <nowiki>{</nowiki>ACM Transactions on Computational Logic<nowiki>}</nowiki>, |
journal = <nowiki>{</nowiki>ACM Transactions on Computational Logic<nowiki>}</nowiki>, |
||
| − | year = |
+ | year = 2019, |
| − | + | volume = <nowiki>{</nowiki>20<nowiki>}</nowiki>, |
|
| ⚫ | |||
| − | (Reduced Ordered BDDs) are a common data structure for |
||
| + | month = jan, |
||
| − | manipulating Boolean expressions, integrated circuit |
||
| + | pages = [1--36 |
||
| − | design, type inferencers, model checkers, and many other |
||
| − | applications. Although the ROBDD is a lightweight data |
||
| − | structure to implement, the behavior, in terms of memory |
||
| − | allocation, may not be obvious to the program architect. We |
||
| − | explore experimentally, numerically, and theoretically the |
||
| − | typical and worst-case ROBDD sizes in terms of number of |
||
| − | nodes and residual compression ratios, as compared to |
||
| − | unreduced BDDs. While our theoretical results are not |
||
| − | surprising, as they are in keeping with previously known |
||
| − | results, we believe our method contributes to the current |
||
| − | body of research by our experimental and statistical |
||
| − | treatment of ROBDD sizes. In addition, we provide an |
||
| − | algorithm to calculate the worst-case size. Finally, we |
||
| − | present an algorithm for constructing a worst-case ROBDD of |
||
| − | a given number of variables. Our approach may be useful to |
||
| − | projects deciding whether the ROBDD is the appropriate data |
||
| − | structure to use, and in building worst-case examples to |
||
| − | test their code.<nowiki>}</nowiki>, |
||
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 11:22, 3 March 2020
- Authors
- Jim Newton, Didier Verna
- Journal
- ACM Transactions on Computational Logic
- Type
- article
- Projects
- Climb
- Date
- 2018-08-28
Abstract
Binary Decision Diagrams (BDDs) and in particular ROBDDs (Reduced Ordered BDDs) are a common data structure for manipulating Boolean expressions, integrated circuit design, type inferencers, model checkers, and many other applications. Although the ROBDD is a lightweight data structure to implement, the behavior, in terms of memory allocation, may not be obvious to the program architect. We explore experimentally, numerically, and theoretically the typical and worst-case ROBDD sizes in terms of number of nodes and residual compression ratios, as compared to unreduced BDDs. While our theoretical results are not surprising, as they are in keeping with previously known results, we believe our method contributes to the current body of research by our experimental and statistical treatment of ROBDD sizes. In addition, we provide an algorithm to calculate the worst-case size. Finally, we present an algorithm for constructing a worst-case ROBDD of a given number of variables. Our approach may be useful to projects deciding whether the ROBDD is the appropriate data structure to use, and in building worst-case examples to test their code.
Documents
Bibtex (lrde.bib)
@Article{ newton.18.tocl,
author = {Jim Newton and Didier Verna},
title = {A Theoretical and Numerical Analysis of the Worst-Case
Size of Reduced Ordered Binary Decision Diagrams},
journal = {ACM Transactions on Computational Logic},
year = 2019,
volume = {20},
number = {1},
month = jan,
pages = [1--36
}