SAT'22 - BiOptSat

Abstract

We explore a 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 SAT 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

@inproceedings{JabsEtAl2022MaxSATBasedBi,
  author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
  booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing ({SAT} 2022)},
  title = {{MaxSAT}-Based Bi-Objective Boolean Optimization},
  year = {2022},
  editor = {Meel, Kuldeep S. Meel and Strichman, Ofer},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},
  series = {Leibniz International Proceedings in Informatics ({LIPIcs})},
  pages = {12:1--12:23},
  volume = {236},
  doi = {10.4230/LIPIcs.SAT.2022.12},
  isbn = {978-3-95977-242-6},
  issn = {1868-8969},
  url = {https://drops.dagstuhl.de/opus/volltexte/2022/16686},
  urn = {urn:nbn:de:0030-drops-166863},
  annote = {Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT},
}