MiniMaxSAT: An Efficient Weighted Max-SAT solver

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 substractionbased 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.

• Type: Journal
• Year: 2008
• Where: JAIR
• Authors: Federico Heras, Javier Larrosa, Albert Oliveras
• Keywords: Hard Clauses, JAIR 2008, Max-SAT, Soft Clauses