Diversified Top-k Partial MaxSAT Solving
  We introduce a diversified top-k partial MaxSAT problem, a combination of
partial MaxSAT problem and enumeration problem. Given a partial MaxSAT formula
F and a positive integer k, the diversified top-k partial MaxSAT is to find k
maximal solutions for F such that the k maximal solutions satisfy the maximum
number of soft clauses of F. This problem can be widely used in many
applications including community detection, sensor place, motif discovery, and
combinatorial testing. We prove the problem is NP-hard and propose an approach
for solving the problem. The concrete idea of the approach is to design an
encoding EE which reduces diversified top-k partial MaxSAT problem into partial
MaxSAT problem, and then solve the resulting problem with state-of-art solvers.
In addition, we present an algorithm MEMKC exactly solving the diversified
top-k partial MaxSAT. Through several experiments we show that our approach can
be successfully applied to the interesting problem.
