Heras, F.; Larrosa, J.; Oliveras, A. Minimaxsat: an efficient weighted Max-SAT solver. (English) Zbl 1183.68578 J. Artif. Intell. Res. (JAIR) 31, 1-32 (2008). Summary: In this paper we introduce MiniMaxSat, a new Max-SAT solver that is built on top of MiniSat+. It incorporates the best current SAT and Max-SAT techniques. It can handle hard clauses(clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and substraction-based lower bounding; and lazy propagation with the two-watched literal scheme. Our empirical evaluation comparing a wide set of solving alternatives on a broad set of optimization benchmarks indicates that the performance of MiniMaxSat is usually close to the best specialized alternative and, in some cases, even better. Cited in 30 Documents MSC: 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Keywords:hard clauses; soft clauses; pseudo-boolean objective functions; constraints Software:MiniSat; Chaff; UBCSAT; MaxSolver; Pueblo; MiniMaxSat PDFBibTeX XMLCite \textit{F. Heras} et al., J. Artif. Intell. Res. (JAIR) 31, 1--32 (2008; Zbl 1183.68578)