LMHS swMATH ID: 16738 Software Authors: Saikko, Paul; Berg, Jeremias; Järvisalo, Matti Description: LMHS: A SAT-IP hybrid maxsat solver. We describe LMHS, an open-source weighted partial maximum satisfiability (MaxSAT) solver. LMHS is a hybrid SAT-IP MaxSAT solver that implements the implicit hitting set approach to MaxSAT. On top of the main algorithm, LMHS offers integrated preprocessing, solution enumeration, an incremental API, and the use of a choice of SAT and IP solvers. We describe the main features of LMHS, and give empirical results on the influence of preprocessing and the choice of the underlying SAT and IP solvers on the performance of LMHS. Homepage: https://www.cs.helsinki.fi/group/coreo/lmhs/ Related Software: MiniSat; QMaxSAT; Sat4j; Open-WBO; Lingeling; CPLEX; maxino; RC2; MaxHS; Treengeling; Glucose; Plingeling; TETRAD; SCIP; Coprocessor; WPM3; Open-WBO-Inc; CCEHC; CCLS; PySAT Cited in: 11 Publications all top 5 Cited by 33 Authors 4 Järvisalo, Matti 2 Berg, Jeremias 2 Hyttinen, Antti 2 Ignatyev, Alexey A. 2 Marques-Silva, João P. 2 Morgado, António 1 Alviano, Mario 1 Bacchus, Fahiem 1 Bonet, Maria Luisa 1 Buss, Sam 1 Danks, David 1 de Lima, Tiago 1 Dodaro, Carmine 1 Eberhardt, Frederick 1 Joshi, Saurabh 1 Koshimura, Miyuki 1 Kumar, Prateek 1 Lagniez, Jean-Marie 1 Le Berre, Daniel 1 Liao, Xiaojuan 1 Martins, Ruben 1 Montmirail, Valentin 1 Niskanen, Andreas 1 Nomoto, Kazuki 1 Plis, Sergey 1 Poole, Alex 1 Rantanen, Kari 1 Rao, Sukrut 1 Saikko, Paul 1 Sakurai, Yuko 1 Ueda, Suguru 1 Wallner, Johannes Peter 1 Yokoo, Makoto Cited in 5 Serials 2 International Journal of Approximate Reasoning 1 Artificial Intelligence 1 Constraints 1 Fundamenta Informaticae 1 Journal of Satisfiability, Boolean Modeling and Computation Cited in 5 Fields 11 Computer science (68-XX) 2 Statistics (62-XX) 1 Mathematical logic and foundations (03-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year