MiniMaxSAT: An Efficient Weighted Max-SAT Solver

F. Heras, J. Larrosa and A. Oliveras

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.