Given a boolean formula $\Phi$(X, Y, Z), the Max\#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of variables Y. We investigate a strict generalization of Max\#SAT allowing dependencies for variables in X, effectively turning it into a synthesis problem. We show that this new problem, called DQMax\#SAT, subsumes the DQBF problem as well. We provide a general resolution method, based on a reduction to Max\#SAT, together with two improvements for dealing with its inherent complexity. We further discuss a concrete application of DQMax\#SAT for symbolic synthesis of adaptive attackers in the field of program security. Finally, we report preliminary results obtained on the resolution on benchmark problems using a prototype DQMax\#SAT solver implementation.

翻译：给定一个布尔公式 $\Phi$(X, Y, Z)，Max\#SAT 问题旨在寻找变量集 X 上的一个部分模型，使得其在变量集 Y 上的投影模型数量最大化。我们研究了 Max\#SAT 的一种严格泛化形式，该形式允许变量 X 之间存在依赖关系，从而将其转化为一个合成问题。我们证明了这个新问题（称为 DQMax\#SAT）同时也包含了 DQBF 问题。我们提出了一种通用的求解方法，该方法基于到 Max\#SAT 的归约，并附带了两项用于处理其固有复杂性的改进措施。我们还讨论了 DQMax\#SAT 在程序安全领域中自适应攻击者的符号合成方面的具体应用。最后，我们报告了使用原型 DQMax\#SAT 求解器实现，对基准问题进行求解所获得的初步结果。