Many-Valued MinSAT Solving

Solving combinatorial optimization problems via their reduction to Boolean MinSAT is an emerging generic problem solving approach. In this paper we extend MinSAT with many-valued variables, and refer to the new formalism as Many-Valued MinSAT. For Many-Valued MinSAT, we describe an exact solver, Mv-MinSatz, which builds on the Boolean branch-and-bound solver MinSatz, and exploits the domain information of many-valued variables. Moreover, we also define efficient and robust encodings from optimization problems with many-valued variables to MinSAT. The empirical results provide evidence of the good performance of the new encodings, and of Many-Valued MinSAT over Boolean MinSAT on relevant optimization problems.