Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams

TL;DR

This paper introduces a dynamic-programming framework using zero-suppressed decision diagrams for boolean synthesis, addressing theoretical challenges, developing a tool, and demonstrating its potential in industrial applications.

Contribution

It presents a novel ZDD-based dynamic programming approach for boolean synthesis, including theoretical solutions, a new tool, and experimental insights.

Findings

The proposed algorithm performs well across various benchmarks.

The concept of magic number helps bound planning time and treewidth.

The framework complements existing industrial synthesis methods.

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.