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.
@mastersthesis{Jabs2022MaximumSatisfiabilityBased,
author = {Jabs, Christoph},
school = {University of Helsinki},
title = {A Maximum Satisfiability Based Approach to Bi-Objective Boolean Optimization},
year = {2022},
url = {http://urn.fi/URN:NBN:fi:hulib-202206132323},
thesis_type = {M. Sc. thesis},
latex_src = {https://github.com/chrjabs/masters-thesis},
}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.
@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), Haifa, Israel, August 2--5, 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},
}A common approach in current research publication on analysing multimodal time-series data from inertial sensors is to use Convolutional Neural Networks (CNNs) to automatically learn patterns in the given data. The disadvantage when using CNNs in such an application on mobile devices is that they are highly computationally complex. Therefore, this thesis studies the question if Long-Short-Term-Memory (LSTM) networks, which are significantly less computationally complex, can be used as an alternative for such applications. Firstly the topic of Human Activity Recognition (HAR) and the used datasets Opportunity and mHealth are presented. Following that, inertial sensors and their functional principles are briefly touched on. In the main part of the work, the methods used, mainly LSTMs and CNNs are laid out. In our experiments, we mainly present an architecture study in which 380 LSTM variants were trained and tested on the Opportunity dataset. A modified training process called Relaxed Truth Training that speeds up the training process slightly is also presented and tested in our experiments. When comparing the best two LSTM networks from the architecture study to two different CNN architectures, we found superior performance from the LSTMs, mainly when looking at close to real life, continuous classification problems. These results were verified by testing the same architectures on the mHealth dataset.
@mastersthesis{Jabs2020RecurrentNeuralNet,
author = {Jabs, Christoph},
school = {Reutlingen University},
title = {A Recurrent Neural Net Approach to Activity Recognition},
year = {2020},
thesis_type = {B. Eng. thesis},
}