DPO：基于混合约束的动态规划优化

在贝叶斯推断中，最可能解释 (MPE) 问题要求在给定某些证据下求出概率最高的变量实例化。由于贝叶斯网络可编码为字面量加权的 CNF 公式 $\varphi$，我们研究布尔 MPE，这是一个更一般的问题，要求给出 $\varphi$ 的具有最高权重的模型 $\tau$，其中 $\tau$ 的权重为 $\tau$ 所满足的字面量权重之积。已知布尔 MPE 可通过归约到（加权部分）MaxSAT 求解。近期工作提出了 DPMC，一种利用图分解技术构造投影-联结树的动态规划模型计数器。投影-联结树是一种执行计划，规定了如何联结子句并投影掉变量。我们基于 DPMC 引入 DPO，一种精确求解布尔 MPE 的动态规划优化器。通过使用代数决策图 (ADD) 表示伪布尔 (PB) 函数，DPO 能够处理析取子句以及 XOR 子句。（基数约束和 PB 约束也可由 ADD 紧凑表示，因此可进一步扩展 DPO 对混合输入的支持。）为检验 DPO 的竞争力，我们生成随机 XOR-CNF 公式。在这些混合基准上，DPO 显著优于 MaxHS、UWrMaxSat 和 GaussMaxHS，它们是求解 MaxSAT 的当前最优精确求解器。