SAT-based Versus CSP-based Constraint Weighting for Satisfiability

Duc Nghia Pham, John Thornton, Abdul Sattar, Abdelraouf Ishtaiwi

Recent research has focused on bridging the gap between 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 performance compared with the traditional SAT and CSP approaches. In this paper, we follow a different route, developing SAT solvers that can automatically recognise CSP structure hidden in SAT encodings. This allows us to look more closely at how constraint weighting can be implemented in the SAT and CSP domains. Our experimental results show that a SAT-based approach to handle weights, together with CSP-based approach to variable 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 outperforms other state-of-the-art solvers.

Content Area: 6. Constraint Satisfaction and Satisfiability

Subjects: 15.2 Constraint Satisfaction; 15.7 Search

Submitted: May 10, 2005

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.