DPO: Dynamic-Programming Optimization on Hybrid Constraints

TL;DR

This paper introduces DPO, a dynamic programming approach using algebraic decision diagrams to efficiently solve Boolean MPE problems, especially on hybrid constraints, outperforming existing MaxSAT solvers.

Contribution

DPO extends DPMC by incorporating ADDs to handle disjunctive and XOR clauses, enabling exact solutions for hybrid Boolean MPE problems.

Findings

DPO significantly outperforms state-of-the-art MaxSAT solvers on hybrid benchmarks.

DPO effectively handles disjunctive, XOR, and PB constraints using ADDs.

The approach demonstrates scalability and efficiency in solving complex Bayesian inference problems.

Abstract

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 $\tau$ of $\varphi$ with the highest weight, where the weight of $\tau$ is the product of weights of literals satisfied by $\tau$. 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.