Solution reuse in partial MAX-SAT problem

Partial MAX-SAT (PMSAT) is a variant of the MAX-SAT problem in propositional logic. It was introduced as an encoding domain for real-world problems in which the satisfiability of some constraints is required to the feasibility of a solution. It consists of two CNF formulae over the same variable set, and its solution must satisfy all clauses of the first formula and as many clauses in the second formula as possible. Existing methods solve PMSAT by repeating the clauses of the first formula and then performing local search on the resulting problem. This involves a larger instance and then can lead to significant increase in the amount of computational time. In this work we propose a new approach for solving PMSAT based mainly on recycling the model of the first formula to satisfy the maximum number of clauses in the second one. We derive three different algorithms and investigate their performance differences by applying them to solve various instances of PMSAT produced from SAT instances. We also compare our results against those of an initial weighting strategy algorithm. The results suggest good prospects of this approach to PMSAT.