Community-Based Partitioning for MaxSAT Solving

摘要

Unsatisfiability-based algorithms for Maximum Satisfiability (MaxSAT) have been shown to be very effective in solving several classes of problem instances. These algorithms rely on successive calls to a SAT solver, where an unsatisfiable subformula is identified at each iteration. However, in some cases, the SAT solver returns unnecessarily large subformulas. In this paper a new technique is proposed to partition the MaxSAT formula in order to identify smaller unsatisfiable subformulas at each call of the SAT solver. Preliminary experimental results analyze the effect of partitioning the MaxSAT formula into communities. This technique is shown to significantly improve the unsatisfiability-based algorithm for different benchmark sets.