Software

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 structure.png

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-boudning) 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.

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.

SAT-based approach to computing treewidth [2] Cactus

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 package (developed by me) can be downloaded from here. To the best of my understanding, the Jdrasil java library also includes an (probably more user friendly) implementation of the same idea.

MaxPRE – an extended MaxSAT preprocessor [3]

maxpre_0

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.
MaxPRE is mainly developed by Tuukka Korhonen, The source code can be downloaded from here.

Triangulator – Minimal triangulations via Potential Maximal Cliques [4]

pace2017-award

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.

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.