Dynamic Programming for Symbolic Boolean Realizability and Synthesis

TL;DR

This paper introduces a dynamic programming approach using tree decomposition and BDDs for boolean realizability and synthesis, demonstrating improved efficiency over heuristic methods.

Contribution

The paper presents a novel dynamic programming framework for boolean realizability and synthesis using graded project-join trees and BDDs, enhancing scalability and performance.

Findings

DPSynth outperforms heuristic approaches in time and space.

The approach scales better for large formulas.

Experimental results validate the efficiency of the method.

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.