Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning. Existing methods for MaxSAT have been successful in solving benchmarks in CNF format. They lack, however, the ability to handle 1) (non-CNF) hybrid constraints, such as XORs and 2) generalized MaxSAT problems natively. To address this issue, we propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints -- called \emph{Dynamic-Programming-MaxSAT} or DPMS for short -- based on Algebraic Decision Diagrams (ADDs). With the power of ADDs and the (graded) project-join-tree builder, our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints. Moreover, DPMS scales provably well on instances with low width. Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail. Hence, DPMS is a promising framework and opens a new line of research that invites more investigation in the future.

翻译：布尔MaxSAT及其广义形式（如Min-MaxSAT和Max-hybrid-SAT）是布尔推理中的基本优化问题。现有的MaxSAT方法在解决CNF格式的基准测试中取得了成功，但它们缺乏处理1）非CNF混合约束（如XOR）以及2）广义MaxSAT问题的原生能力。为解决这一问题，我们提出了一种基于代数决策图（ADD）的新型动态规划方法——称为Dynamic-Programming-MaxSAT（简称DPMS）——用于求解具有混合约束的广义MaxSAT问题。借助ADD的能力和（分级）投影连接树构建器，我们的通用框架支持CNF-MaxSAT的多种推广形式，例如具有混合约束的MaxSAT、Min-MaxSAT和MinSAT。此外，DPMS在低宽度实例上具有良好的理论可扩展性。实验结果表明，DPMS能够快速解决某些其他基于不同技术的算法均无法处理的问题。因此，DPMS是一个具有前景的框架，为未来需要进一步探索的研究开辟了新方向。