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.

翻译：受近期加权模型计数中动态规划方法进展的启发，我们针对布尔可实现性与综合问题提出一种动态规划方法。该方法以基于输入/输出变量的合取范式布尔公式为对象，旨在依据输入变量为输出变量综合见证函数。我们展示了如何通过树分解获得的分级投影-连接树，以自底向上的顺序计算表示输入公式可实现性集合的BDD。随后阐明如何在可实现性检测阶段生成的中间BDD基础上，以自顶向下的方式实现见证函数的综合。基于上述思想实现的求解器DPSynth的实验评估表明：与采用相同符号表示的启发式方法相比，我们的布尔可实现性与综合方法在时间和空间性能上均具有显著优势。本文进一步讨论了新方法在可扩展性方面的优势，并分析了动态规划框架性能的相关发现。