Local Search Algorithm for the Partial Minimum Satisfiability Problem

The Minimum Satisfiability Problem (MinSAT) consists in finding the minimum number of satisfied clauses of a CNF formula. This NP-hard problem is an extension of the famous SAT problem and has received less attention than its dual problem MaxSAT (Maximum Satisfiability). One of the MinSAT variants is the Partial MinSAT Problem where some clauses are hard and the others are soft. This variant is used to encode many optimization problems. Recent works on Partial MinSAT are only focused on its exact solving. In this paper, we propose a local search algorithm called GMinSAT to solve the Partial MinSAT Problem. It handles two opposite objectives: satisfying the hard clauses while minimizing the number of satisfied soft clauses. We compare empirically our proposed solver to the Branch & Bound solver MinSatz and show its interest on random and crafted instances. To the best of our knowledge, GMinSAT is the first genuine local search algorithm for this problem.