Author name cluster

Christoph Jabs

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

SAT Conference 2025 Conference Paper

RustSAT: A Library for SAT Solving in Rust

Christoph Jabs

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.

Details

JAIR Journal 2024 Journal Article

From Single-Objective to Bi-Objective Maximum Satisfiability Solving

Christoph Jabs
Jeremias Berg
Andreas Niskanen
Matti Järvisalo

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.

PDF Details DOI

SAT Conference 2024 Conference Paper

Global Benchmark Database

Ashlin Iser
Christoph Jabs

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.

Details

SAT Conference 2022 Conference Paper

MaxSAT-Based Bi-Objective Boolean Optimization

Christoph Jabs
Jeremias Berg
Andreas Niskanen
Matti Järvisalo

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.

Details