DROPS

Document

Interactions in Constraint Optimization (Dagstuhl Seminar 25371)

Authors: Katalin Fazekas, Matti Järvisalo, Nina Narodytska, Peter J. Stuckey, and Christoph Jabs

Published in: Dagstuhl Reports, Volume 15, Issue 9 (2026)

Abstract

This report documents the Dagstuhl Seminar 25371 "Interactions in Constraint Optimization". Our Dagstuhl Seminar gathered 41 researchers from 15 countries, working on different constraint optimization paradigms. The report consists of an executive summary, and abstracts on tutorials, research talks, and panel discussions.

Cite as

Katalin Fazekas, Matti Järvisalo, Nina Narodytska, Peter J. Stuckey, and Christoph Jabs. Interactions in Constraint Optimization (Dagstuhl Seminar 25371). In Dagstuhl Reports, Volume 15, Issue 9, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{fazekas_et_al:DagRep.15.9.1,
  author =	{Fazekas, Katalin and J\"{a}rvisalo, Matti and Narodytska, Nina and Stuckey, Peter J. and Jabs, Christoph},
  title =	{{Interactions in Constraint Optimization (Dagstuhl Seminar 25371)}},
  pages =	{1--20},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{9},
  editor =	{Fazekas, Katalin and J\"{a}rvisalo, Matti and Narodytska, Nina and Stuckey, Peter J. and Jabs, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.9.1},
  URN =		{urn:nbn:de:0030-drops-249811},
  doi =		{10.4230/DagRep.15.9.1},
  annote =	{Keywords: constraint programming, maximum satisfiability, mixed integer linear programming, optimization modulo theories, pseudo-boolean optimization}
}

Document

DOI: 10.4230/LIPIcs.SAT.2022.26

Analysis of Core-Guided MaxSat Using Cores and Correction Sets

Authors: Nina Narodytska and Nikolaj Bjørner

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.

Cite as

Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSat Using Cores and Correction Sets. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2022.26},
  URN =		{urn:nbn:de:0030-drops-167006},
  doi =		{10.4230/LIPIcs.SAT.2022.26},
  annote =	{Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}

Search Results

Documents authored by Narodytska, Nina

Interactions in Constraint Optimization (Dagstuhl Seminar 25371)

Abstract

Cite as

Analysis of Core-Guided MaxSat Using Cores and Correction Sets

Abstract

Cite as

Thanks for your feedback!

Could not send message