# DPO: Dynamic-Programming Optimization on Hybrid Constraints

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 48 references that are in the map.
- First posted on arXiv 17 May 2022.

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

- [FAQ: Questions Asked Frequently](https://mlsanity.com/paper/1504.04044/) (2015)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [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)

## Built on by (most cited first, 1 of 1)

- [DPER: Dynamic Programming for Exist-Random Stochastic SAT](https://mlsanity.com/paper/2205.09826/) (2022)

## Abstract (arXiv)

In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literal-weighted CNF formula varphi, we study Boolean MPE, a more general problem that requests a model τ of varphi with the highest weight, where the weight of τ is the product of weights of literals satisfied by τ. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. Recent work proposed DPMC, a dynamic-programming model counter that leverages graph-decomposition techniques to construct project-join trees. A project-join tree is an execution plan that specifies how to conjoin clauses and project out variables. We build on DPMC and introduce DPO, a dynamic-programming optimizer that exactly solves Boolean MPE. By using algebraic decision diagrams (ADDs) to represent pseudo-Boolean (PB) functions, DPO is able to handle disjunctive clauses as well as XOR clauses. (Cardinality constraints and PB constraints may also be compactly represented by ADDs, so one can further extend DPO's support for hybrid inputs.) To test the competitiveness of DPO, we generate random XOR-CNF formulas. On these hybrid benchmarks, DPO significantly outperforms MaxHS, UWrMaxSat, and GaussMaxHS, which are state-of-the-art exact solvers for MaxSAT.