The Maximum Satisfiability (MaxSAT), an important optimization problem, has a range of applications, including network routing, planning and scheduling, and combinatorial auctions. Among these applications, one usually benefits from having not just one single solution, but $k$ diverse solutions. Motivated by this, we study an extension of MaxSAT, named Diversified Top-$k$ MaxSAT (DTKMS) problem, which is to find $k$ feasible assignments of a given formula such that each assignment satisfies all hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, LS-DTKMS, for DTKMS problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-$k$ MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-$k$ clique problem.
LS-DTKMS: a Local Search Algorithm for Diversified Top-K MaxSAT Problem