A Complete Multi-valued SAT Solver

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. 1 Multi-Valued SAT One of the very successful solvers for constraint satisfaction problems (CSPs) is Sugar [23]. It is based on the reduction of CSP to the satisfiability problem (SAT). Sugar first encodes the given problem as a SAT...

• Type: Journal
• Year: 2010
• Where: CP
• Authors: Siddhartha Jain, Eoin O'Mahony, Meinolf Sellmann
• Keywords: Artificial Intelligence, CP 2010, Multi-valued, Multi-valued Variable Xi, Multi-valued Variables