Solving incremental MAX-SAT

The maximum satisfiability problem (MAX-SAT) consists of finding a truth assignment that satisfies the maximum possible number of clauses in a given formula in CNF form. In this paper, we introduce the incremental MAX-SAT problem which focuses on maintaining the maximum satisfiability of a propositional formula anytime a conjunction of new clauses is added. More precisely, the goal here is to check whether the maximum number of clauses is maintained after a new set of clauses is added and if not, look for a new maximum in an incremental manner. We will investigate the applicability of different methods based on exact and approximation algorithms for solving incremental MAX-SAT problems. The exact algorithm is a branch and bound technique while the approximation techniques rely on stochastic local search and genetic algorithms.