论文标题
DPER：ANTAMOM随机SAT的动态编程
DPER: Dynamic Programming for Exist-Random Stochastic SAT
论文作者
论文摘要
在贝叶斯推断中，最大后验（MAP）问题结合了最可能的解释（MPE）和边缘化（MAR）问题。命题逻辑中的对应物是现有的随机性满足性（ER-SSAT）问题，它结合了满意度（SAT）和加权模型计数（WMC）问题。 MAP和ER-SSAT都具有$ \ operatatorName {argmax} _x \ sum_y f（x，y）$的表单，其中$ f $是差异集$ x $和$ y $变量的真实功能。这两个优化问题要求对$ x $变量的价值分配，该变量最大化$ f（x，y）$的加权总和比$ y $变量的所有值分配。 ER-SSAT已被证明是正式验证监督学习中公平性的一种有前途的方法。最近，已经提出了对分级项目加入树的动态编程来解决加权的投影模型计数（WPMC），这是一个相关问题，具有$ \ sum_x \ max_y f（x，y）$的形式。我们将此WPMC框架扩展到精确求解ER-SSAT并实现一个名为DPER的动态编程求解器。我们的经验评估表明，DPE通过在低宽度问题实例上竞争性能，有助于最先进的ER-SSAT求解器（DC-SSAT和ERSSAT）的投资组合。
In Bayesian inference, the maximum a posteriori (MAP) problem combines the most probable explanation (MPE) and marginalization (MAR) problems. The counterpart in propositional logic is the exist-random stochastic satisfiability (ER-SSAT) problem, which combines the satisfiability (SAT) and weighted model counting (WMC) problems. Both MAP and ER-SSAT have the form $\operatorname{argmax}_X \sum_Y f(X, Y)$, where $f$ is a real-valued function over disjoint sets $X$ and $Y$ of variables. These two optimization problems request a value assignment for the $X$ variables that maximizes the weighted sum of $f(X, Y)$ over all value assignments for the $Y$ variables. ER-SSAT has been shown to be a promising approach to formally verify fairness in supervised learning. Recently, dynamic programming on graded project-join trees has been proposed to solve weighted projected model counting (WPMC), a related problem that has the form $\sum_X \max_Y f(X, Y)$. We extend this WPMC framework to exactly solve ER-SSAT and implement a dynamic-programming solver named DPER. Our empirical evaluation indicates that DPER contributes to the portfolio of state-of-the-art ER-SSAT solvers (DC-SSAT and erSSAT) through competitive performance on low-width problem instances.
