On this page you can find the software that I have been most involved with contributing to. The CoReO homepage contains more software that has been developed in my current group.

Loandra – Core-boosted linear search for incomplete MaxSAT [1]

Loandra is an implementation of core-boosted search for incomplete MaxSAT. 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. More details can be found in this paper. Loandra performed very well in the 2019 MaxSAT Evaluation, placing first and second in the unweighted and weighted incomplete tracks, respectively.

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.

Abstract Cores in IHS-based MaxSAT solving [7,8]

During my visit to professor Fahiem Bacchus the university of Toronto we worked on an extension of the so called implicit hitting set approach to MaxSAT. The results of the work are summarised in the 2020 SAT paper [8] that won the best paper award of the conference. The potential of abstract cores was further demonstrated by the state-of-the-art IHS solver MaxHS [7] extended with abstract cores taking top positions in the MaxSAT evaluations of 2019 and 2020.

An older version of MaxHS can be found here. The newest version, with the abstract cores, can be downloaded from the evaluation webpage. I’d like to thank professor Bacchus for his work on the solver.

INC-IHS – An incremental version of MaxHS that suports changing weights [5]

We implemented a version of the implicit hitting set based approach to MaxSAT solving that supports changing weights between iterations while maintaining its internal state. In the paper, we demonstrate how maintaining the state greatly improves empirical performance on two applications from the domain of learning interpretable classifiers.

INC-IHS is mainly developed by Andreas Niskanen and can be found at:
https://bitbucket.org/coreo-group/incremental-maxhs/

CGSS – Improved Core Relaxations on top of RC2 [6] 

We investigated an improvement to the standard way in which so called Core-Guided MaxSAT solvers relax unsatisfiable cores during search. The new technique is based on the insight that, on weighted instances, the cores extracted might overlap, which in turn allows for more compact encodings for relaxing them. The resulting technique is dubbed structure sharing. In the paper, we demonstrate how structure sharing improves the performance of RC2, a state-of-the-art implementation of the core-guided OLL algorithm for MaxSAT.

CGSS was developed by Hannes Ihalainen, the implementation can be found at:
https://bitbucket.org/coreo-group/cgss/

PBO-IHS – An implicit hitting set approach to pseudo Boolean optimisation [9]

In CP 2021 we presented a first implementation of the so called implicit hitting set-based approach to pseudo Boolean Optimisation. In addition to proposing the basic framework, the solver also generalises many of the refinements that have previously been proposed for MaxSAT. In the future, we aim to further develop this with PB specific techniques.

PBO-IHS was mainly developed by Pavel Smirnov. It can be found on bitbucket.

SAT-based approach to computing treewidth [2]

The package includes code to reproduce the SAT-based approach approach for computing treewidth described in this paper. More precisely, the package includes a Haskell script that converts a graph in .dgf format (the package also includes examples of this format) to a .wcnf file, i.e. a MaxSAT instance whose optimal cost is equal to the treewidth of the graph. The .wcnf file can then be input to any MaxSAT solver in order to reproduce the MaxSAT approach described in [2]. Alternatively, the .wcnf files can be given to the modified version of MiniSAT (also included in the package) in order to reproduce the Iterative SAT approaches of the paper.

The Jdrasil java library includes an (probably more user friendly) implementation of the idea.

MaxPRE – an extended MaxSAT preprocessor [3]

MaxPRE is a preprocessor for weighted partial MaxSAT. It offers an efficient lifting of several SAT-based preprocessing techniques for MaxSAT as well as implementations of a few MaxSAT specific techniques developed in our group.

See references for technical details). The tool can be used as stand-alone, it can either output the preprocessed instance to a separate file, or  use a given solver binary to solve the preprocessed instance and reconstruct a model to the original one. Finally MaxPRE also offer an API which can be used to integrate it directly with another solver.
The first version of MaxPRE was developed by Tuukka Korhonen, The source code can be downloaded from here.

The second version of MaxPRE, dubbed MaxPre 2.0 is developed by Hannes Ihalainen. It can be downloaded from bitbucket. Compared to the first version, MaxPre 2.0 includes a number of quality of life changes and a number of extended reasoning techniques.

Triangulator – Minimal triangulations via potential maximal cliques [4]

Triangulator is an implementation of the Bouchitté-Todinca algorithm for finding minimal graph triangulations that are optimal w.r.t. some given cost function. The approach can be used to solve many different graph-related problems, 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 mainly developed by Tuukka Korhonen, its source code can be found on Github.

MaxSAT benchmarks

In addition to software, my research has resulted in various MaxSAT benchmarks that are available to the community via the MaxSAT evaluations and MaxSAT LIB.

I have submitted benchmarks related to:

• Correlation clustering and the 2017 AIJ paper,

• Bayesian network structure learning and the 2014 AISTATS paper,

• Minimum-width confidence bands and the 2017 CP paper

• Computing (generalized) tree-width and the ICTAI paper from 2014 and

• Minimum-fill in and the JEA paper from 2019.

References:

[1] Berg J., Demirović E. and Stuckey P.J., 2019, June. Core-Boosted Linear Search for Incomplete MaxSAT. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research(pp. 39-56). Springer, Cham.

[2] Berg J. and Järvisalo M., 2014, November. SAT-based approaches to treewidth computation: An evaluation. In 2014 IEEE 26th International Conference on Tools with Artificial Intelligence (pp. 328-335). IEEE.

[3] Korhonen T., Berg J., Saikko P. and Järvisalo M., 2017, August. MaxPre: an extended MaxSAT preprocessor. In International Conference on Theory and Applications of Satisfiability Testing (pp. 449-456). Springer, Cham.

[4] Korhonen T., Berg J. and Järvisalo M., 2019. Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitté–Todinca Algorithm. Journal of Experimental Algorithmics (JEA), 24(1), pp.1-9.

[5] Niskanen A., Berg J., and Järvisalo M.. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT under Changing Weights. In International Conference on Principles and Practice of Constraint Programming LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. (pp. 44:1–44:19)

[6] Ihalainen H., Berg J., and Järvisalo M.. Refined Core Relaxation for Core-Guided MaxSAT Solving. In International Conference on Principles and Practice of Constraint Programming LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. (pp. 28:1–28:19)

[7] Davies, J. and Bacchus, F., 2013, July. Exploiting the power of MIP solvers in MAXSAT. In International conference on theory and applications of satisfiability testing (pp. 166-181). Springer, Berlin, Heidelberg.

[8] Berg, J., Bacchus, F. and Poole, A., 2020, July. Abstract Cores in Implicit Hitting Set MaxSat Solving. In International Conference on Theory and Applications of Satisfiability Testing (pp. 277-294). Springer, Cham.

[9] Smirnov, P., Berg, J. and Järvisalo, M., 2021. Pseudo-Boolean Optimization by Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. (pp. 51:1–51:20)