LMHS

A SAT-IP Hybrid MaxSAT solver

About

LMHS [1] is a from-scratch MaxSAT solver implementation based on the implicit hitting set approach [2,3] using interacting SAT and IP solvers, as first implemented in the MaxHS solver [4]. LMHS is developed by the Constraint Optimization and Reasoning Group at the Department of Computer Science, University of Helsinki. The system is implemented by Paul Saikko. LMHS ranked number-1 among non-portfolio solvers with respect to the number of instances solved in the industrial and crafted weighted partial categories of MaxSAT Evaluation 2015.

Features

LMHS currently

  • supports the standard WCNF input format, including weighted partial;
  • supports real-valued weights on soft clauses;
  • offers an incremental API;
  • enables applying SAT-based preprocessing in a tightly-coupled manner [5];
  • supports MiniSAT and Lingeling as the SAT solver, and CPLEX and SCIP as the IP solver.

Downloads

LMHS is available in open source under the MIT license at GitHub.

References

[1] Paul Saikko, Jeremias Berg, Matti Järvisalo: LMHS: A SAT-IP Hybrid MaxSAT Solver. SAT 2016: 539-546

[2] Erick Moreno-Centeno and Richard M. Karp: The implicit hitting set approach to solve combinatorial optimization problems with an application to multi-genome alignment. Operations Research 61(2) 2013, 453-468.

[3] Paul Saikko, Johannes Peter Wallner, Matti Järvisalo: Implicit Hitting Set Algorithms for Reasoning Beyond NP. KR 2016: 104-113

[4] Jessica Davies, Fahiem Bacchus: Exploiting the Power of MIP Solvers in MaxSAT. SAT 2013: 166-181

[5] Jeremias Berg, Paul Saikko, Matti Järvisalo: Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT. IJCAI 2015: 239-245