A Maximum Satisfiability Based Approach to Bi-Objective Boolean Optimization

Visa fullständig post



Permalänk

http://urn.fi/URN:NBN:fi:hulib-202206132323
Titel: A Maximum Satisfiability Based Approach to Bi-Objective Boolean Optimization
Författare: Jabs, Christoph
Medarbetare: Helsingin yliopisto, Matemaattis-luonnontieteellinen tiedekunta
University of Helsinki, Faculty of Science
Helsingfors universitet, Matematisk-naturvetenskapliga fakulteten
Utgivare: Helsingin yliopisto
Datum: 2022
Språk: eng
Permanenta länken (URI): http://urn.fi/URN:NBN:fi:hulib-202206132323
http://hdl.handle.net/10138/344612
Nivå: pro gradu-avhandlingar
Utbildningsprogram: Tietojenkäsittelytieteen maisteriohjelma
Master's Programme in Computer Science
Magisterprogrammet i datavetenskap
Studieinriktning: Algoritmit
Algorithms
Algoritmer
Abstrakt: Many real-world problem settings give rise to NP-hard combinatorial optimization problems. This results in a need for non-trivial algorithmic approaches for finding optimal solutions to such problems. Many such approaches—ranging from probabilistic and meta-heuristic algorithms to declarative programming—have been presented for optimization problems with a single objective. Less work has been done on approaches for optimization problems with multiple objectives. We present BiOptSat, an exact declarative approach for finding so-called Pareto-optimal solutions to bi-objective optimization problems. A bi-objective optimization problem arises for example when learning interpretable classifiers and the size, as well as the classification error of the classifier should be taken into account as objectives. Using propositional logic as a declarative programming language, we seek to extend the progress and success in maximum satisfiability (MaxSAT) solving to two objectives. BiOptSat can be viewed as an instantiation of the lexicographic method and makes use of a single SAT solver that is preserved throughout the entire search procedure. It allows for solving three tasks for bi-objective optimization: finding a single Pareto-optimal solution, finding one representative solution for each Pareto point, and enumerating all Pareto-optimal solutions. We provide an open-source implementation of five variants of BiOptSat, building on different algorithms proposed for MaxSAT. Additionally, we empirically evaluate these five variants, comparing their runtime performance to that of three key competing algorithmic approaches. The empirical comparison in the contexts of learning interpretable decision rules and bi-objective set covering shows practical benefits of our approach. Furthermore, for the best-performing variant of BiOptSat, we study the effects of proposed refinements to determine their effectiveness.
Subject: Bi-objective optimization
MaxSAT
incremental SAT
interpretable classifiers
bi-objective set covering


Filer under denna titel

Totalt antal nerladdningar: Laddar...

Filer Storlek Format Granska
Jabs_Christoph_thesis_2022.pdf 1.435Mb PDF Granska/Öppna

Detta dokument registreras i samling:

Visa fullständig post