Byungki Cha, Kazuo Iwama, Yahiko Kambayashi, Shuichi Miyazaki
MAXSAT solutions, i.e., near-satisfying assignments for propositional formulas, are sometimes meaningless for real-world problems because such formulas include "mandatory clauses" that must be all satisfied for the solution to be reasonable. In this paper, we introduce Partial MAXSAT and investigate how to solve it using local search algorithms. An instance of Partial MAXSAT consists of two formulas fA and fB, and its solution must satisfy all clauses in fA and as many clauses in fB as possible. The basic idea of our algorithm is to give weight to fA-clauses (the mandatory clauses) and then apply local search. We face two problems; (i) what amount of weight is appropriate and (ii) how to deal with the common action of local search algorithms, giving weight to clauses for their own purpose, which will hide the initial weight as the algorithms proceed.