Solving MaxSAT by successive calls to a SAT solver

Abstract

The Maximum Satisfiability (MaxSAT) is the problem of determining the maximum number of clauses of a given Boolean formula in Conjunctive Normal Form (CNF) that can be satisfied by an assignment of truth values to the variables of the formula. Many exact solvers for MaxSAT have been developed during recent years, and many of them were presented in the well-known SAT Conference. Algorithms for MaxSAT generally fall into two categories: (1) branch and bound algorithms and (2) algorithms that use successive calls to a SAT solver (SAT-based), which this paper in on. In practical problems, SAT-based algorithms have been shown to be more efficient. This paper provides an experimental investigation to compare the performance of recent SAT-based and branch and bound algorithms on benchmarks of the MaxSAT Evaluations.