State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems.
To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced.
We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language.
RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files.
Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API.
Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
@inproceedings{Jabs2025RustsatLibrarySat,title={{RustSAT}: {A} Library For {SAT} Solving in Rust},author={Jabs, Christoph},booktitle={28th International Conference on Theory and Applications of Satisfiability
Testing ({SAT} 2025)},editor={Berg, Jeremias and Nordstr{\"o}m, Jakob},year={2025},volume={341},publisher={Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},series={Leibniz International Proceedings in Informatics ({LIPIcs})},pages={24:1--24:13},doi={10.4230/LIPIcs.SAT.2025.24},eprint={2505.15221},eprinttype={arXiv},}
From Scalable SAT to MaxSAT: Massively Parallel Solution Improving Search
Maximum Satisfiability (MaxSAT) is an essential framework for combinatorial optimization at the core of automated reasoning.
However, to date, no notable parallelizations with convincing scaling behaviour exist.
We suggest to exploit and transfer recent advances in massively parallel SAT solving to perform scalable solution improving search (SIS) for MaxSAT solving.
Building upon the distributed job scheduling and SAT solving platform Mallob, we present the first MaxSAT solver that scales to hundreds of cores through a careful combination of parallel and distributed incremental SAT solving, task parallelism and flexible load balancing, and clause sharing within and across SAT solving tasks.
Experiments on up to 768 cores (16 nodes) show that our approach clearly outscales state-of-the-art SIS-based MaxSAT solvers, marking a new baseline for parallel MaxSAT solving.
Certifying Pareto Optimality in Multi-objective Maximum Satisfiability
In Tools and Algorithms for the Construction and Analysis of Systems
—31st International Conference, TACAS 2025, Held as Part of the
International Joint Conferences on Theory and Practice of Software,
ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part
II, vol. 15697, pp. 108–129, 2025
Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy.
For Boolean satisfiability (SAT) solvers - and more recently SAT-based maximum satisfiability (MaxSAT) solvers - trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed.
In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques.
Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto optimality, without extending the VeriPB format or the proof checker.
By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.
@inproceedings{JabsEtAl2025CertifyingParetoOptimality,author={Jabs, Christoph and Berg, Jeremias and Bogaerts, Bart and Järvisalo, Matti},title={Certifying Pareto Optimality in Multi-objective Maximum Satisfiability},year={2025},booktitle={Tools and Algorithms for the Construction and Analysis of Systems
---31st International Conference, {TACAS} 2025, Held as Part of the
International Joint Conferences on Theory and Practice of Software,
{ETAPS} 2025, Hamilton, ON, Canada, May 3--8, 2025, Proceedings, Part
{II}},editor={Gurfinkel, Arie and Heule, Marijn},pages={108--129},volume={15697},publisher={Springer},series={Lecture Notes in Computer Science},doi={10.1007/978-3-031-90653-4_6},eprinttype={arXiv},}
This paper presents Global Benchmark Database (GBD), a comprehensive suite of tools for provisioning and sustainably maintaining benchmark instances and their metadata.
The availability of benchmark metadata is essential for many tasks in empirical research, e.g., for the data-driven compilation of benchmarks, the domain-specific analysis of runtime experiments, or the instance-specific selection of solvers.
In this paper, we introduce the data model of GBD as well as its interfaces and provide examples of how to interact with them.
We also demonstrate the integration of custom data sources and explain how to extend GBD with additional problem domains, instance formats and feature extractors.
@inproceedings{IserJabs2024GlobalBenchmarkDatabase,author={Iser, Markus and Jabs, Christoph},title={Global Benchmark Database},booktitle={27th International Conference on Theory and Applications of Satisfiability Testing ({SAT} 2024)},year={2024},pages={18:1--18:10},editor={Chakraborty, Supratik and Jiang, Jie-Hong Roland},publisher={Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},address={Dagstuhl, Germany},series={Leibniz International Proceedings in Informatics ({LIPIcs})},isbn={978-3-95977-334-8},issn={1868-8969},volume={305},eprinttype={arXiv},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.18},doi={10.4230/LIPIcs.SAT.2024.18},}
Core Boosting in SAT-Based Multi-objective Optimization
In Integration of Constraint Programming, Artificial Intelligence, and Operations Research—21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28–31, 2024, Proceedings, Part II, vol. 14743, pp. 1–19, 2024
Maximum satisfiability (MaxSAT) constitutes today a successful approach to solving various types of real-world optimization problems through propositional encodings.
Building on this success, various approaches have recently been proposed for finding Pareto-optimal solutions to multi-objective MaxSAT (MO-MaxSAT) instances, i.e., propositional encodings under multiple objective functions.
In this work, we propose core boosting as a reformulation/preprocessing technique for improving the runtime performance of MO-MaxSAT solvers.
Core boosting in the multi-objective setting allows for shrinking the ranges of the multiple objectives at hand, which can be particularly beneficial for MO-MaxSAT relying on search that requires enforcing increasingly tighter objective bounds through propositional encodings.
We show that core boosting is effective in improving the runtime performance of SAT-based MO-MaxSAT solvers with typically little overhead.
@inproceedings{JabsEtAl2024CoreBoostingSAT,author={Jabs, Christoph and Berg, Jeremias and J{\"{a}}rvisalo, Matti},booktitle={Integration of Constraint Programming, Artificial Intelligence, and Operations Research---21st International Conference, {CPAIOR} 2024, Uppsala, Sweden, May 28--31, 2024, Proceedings, Part {II}},title={Core Boosting in SAT-Based Multi-objective Optimization},year={2024},editor={Dilkina, Bistra},publisher={Springer},series={Lecture Notes in Computer Science},pages={1--19},volume={14743},isbn={978-3-031-60599-4},doi={10.1007/978-3-031-60599-4_1},url={https://link.springer.com/chapter/10.1007/978-3-031-60599-4_1},}
From Single-Objective to Bi-Objective Maximum Satisfiability Solving
The declarative approach is key to efficiently finding optimal solutions to various types of NP-hard real-world combinatorial optimization problems.
Most work on practical declarative solvers—ranging from classical integer programming to finite-domain constraint optimization and maximum satisfiability (MaxSAT)—has focused on optimization under a single objective; fewer advances have been made towards efficient declarative techniques for multi-objective optimization problems.
Motivated by significant recent advances in practical solvers for MaxSAT, in this work we develop BiOptSat, an exact declarative approach for finding Pareto-optimal solutions to bi-objective optimization problems, with propositional logic as the underlying constraint language.
BiOptSat can be viewed as an instantiation of the lexicographic method.
The approach makes use of a single Boolean satisfiability solver that is incrementally employed throughout the entire search procedure, allowing for finding a single Pareto-optimal solution, finding one representative solution for each non-dominated point, and enumerating all Pareto-optimal solutions.
We detail several algorithmic instantiations of BiOptSat, each building on recent algorithms proposed for single-objective MaxSAT.
We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective MaxSAT solving on several real-world domains from the literature, showing the practical benefits of our approach.
@article{JabsEtAl2024FromSingleObjective,author={Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J{\"{a}}rvisalo, Matti},title={From Single-Objective to Bi-Objective Maximum Satisfiability Solving},journal={Journal of Artificial Intelligence Research},year={2024},volume={80},month=aug,pages={1223--1269},publisher={AI Access Foundation},url={http://dx.doi.org/10.1613/jair.1.15333},doi={10.1613/jair.1.15333},}
2023
Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization
Building on Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solving algorithms, several approaches to computing Pareto-optimal MaxSAT solutions under multiple objectives have been recently proposed.
However, preprocessing in (Max)SAT-based multi-objective optimization remains so-far unexplored.
Generalizing clause redundancy to the multi-objective setting, we establish provably-correct liftings of MaxSAT preprocessing techniques for multi-objective MaxSAT in terms of computing Pareto-optimal solutions.
We also establish preservation of Pareto-MCSes—the multi-objective lifting of minimal correction sets tightly connected to optimal MaxSAT solutions—as a distinguishing feature between different redundancy notions in the multi-objective setting.
Furthermore, we provide a first empirical evaluation of the effect of preprocessing on instance sizes and multi-objective MaxSAT solvers.
@inproceedings{JabsEtAl2023PreprocessingSATBased,author={Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J{\"{a}}rvisalo, Matti},booktitle={29th International Conference on Principles and Practices of Constraint Programming ({CP} 2023)},title={Preprocessing in {SAT}-Based Multi-Objective Combinatorial Optimization},year={2023},editor={Yap, Roland H. C.},pages={18:1--18:19},publisher={Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},series={Leibniz International Proceedings in Informatics ({LIPIcs})},volume={280},doi={10.4230/LIPIcs.CP.2023.18},annote={Keywords: maximum satisfiability, multi-objective combinatorial optimization, preprocessing, redundancy},}
2022
A Maximum Satisfiability Based Approach to Bi-Objective Boolean Optimization
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)},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},}
2020
A Recurrent Neural Net Approach to Activity Recognition
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},}