Solving MaxSAT by Successive Calls to a SAT Solver
This work addresses the efficiency of exact solvers for MaxSAT, which is important for researchers and practitioners in computational logic and optimization, but it is incremental as it focuses on comparing existing algorithm types.
The paper compares the performance of SAT-based and branch-and-bound algorithms for solving the Maximum Satisfiability (MaxSAT) problem, finding that SAT-based methods are more efficient in practical scenarios based on experimental results from MaxSAT Evaluations benchmarks.
The Maximum Satisfiability (MaxSAT) problem is the problem of finding a truth assignment that maximizes the number of satisfied clauses of a given Boolean formula in Conjunctive Normal Form (CNF). 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 the benchmarks of the MaxSAT Evaluations.