ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver

Abstract

Branch and bound (BnB) solvers for Max-SAT count at each node of the search tree the number of disjoint inconsistent subsets to compute the lower bound. In the last ten years, important advances have been made regarding the lower bound computation. Unit propagation based methods have been introduced to detect inconsistent subsets and a resolution-like inference rules have been proposed which allow a more efficient and incremental lower bound computation. We present in this paper our solver ahmaxsat, which uses these new methods and improves them in several ways. The main specificities of our solver over the state of the art are: a new unit propagation scheme which considers all the variable propagation sources; an extended set of patterns which increase the amount of learning performed by the solver; a heuristic which modifies the order of application of the max-resolution rule when transforming inconsistent subset; and a new inconsistent subset treatment method which improves the lower bound estimation. All of them have been published in recent international conferences. We describe these four main components and we give a general overview of ahmaxsat, with additional implementation details. Finally, we present the result of the experimental study we have conducted. We first evaluate the impact of each component on ahmaxsat performance before comparing our solver to some of the current best performing complete Max-SAT solvers. The results obtained confirm the ones of the Max-SAT Evaluation 2014 where ahmaxsat was ranked first in three of the nine categories.