The Loandra MaxSAT solver authored by Jeremias Berg of the Constraint Reasoning and Optimization group is the best incomplete solver on unweighted instances in the international MaxSAT Evaluation 2019. Further, Loandra reached second place in the incomplete weighted track among nine solvers participating in the competition.
Loandra is based on ideas co-authored by Berg together with Emir Demirović and Peter Stuckey (University of Melbourne, Australia). In particular, Loandra implements core-boosted linear search, a two stage search strategy for incomplete MaxSAT solving. Initially the search starts in a core-guided (lower bounding) phase. If the first phase is unable to find an optimal solution the search switches to a linear (upper bounding) phase. The linear phase runs until either finding an optimal solution, or running out time, at which point the currently best known solution is returned.
The MaxSAT Evaluations focus as the main international yearly evaluation event in the research area on the evaluation of the current state-of-the-art in open-source solver implementations for the Boolean optimization paradigm of Maximum satisfiability (MaxSAT). The main goals of the MaxSAT Evaluation series are to assess the state of the art in the field of MaxSAT solvers, to collect and re-distribute a heterogeneous MaxSAT benchmark set for further scientific evaluations, and to promote MaxSAT as a viable option for solving instances of a wide range of NP-hard optimization problems.