On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving

Ruben Martins Saurabh Joshi Vasco Manquinho InÍs Lynce
Abstract In recent years, unsatisfiability-based algorithms have become prevalent as state of the art for solving industrial instances of Maximum Satisfiability (MaxSAT). These algorithms perform a succession of unsatisfiable SAT solver calls until an optimal solution is found. In several of these algorithms, cardinality or pseudo-Boolean constraints are extended between iterations. However, in most cases, the formula provided to the SAT solver in each iteration must be rebuilt and no knowledge is reused from one iteration to the next.