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——的实验评估表明，我们针对布尔可实现性与综合的方法，在使用相同符号表示的情况下，在时间和空间性能上均优于基于启发式的方法。我们讨论了新方法在可扩展性方面的优势，并研究了我们对DP框架性能的发现。