LMHSA SAT-IP Hybrid MaxSAT solverAboutLMHS [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. FeaturesLMHS currently
DownloadsLMHS 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 |