License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.26
URN: urn:nbn:de:0030-drops-167006
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16700/
Go to the corresponding LIPIcs Volume Portal

Narodytska, Nina ; Bjørner, Nikolaj

Analysis of Core-Guided MaxSat Using Cores and Correction Sets

pdf-format:
LIPIcs-SAT-2022-26.pdf (2 MB)

Abstract

Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers (MaxHS) extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates. In this work we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate that a set of MUSes that a core-guided algorithm discovers possess the same key properties as cores extracted by MaxHS solvers. For instance, we prove the size of a minimum hitting set of these cores equals the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.

BibTeX - Entry

@InProceedings{narodytska_et_al:LIPIcs.SAT.2022.26,
  author =	{Narodytska, Nina and Bj{\o}rner, Nikolaj},
  title =	{{Analysis of Core-Guided MaxSat Using Cores and Correction Sets}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16700},
  URN =		{urn:nbn:de:0030-drops-167006},
  doi =		{10.4230/LIPIcs.SAT.2022.26},
  annote =	{Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}

Keywords: maximum satisfiability, unsatisfiable cores, correction sets
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI