Exploiting Many-Valued Variables in MaxSAT

Solving combinatorial optimization problems by reducing them to MaxSAT has shown to be a competitive problem solving approach. Since a lot of optimization problems have many-valued variables, we propose to exploit the domain information of the many-valued variables to enhance MaxSAT-based problem solving: first, we define a new way of encoding weighted maximum constraint satisfaction problems to both Boolean MaxSAT and manyvalued MaxSAT; and second, we define a variable selection heuristic that takes into account the domain information and allow us to easily implement a many-valued MaxSAT solver. Moreover, the empirical results provide evidence of the good performance of the new encodings and the new branching heuristic on a representative set of instances. © 2017 IEEE.This work was supported by the Generalitat de Catalunya grant AGAUR 2014-SGR-118, and the MINECO-FEDER project RASO TIN2015-71799-C2-1-P/2-P. The third author was supported by Mobility Grant PRX16/00215 of the Ministerio de Educación, Cultura y Deporte.Peer Reviewe