Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams

Yi Lin, Moshe Y. Vardi

TL;DR

The paper advances symbolic boolean synthesis by introducing a dynamic-programming framework built on zero-suppressed decision diagrams (ZDDs) and graded project-join trees. It defines realizability and witness construction within this DP setting, then presents a practical tool (DPZynth) that balances planning and execution via a magic-number bound to treewidth, showing competitive end-to-end performance against BDD-based and monolithic ZDD solvers. The work demonstrates the method's scalability and complementary value to industrial solvers, and outlines future directions like machine-learning-driven configuration and broader applications in symbolic model checking and temporal synthesis. Overall, it offers a principled, scalable approach to ZDD-based boolean synthesis with actionable insights into planning-execution trade-offs.

Abstract

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.

Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams

TL;DR

The paper advances symbolic boolean synthesis by introducing a dynamic-programming framework built on zero-suppressed decision diagrams (ZDDs) and graded project-join trees. It defines realizability and witness construction within this DP setting, then presents a practical tool (DPZynth) that balances planning and execution via a magic-number bound to treewidth, showing competitive end-to-end performance against BDD-based and monolithic ZDD solvers. The work demonstrates the method's scalability and complementary value to industrial solvers, and outlines future directions like machine-learning-driven configuration and broader applications in symbolic model checking and temporal synthesis. Overall, it offers a principled, scalable approach to ZDD-based boolean synthesis with actionable insights into planning-execution trade-offs.

Abstract

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.

Paper Structure

This paper contains 27 sections, 8 theorems, 13 equations, 4 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Binary Decision Diagrams.
  4. Zero-Suppressed Decision Diagrams (ZDDs).
  5. ZDD Realizability Algorithm
  6. Project-join tree of a CNF formula.
  7. Graded project-join tree of a CNF formula.
  8. ZDD Operations and Notations
  9. Notations on sub-trees:
  10. Realizability Set
  11. Synthesis of Witnesses
  12. Monolithic Techniques for ZDD-based Synthesis
  13. Algorithm for ZDD-based Synthesis on Graded Project-join Trees decompositions
  14. Synthesizing Inner-node Variables.
  15. Synthesizing on Inter-node Variables.
  16. ...and 12 more sections

Key Result

lemma 1

Symbolic Resolution For a CNF formula ${\varphi}$ with a single boolean variable $y$ that occurs in this formula, the ZDD of ${\Sigma}_y{\varphi}$ is equivalent to a representation of $(( \llbracket{ \varphi^+_y }\rrbracket \times_{cd} \llbracket{ \varphi^-_y }\rrbracket) \bigcup_{sf} \llbracket{ \v

Figures (4)

  • Figure 1:
  • Figure 2: Comparison on End-to-end Realizability Time
  • Figure 3: Comparison on End-to-end Synthesis Time
  • Figure 4:

Theorems & Definitions (21)

  • definition 1: Boolean Synthesis Problem
  • definition 2: Realizability Set
  • definition 3: Full, Partial and Nullary Realizability
  • definition 4: Witnesses in Boolean Synthesis Problem
  • definition 5: Synthesis
  • definition 6
  • definition 7: ZDD Operations minato1993zeroClause_Distribution_and_Subsum_Free_DBLP:conf/ictai/ChatalicS00mishchenko2001introductionKNUTH_10.5555/1593023)
  • lemma 1
  • definition 8: ZDD-Valuations of Nodes in Graded Project Join Tree
  • theorem 1
  • ...and 11 more