Dynamic Programming for Symbolic Boolean Realizability and Synthesis

TL;DR

This work tackles Boolean synthesis for CNF specifications by reframing realizability and witness construction as a dynamic-programming problem over graded project-join trees, implemented in the DPSynth tool. The approach performs a bottom-up realizability check using BDD-based valuations to compute the realizability set, followed by a top-down synthesis pass that constructs witness functions for the output variables in terms of the inputs. It extends prior factored and monolithic methods by enabling partial realizability handling and improved scalability on large benchmarks, with experimental evidence showing favorable time and space performance relative to Factored RSynth and non-BDD approaches. The results highlight the practical impact for modular circuit design and temporal synthesis, where identifying the realizability domain and producing witnesses efficiently is crucial.

Abstract

Inspired by recent progress in dynamic programming approaches for weighted model counting, we investigate a dynamic-programming approach in the context of boolean realizability and synthesis, which takes a conjunctive-normal-form boolean formula over input and output variables, and aims at synthesizing witness functions for the output variables in terms of the inputs. We show how graded project-join trees, obtained via tree decomposition, can be used to compute a BDD representing the realizability set for the input formulas in a bottom-up order. We then show how the intermediate BDDs generated during realizability checking phase can be applied to synthesizing the witness functions in a top-down manner. An experimental evaluation of a solver -- DPSynth -- based on these ideas demonstrates that our approach for Boolean realizabilty and synthesis has superior time and space performance over a heuristics-based approach using same symbolic representations. We discuss the advantage on scalability of the new approach, and also investigate our findings on the performance of the DP framework.

Figures (5)

• Figure 1: Original and intermediate trees generated by our algorithms for the CNF example $(x_1 \lor y_4 \lor \neg y_5) \land (\neg x_3 \lor x_2 \lor \neg y_5) \land (\neg x_1 \lor x_2 \lor y_6) \land (\neg x_3 \lor x_1 \lor \neg y_4) \land (x_1 \lor \neg x_2 \lor x_3 \lor y_5)$. The label for each internal node is denoted by $e$.
• Figure 2:
• Figure 3:
• Figure 4:
• Figure 5:

Theorems & Definitions (20)

• definition thmcounterdefinition: Realizability
• definition thmcounterdefinition: Witnesses in Boolean Synthesis Problem
• definition thmcounterdefinition: Synthesis
• definition thmcounterdefinition: Project-Join Tree of a CNF formula
• definition thmcounterdefinition: Graded Project-Join Tree of a CNF formula Procount
• definition thmcounterdefinition: BDD-Valuations of Nodes in Project Join Tree
• theorem thmcountertheorem
• theorem thmcountertheorem
• theorem thmcountertheorem
• theorem thmcountertheorem