Abstract
We perform a comprehensive study of mappings between constraint satisfaction problems (CSPs) and propositional satisfiability (SAT). We analyse four different mappings of SAT problems into CSPs, and two of CSPs into SAT problems. For each mapping, we compare the impact of achieving arc-consistency on the CSP with unit propagation on the SAT problem. We then extend these results to CSP algorithms that maintain (some level of) arc-consistency during search like FC and MAC, and to the Davis-Putnam procedure (which performs unit propagation at each search node). Because of differences in the branching structure of their search, a result showing the dominance of achieving arc-consistency on the CSP over unit propagation on the SAT problem does not necessarily translate to the dominance of MAC over the Davis-Putnam procedure. These results provide insight into the relationship between propositional satisfiability and constraint satisfaction.
The author is supported by an EPSRC advanced research fellowship. The author is a member of the APES research group (http://www.cs.strath.ac.uk/~apes) and wishes to thank the other members for their comments and feedback.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K. Apt. Some Remarks on Boolean Constraint Propagation. In New Trends in Constraints, Papers from the Joint ERCIM/Compulog-Net Workshop. Springer, 1999.
H. Bennaceur. The satisfiability problem regarded as a constraint satisfaction problem. In W. Wahlster, editor, Proc. of the 12th ECAI, pages 155–159. European Conference on Artificial Intelligence, Wiley, 1996.
C. Bessière, P. Meseguer, E. C. Freuder, and J. Larrosa. On Forward Checking for Non-binary Constraint Satisfaction. In A. Brodsky and J. Jaffar, editors, Proc. of Fifth International Conference on Principles and Practice of Constraint Programming (CP99). Springer, 1999.
F. Bacchus and P. van Beek. On the conversion between non-binary and binary constraint satisfaction problems. In Proc. of 15th National Conference on Artificial Intelligence, pages 311–318. AAAI Press/The MIT Press, 1998.
J. de Kleer. A comparison of ATMS and CSP techniques. In Proc. of the 11th IJCAI. International Joint Conference on Artificial Intelligence, 1989.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394–397, 1962.
A. M. Frisch and T. J. Peugniez. Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings., 1999. Unpublished manuscript, available from http://www.cs.york.ac.uk/aig/publications.html.
J. Gaschnig. Performance measurement and analysis of certain search algorithms. Technical report CMU-CS-79-124, Carnegie-Mellon University, 1979. PhD thesis.
M. R. Garey and D. S. Johnson. Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman, 1979.
R. Genisson and P. Jegou. Davis and Putnam were already forward checking. In W. Wahlster, editor, Proc. of the 12th ECAI, pages 180–184. European Conference on Artificial Intelligence, Wiley, 1996.
R. Mohr and G. Masini. Good old discrete relaxation. In Proc. of the 8th ECAI, pages 651–656, European Conference on Artificial Intelligence, 1988.
K. Stergiou and T. Walsh. Encodings of non-binary constraint satisfaction problems. In Proc. of the 16th National Conference on AI. American Association for Artificial Intelligence, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Walsh, T. (2000). SAT v CSP. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_32
Download citation
DOI: https://doi.org/10.1007/3-540-45349-0_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41053-9
Online ISBN: 978-3-540-45349-9
eBook Packages: Springer Book Archive