SAT-Based Versus CSP-Based Constraint Weighting for Satisfiability

Abstract

Recent research has focused on bridging the gap be-tween the satisfiability (SAT) and constraint satisfaction problem (CSP) formalisms. One approach has been to develop a many-valued SAT formula (MV-SAT) as an intermediate paradigm between SAT and CSP, and then to translate existing highly efficient SAT solvers to the MV-SAT domain. Experimental results have shown this approach can achieve significant improvements in per-formance compared with the traditional SAT and CSP approaches. In this paper, we follow a different route, developing SAT solvers that can automatically recognise CSP struc-ture hidden in SAT encodings. This allows us to look more closely at how constraint weighting can be im-plemented in the SAT and CSP domains. Our experi-mental results show that a SAT-based approach to han-dle weights, together with CSP-based approach to vari-able instantiation, is superior to other combinations of SAT and CSP-based approaches. A further experiment on the round robin scheduling problem indicates that this many-valued constraint weighting approach outper-forms other state-of-the-art solvers.