Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Jabs, Christoph; Berg, Jeremias; Niskanen, Andreas; Järvisalo, Matti https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-166863
URL:

; ; ;

MaxSAT-Based Bi-Objective Boolean Optimization

pdf-format:


Abstract

We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.

BibTeX - Entry

@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12,
  author =	{Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
  title =	{{MaxSAT-Based Bi-Objective Boolean Optimization}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{12:1--12:23},
  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/16686},
  URN =		{urn:nbn:de:0030-drops-166863},
  doi =		{10.4230/LIPIcs.SAT.2022.12},
  annote =	{Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT}
}

Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT
Seminar: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Source Code and Data): https://bitbucket.org/coreo-group/bioptsat archived at: https://archive.softwareheritage.org/swh:1:dir:3bb8b3ab49f2c36cfeb99211ccd60ac0f8b9bb15


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