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.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Hyttinen, Antti; Plis, Sergey; Järvisalo, Matti; Eberhardt, Frederick; Danks, David: A constraint optimization approach to causal discovery from subsampled time series data (2017)
- Korhonen, Tuukka; Berg, Jeremias; Saikko, Paul; Järvisalo, Matti: Maxpre: an extended maxsat preprocessor (2017)
- Niskanen, Andreas; Wallner, Johannes P.; Järvisalo, Matti: Pakota: a system for enforcement in abstract argumentation (2016)
- Saikko, Paul; Berg, Jeremias; Järvisalo, Matti: LMHS: A SAT-IP hybrid maxsat solver (2016)