# DPER: Dynamic Programming for Exist-Random Stochastic SAT

arXiv: https://arxiv.org/abs/2205.09826 · HTML: https://mlsanity.com/paper/2205.09826/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 45 references that are in the map.
- First posted on arXiv 19 May 2022.

## Builds on (most cited first, 7 of 7)

- [Justicia: A Stochastic SAT Approach to Formally Verify Fairness](https://mlsanity.com/paper/2009.06516/) (2020)
- [FAQ: Questions Asked Frequently](https://mlsanity.com/paper/1504.04044/) (2015)
- [Computing Tree Decompositions with FlowCutter: PACE 2017 Submission](https://mlsanity.com/paper/1709.08949/) (2017)
- [Exploiting Database Management Systems and Treewidth for Counting](https://mlsanity.com/paper/2001.04191/) (2020)
- [DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees](https://mlsanity.com/paper/2008.08748/) (2020)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [DPO: Dynamic-Programming Optimization on Hybrid Constraints](https://mlsanity.com/paper/2205.08632/) (2022)

## Abstract (arXiv)

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 operatornameargmaxX sumY 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 sumX maxY 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.