software | Jeremias Berg

Berg, J., Demirovic, E., & Stuckey, P. J. (2019). Core-Boosted Linear Search for Incomplete MaxSAT. In L.-M. Rousseau & K. Stergiou (Eds.), Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings (Vol. 11494, pp. 39–56). Springer. https://doi.org/10.1007/978-3-030-19212-9_3

Loandra - Core-Boosted Linear Search

Loandra is an any-time MaxsAT solver that implements the so called core-boosted search algorithm that we developed during my visit to Melbourne in 2018. Core-boosted search is a two stage search strategy that starts of in a core-guided (lower bounding) phase and then switches to a linear (upper bounding) phase. Loandra performed very well in the 2019 MaxSAT Evaluation, placing first and second in the unweighted and weighted incomplete tracks, respectively. The algorithmic ideas underlying Loandra have also been implemented in pseudo-Boolean optimization, and constraint programming.

In 2021 Loandra with added preprocessing again did very well, taking first in the weighted 300s category and 4th in all others.

Loandra is mainly developed by me, the source code can be found on github. Loandra owns much of its existence to the developers of Open WBO. I’d like to thank them for their hard work.

code Cite

Berg, J., Bacchus, F., & Poole, A. (2020). Abstract Cores in Implicit Hitting Set MaxSat Solving. In L. Pulina & M. Seidl (Eds.), Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings (Vol. 12178, pp. 277–294). Springer. https://doi.org/10.1007/978-3-030-51825-7_20

Abstract Cores - in Implicit Hitting Set-based MaxSAT

During my visit to Toronto in 2019. We worked on extending the implicit hitting set (IHS) algorithm for MaxSAT with abstract cores. Abstract cores which can be seen as a hybridization between core-guided and hitting set-based algorithms, as well as symmetry breaking. The work was recognized with a paper award at the 2020 SAT conferece, the flagship conference of the research field of Boolean satisfiability.

We show how adding abstract cores into the MaxSAT solver MaxHS significantly improves its performance. The solver took top positions in the 2020 and 2021 MaxSAT Evaluations. More recently, we have shown how abstract cores can be used as a basis for a framework that unifies most of the existing SAT-based MaxSAT algorithms.

MaxHS is available [on the MaxSAT Evaluaitons webpage]https://maxsat-evaluations.github.io/2020/mse20-solver-src/complete/MaxHS.zip).

code Cite

Korhonen, T., Berg, J., Saikko, P., & Järvisalo, M. (2017). MaxPre: An Extended MaxSAT Preprocessor. In S. Gaspers & T. Walsh (Eds.), Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings (Vol. 10491, pp. 449–456). Springer. https://doi.org/10.1007/978-3-319-66263-3_28

MaxPre - Preprocessing for Maximum Satisfiability

MaxPRE is a preprocessor capable of simplifying single-, and multiobjective MaxSAT instances in a cost-preserving manner. MaxPre imnplements a wide-range of different simplification rules, including MaxSAT-liftings of preprocessing rules commonly used in SAT solving (BVE, SE; SCE, BVA etc.) as well as MaxSAT-specific preprocessing rules that we have developed in our group.

MaxPre implements a multitude of the algorithmic techniques proposed by me during my PhD research and after it. MaxPre can be used either as stand-alone, or through an API that allows tight integration with your solver. The first version of MaxPRE was developed by Tuukka Korhonen, The source code of that version is available in open-source on github.

The second version of MaxPRE, dubbed MaxPre 2.0 is currently developed by Hannes Ihalainen. It is available in open-source on bitbucket. Compared to the first version, MaxPre 2.0 includes a number of quality of life improvements and extended reasoning techniques.

code Cite

Smirnov, P., Berg, J., & Järvisalo, M. (2022). Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. In K. S. Meel & O. Strichman (Eds.), 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Vol. 236, pp. 13:1–13:18). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2022.13

PBO-IHS - Pseudo-Boolean Optimization via Implicit Hitting Sets

PBO-IHS is an implementation of the implicit hitting set approach to pseudo-Boolean optimization. PBO-IHS uses the conflict-driven pseudo-Boolean solver RoundingSAT as a core-extractor and the CPLEX mixed-integer programming solver as a hitting-set solver. We have shown that PBO-IHS achieves orthogonal performance compared to other state-of-the-art PBO-solvers and currently represents one of the best performing approaches to PBO.

PBO-IHS was developed by Pavel Smirnov. It is available in open source (as long as you supply your own MIP solver) on bitbucket

code Cite

Jabs, C., Berg, J., Niskanen, A., & Järvisalo, M. (2022). MaxSAT-Based Bi-Objective Boolean Optimization. In K. S. Meel & O. Strichman (Eds.), 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Vol. 236, pp. 12:1–12:23). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2022.12

Scuttle & BiOptSAT - Multi-Objective MaxSAT

Scuttle and BiOptSAT are two solvers for multiobjective MaxSAT developed in out group. Both solvers compute the so-called pareto-optimal solutions of multiopbjective MaxSAT isntances. BiOptSAT is an efficient implementation of the so-called lexicographic method for bi-objective problems, first proposed for MaxSAT by our group. Scuttle implements a number of other algorithms first proposed by other groups, including the so called P-minimal algorithm, and a lower-bounding core-guided algorithm.

Both solvers have been mainly developed by my PhD student Christoph Jabs who wrote his M.Sc. thesis on BiOptSAT.

code Cite

Niskanen, A., Berg, J., & Järvisalo, M. (2022). Incremental Maximum Satisfiability. In K. S. Meel & O. Strichman (Eds.), 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Vol. 236, pp. 14:1–14:19). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2022.14

IMaxHS - Incremental Optimization with Hitting Sets

IMaxHS is an incremental version of the MaxHS solver that implements the implicit hitting set approach to MaxSAT. IMaxHS is tailored toward applications that require solving a sequence of optimization problems. By maintaining its internal state we demonstrate that IMaxHS can e.g. learn interpretable classifiers much more efifciently compared to the naive approach of restaring search from scratch on each iteration.

iMaxHS is primarly developed by Andreas Niskanen.

code Cite

Ihalainen, H., Berg, J., & Järvisalo, M. (2021). Refined Core Relaxation for Core-Guided MaxSAT Solving. In L. D. Michel (Ed.), 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021 (Vol. 210, pp. 28:1–28:19). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.CP.2021.28

CGSS - A Core-Guided MaxSAT solver

CGSS is an effective implementation of the OLL algorithm for MaxSAT. The first version of CGSS was built on top of the RC2 MaxSAT solver in Python. The current–and much more effective–version is a reimplementation from scratch in C++. Most notably, CGSS extends RC2 with the so called structure sharing (SS) technique that results in more compact encodings of the constraints required for optimization. More details can be found in (Ihalainen et al., 2021).

CGSS is developed by my PhD student Hannes Ihalainen who wrote his M.Sc. thesis on it. The implementation is available in open source on bitbucket. The first (Python) version of CGSS was further extended with proof logging in 2023 by Andy Oertel. The source code of the proof-logging version can be found on gitlab

code Cite

Triangulator - Potential Maximal Cliques for Graph Parameters

Triangulator is an implementation of the Bouchitté-Todinca algorithm for finding minimal graph triangulations that are optimal with respect to different cost function. The approach can be used to solve many different graph-related problems. More precisely, Triangulator can be used for computing the treewidth and minimum fill-in of a graph, the generalized hypertreewidth and fractional hypertreewidth of a hypergraph or the total table size of a Bayesian network. Triangulator placed second in the minimum-fill in track of the 2017 PACE challenge.

Triangulator is developed by Tuukka Korhonen. It is available in open-source on GitHub.