Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915659724619776 |
|---|---|
| author | Lin, Yi Vardi, Moshe Y. |
| author_facet | Lin, Yi Vardi, Moshe Y. |
| contents | Motivated by functional synthesis in sequential circuit construction and quantified boolean formulas (QBF), boolean synthesis serves as one of the core problems in Formal Methods. Recent advances show that decision diagrams (DD) are particularly competitive in symbolic approaches for boolean synthesis, among which zero-suppressed decision diagram (ZDD) is a relatively new algorithmic approach, but is complementary to the industrial portfolio, where binary decision diagrams (BDDs) are more often applied. We propose a new dynamic-programming ZDD-based framework in the context of boolean synthesis, show solutions to theoretical challenges, develop a tool, and investigate the experimental performance. We also propose an idea of magic number that functions as the upper bound of planning-phase time and treewidth, showing how to interpret the exploration-exploitation dilemma in planning-execution synthesis framework. The algorithm we propose shows its strengths in general, gives inspiration for future needs to determine industrial magic numbers, and justifies that the framework we propose is an appropriate addition to the industrial synthesis solvers portfolio. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_07018 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams Lin, Yi Vardi, Moshe Y. Symbolic Computation Logic in Computer Science I.1.2; F.2.1; F.2.2 Motivated by functional synthesis in sequential circuit construction and quantified boolean formulas (QBF), boolean synthesis serves as one of the core problems in Formal Methods. Recent advances show that decision diagrams (DD) are particularly competitive in symbolic approaches for boolean synthesis, among which zero-suppressed decision diagram (ZDD) is a relatively new algorithmic approach, but is complementary to the industrial portfolio, where binary decision diagrams (BDDs) are more often applied. We propose a new dynamic-programming ZDD-based framework in the context of boolean synthesis, show solutions to theoretical challenges, develop a tool, and investigate the experimental performance. We also propose an idea of magic number that functions as the upper bound of planning-phase time and treewidth, showing how to interpret the exploration-exploitation dilemma in planning-execution synthesis framework. The algorithm we propose shows its strengths in general, gives inspiration for future needs to determine industrial magic numbers, and justifies that the framework we propose is an appropriate addition to the industrial synthesis solvers portfolio. |
| title | Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams |
| topic | Symbolic Computation Logic in Computer Science I.1.2; F.2.1; F.2.2 |
| url | https://arxiv.org/abs/2512.07018 |