Solving (Weighted) Partial MaxSAT with ILP.
Carlos Ansótegui, Joel Gabàs · Integration of AI and OR Techniques in Constraint Programming · 2013
Several combinatorial optimization problems can be translated into the Weighted Partial Maximum Satisfiability (WPMS) problem. This is an optimization variant of the Satisfiability (SAT) problem. There are two main families of WPMS solvers based on SAT technology: branch and bound and SAT-based. From the MaxSAT evaluations, we have learned that SAT-based solvers dominate on industrial instances while branch and bound dominate on random. For crafted instances it depends on the category. In this work, we study the performance of an Integer Linear Programming approach. In particular, we translate the WPMS problem into ILP and apply the Mixed Integer Programming (MIP) solver, IBMCPLEX. We present an extensive experimental evaluation showing that this approach clearly dominates on crafted instances.