Towards Solving Many-Valued MaxSAT

We define the MaxSAT problem for many-valued CNF formulas, called many-valued MaxSAT, and establish its complexity class. We then describe a basic branch and bound algorithm for solving many-valued MaxSAT, and an exact many-valued MaxSAT solver we have implemented. Finally, we report the experimental investigation we have performed to compare our solver with Boolean MaxSAT solvers on graph coloring instances. The results obtained indicate that many-valued CNF formulas can become a competitive formalism for representing and solving combinatorial optimization problems.

• Type: Conference
• Year: 2006
• Where: ISMVL
• Authors: Josep Argelich, Xavier Domingo, Chu Min Li, Felip Manyà, Jordi Planes
• Keywords: Artificial Intelligence, ISMVL 2006, Many-valued Cnf Formulas, Many-valued Maxsat, Many-valued Maxsat Solver