The LMHS MaxSAT solver gained top positions in MaxSAT Evaluation 2015, the primary yearly international competitive event for state-of-the-art constrained optimization solvers for the maximum satisfiability (MaxSAT) optimization paradigm. The solver was ranked first in terms of the total number of benchmarks solved in both the industrial and crafted categories of the weighted partial competition benchmarks among the participating non-portfolio solvers. In total, close to 40 state-of-the-art MaxSAT solvers by research groups from around the world participated in the evaluation.

Due to recent advances in MaxSAT solver technology, the MaxSAT paradigm is finding more and more applications in efficiently solving hard optimization problems as an alternative to other established constrained optimization paradigms such as integer programming. As the most generic well-studied variant of MaxSAT, weighted partial MaxSAT provides a suitable modelling language for many types of Boolean optimization problems.

The LMHS solver applies a hybrid approach based on interatively interacting Boolean satisfiability (SAT) and integer programming solvers. The main developer of the solver is Paul Saikko, who is currently finishing up his MSc thesis on the solver. In addition to Saikko, the other main contributors are Jeremias Berg and Matti Järvisalo from the Constraint Reasoning and Optimization (CoReO) group led by Järvisalo at the Department of Computer Science of the University of Helsinki.

Full results of the MaxSAT Evaluation 2015 are available here.