# UpMax: User partitioning for MaxSAT

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 54 references that are in the map.
- First posted on arXiv 25 May 2023.

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

- [Incremental Cardinality Constraints for MaxSAT](https://mlsanity.com/paper/1408.4628/) (2014)
- [Exploiting Resolution-based Representations for MaxSAT Solving](https://mlsanity.com/paper/1505.02405/) (2015)

## Abstract (arXiv)

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.