DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2023.19

UpMax: User Partitioning for MaxSAT

Authors: Pedro Orvalho, Vasco Manquinho, and Ruben Martins

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract

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.

Cite as

Pedro Orvalho, Vasco Manquinho, and Ruben Martins. UpMax: User Partitioning for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{orvalho_et_al:LIPIcs.SAT.2023.19,
  author =	{Orvalho, Pedro and Manquinho, Vasco and Martins, Ruben},
  title =	{{UpMax: User Partitioning for MaxSAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{19:1--19:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.19},
  URN =		{urn:nbn:de:0030-drops-184819},
  doi =		{10.4230/LIPIcs.SAT.2023.19},
  annote =	{Keywords: Maximum Satisfiability, Formula partitioning, Graph-based methods}
}

Search Results

Documents authored by Orvalho, Pedro

UpMax: User Partitioning for MaxSAT

Abstract

Cite as

Thanks for your feedback!

Could not send message