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 both the DQBF and DSSAT problems. 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 of benchmark problems using a prototype DQMax\#SAT solver implementation.

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