Abstract
We introduce some new mappings of constraint satisfaction problems into propositional satisfiability. These encodings generalize most of the existing encodings. Unit propagation on those encodings is the same as establishing relational k -arc consistency on the original problem. They can also be used to establish (i,j)-consistency on binary constraints. Experiments show that these encodings are an effective method for enforcing such consistencies, that can lead to a reduction in runtimes at the phase transition in most cases. Compared to the more traditional (direct) encoding, the search tree can be greatly pruned.
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
Bacchus, F., Chen, X., van Beek, P., Walsh, T.: Binary vs. non-binary constraints. Artificial Intelligence 140(1-2), 1–37 (2002)
Bessière, C., Chmeiss, A., Saïs, L.: Neighborhood-based variable ordering heuristics for the constraint satisfaction problem. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 565–569. Springer, Heidelberg (2001) (short paper)
Bessière, C., Meseguer, P., Freuder, E.C., Larrosa, J.: On forward checking for non-binary constraint satisfaction. Artificial Intelligence 141, 205–224 (2002)
Bessière, C., Régin, J.C.: MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 61–75. Springer, Heidelberg (1996)
Bessière, C., Régin, J.C.: Refining the basic constraint propagation algorithm. In: Proceedings IJCAI 2001, pp. 309–315 (2001)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Debruyne, R.: A property of path inverse consistency leading to an optimal PIC algorithm. In: Proceedings ECAI 2000, pp. 88–92 (2000)
Dechter, R., van Beek, P.: Local and global relational consistency. Theoretical Computer Science 173(1), 283–308 (1997)
Freuder, E.C.: A sufficient condition for backtrack-bounded search. Journal of the ACM 32, 755–761 (1985)
Gent, I.P.: Arc consistency in SAT. In: Proceedings ECAI 2002 (2002)
Golberg, E., Novikov, Y.: Berkmin: a fast and robust sat-solver. In: Proceeding DATE 2002, pp. 142–149 (2002)
Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence 45, 275–286 (1990)
Nadel, B.A.: Constraint satisfaction algorithms. Computational Intelligence 5, 188–224 (1989)
van Beek, P., Dechter, R.: Constraint tightness and looseness versus local and global consistency. Journal of the ACM 44, 549–566 (1997)
van Beek, P., Wilken, K.: Fast optimal instruction scheduling for single issue processors with arbitrary latencies. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 625–639. Springer, Heidelberg (2001)
Verfaillie, G., Martinez, D., Bessière, C.: A generic customizable framework for inverse local consistency. In: Proceeding AAAI 1999, pp. 169–174 (1999)
Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bessière, C., Hebrard, E., Walsh, T. (2004). Local Consistencies in SAT. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive