Solving Over-Constrained Problems with Max-SAT Algorithms ⋆

Abstract. We present a new generic problem solving approach for overconstrained problems based on Max-SAT algorithms. We first define a clausal form formalism that deals with blocks of clauses instead of individual clauses, and that allows to declare each block either as hard (i.e., must be satisfied by any solution) or soft (i.e., can be violated by some solution). We then present a Max-SAT branch and bound algorithm that finds a truth assignment that satisfies all the hard blocks of clauses and the maximum number of soft blocks of clauses. Finally, we present an experimental investigation to assess the performance of our approach.