It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

翻译：大量研究表明，通过将软子句集合划分为多个不交子集可以有效求解最大可满足性（Maximum Satisfiability, MaxSAT）问题实例。划分方法可基于子句权重（如分层法）或基于公式的图表示。随后通过合并过程确保找到最优解。本文提出一种名为UpMax的新框架，将划分过程与MaxSAT求解算法解耦。由此，可独立于待使用的MaxSAT算法定义新的划分过程。此外，这种解耦使构建新MaxSAT公式的用户能够基于对待求解问题的认知提出定制化划分方案。我们通过多个问题实例验证该方法的有效性，并证明划分策略对基于不可满足性的MaxSAT算法的性能具有重大影响。