A complete multi-valued SAT solver

Abstract

We present a new complete multi-valued SAT solver, based on current state-of-the-art SAT technology. It features watched literal propagation and conflict driven clause learning. We combine this technology with state-of-the-art CP methods for branching and introduce quantitative supports which augment the watched literal scheme with a watched domain size scheme. Most importantly, we adapt SAT nogood learning for the multi-valued case and demonstrate that exploiting the knowledge that each variable must take exactly one out of many values can lead to much stronger nogoods. Experimental results assess the benefits of these contributions and show that solving multi-valued SAT directly often works better than reducing multi-valued constraint problems to SAT. © 2010 Springer-Verlag.