References & Citations
Computer Science > Formal Languages and Automata Theory
Title: Dynamic Programming for Symbolic Boolean Realizability and Synthesis
(Submitted on 13 May 2024 (v1), last revised 27 May 2024 (this version, v3))
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.
Submission history
From: Yi Lin [view email][v1] Mon, 13 May 2024 17:48:45 GMT (3696kb,D)
[v2] Mon, 20 May 2024 16:40:35 GMT (3696kb,D)
[v3] Mon, 27 May 2024 15:53:12 GMT (3696kb,D)
Link back to: arXiv, form interface, contact.