Abstract
We study how propositional satisfiability (SAT) problems can be reformulated as constraint satisfaction problems (CSPs). We analyse four different mappings of SAT problems into CSPs. For each mapping, we compare theoretically the performance of systematic algorithms like FC and MAC applied to the encoding against the Davis-Putnam procedure applied to the original SAT problem. We also compare local search methods like GSAT and WalkSAT on a SAT problem against the Min-Conflicts procedure applied to its encoding. Finally, we look at the special case of local search methods applied to 2-SAT problems and encodings of 2-SAT problems. Our results provide insight into the relationship between propositional satisfiability and constraint satisfaction, as well as some of the potential benefits of reformulating problems as constraint satisfaction problems.
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.
references
H. Bennaceur. The satisfiability problem regarded as a constraint satisfaction problem. In W. Wahlster, editor, Proceedings of the 12th EC AI, pages 155–159. European Conference on Artificial Intelligence, Wiley, 1996.
C. Bessiere, P. Meseguer, E.C. Freuder, and J. Larrosa. On forward checking for non-binary constraint satisfaction. In Proceedings of IJCAI-99 Workshop on Non-binary constraints International Joint Conference on Artificial Intelligence, 1999.
F. Bacchus and P. van Beek. On the conversion between non-binary and binary constraint satisfaction problems. In Proceedings of 15th National Conference on Artificial Intelligence, pages 311–318. AAAI Press/The MIT Press, 1998.
V. Chvatal and B. Reed. Mick gets some (the odds are on his side). In Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, pages 620–627. IEEE, 1992.
R. Debruyne and C. Bessiére. Some practicable filtering techniques for the constraint satisfaction problem. In Proceedings of the 15th IJCAI, pages 412–417. International Joint Conference on Artificial Intelligence, 1997.
R. Dechter. Enhancement schemes for constraint processing: Backjumping, learning and cutset decompositio. Artificial Intelligence, 41(3):273–312, 1990.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394–397, 1962.
M. L. Ginsberg. Dynamic backtracking. Journal of Artificial Intelligence Research, 1:25–46, 1993.
A. Goerdt. A theshold for unsatisfiability. In I. Havel and V. Koubek, editors, Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, pages 264–274. Springer Verlag, 1992.
H. Kautz and B. Selman. BLACKBOX: A new approach to the application of theorem proving to problem solving. In Working notes of the Workshop on Planning as Combinatorial Search, 1998. Held in conjunction with AIPS-98, Pittsburgh, PA, 1998.
H. Kautz and B. Selman. The role of domain-specific knowledge in the planning as satisfiability framework. In Proceedings of AIPS-98, Pittsburgh, PA, 1998.
C.H. Papadimitriou. On selecting a satisfying truth assigment. In Proceedings of the Conference on the Foundations of Computer Science, pages 163–169, 1991.
K. Stergiou and T. Walsh. Encodings of non-binary constraint satisfaction problems. In Proceedings of the 16th National Conference on AI American Association for Artificial Intelligence, 1999.
P. van Beek and X. Chen. Cplan: a constraint programming approach to planning. In Proceedings of 16th National Conference on Artificial Intelligence AAAI Press/The MIT Press, 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). Reformulating Propositional Satisfiability as Constraint Satisfaction. In: Choueiry, B.Y., Walsh, T. (eds) Abstraction, Reformulation, and Approximation. SARA 2000. Lecture Notes in Computer Science(), vol 1864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44914-0_14
Download citation
DOI: https://doi.org/10.1007/3-540-44914-0_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67839-7
Online ISBN: 978-3-540-44914-0
eBook Packages: Springer Book Archive