Abstract
We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and prove that it is refutation complete for many-valued CNF formulas and, moreover, enforces CSP (i,j)-consistency when applied to a many-valued SAT encoding of a CSP. Instances of our rule enforce well-known local consistency properties such as arc consistency and path consistency.
Research partially supported by projects iDEAS (TIN2004-04343), Mulog (TIN2004-07933-C03-01/03) and IEA (TIN2006-15662-C02-02) funded by the MEC.
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
Ansótegui, C., et al.: The logic behind weighted CSP. In: Proc. of the 20th Int. Joint Conf. on Artificial Intelligence, IJCAI’07, pp. 32–37 (2007)
Ansótegui, C., Larrubia, J., Manyà, F.: Boosting Chaff’s performance by incorporating CSP heuristics. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 96–107. Springer, Heidelberg (2003)
Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with boolean variables. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 1–15. Springer, Heidelberg (2005)
Bacchus, F.: CSPs: Adding structure to SAT. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, Springer, Heidelberg (2006)
Beckert, B., Hähnle, R., Manyà, F.: Transformations between signed and classical clause logic. In: Proc. of the 29th Int. Symp. on Multiple-Valued Logics, ISMVL’99, pp. 248–255 (1999)
Beckert, B., Hähnle, R., Manyà, F.: The SAT problem of signed CNF formulas. In: Labelled Deduction. Applied Logic Series, vol. 17, pp. 61–82. Kluwer, Dordrecht (2000)
Bessière, C., Hebrard, E., Walsh, T.: Local consistencies in SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 299–314. Springer, Heidelberg (2004)
Dimopoulos, Y., Stergiou, K.: Propagation in CSP and SAT. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 137–151. Springer, Heidelberg (2006)
Frisch, A.M., Peugniez, T.J.: Solving non-boolean satisfiability problems with stochastic local search. In: Proc. of the Int. Joint Conf. on Artificial Intelligence, IJCAI’01, pp. 282–288 (2001)
Gent, I.P.: Arc consistency in SAT. In: Proc. of the 15th European Conf. on Artificial Intelligence, ECAI’02, pp. 121–125 (2002)
Hähnle, R.: Short CNF in finitely-valued logics. In: Komorowski, J., Raś, Z.W. (eds.) ISMIS 1993. LNCS, vol. 689, pp. 49–58. Springer, Heidelberg (1993)
Hähnle, R.: Efficient deduction in many-valued logics. In: Proc. of the Int. Symp. on Multiple-Valued Logics, ISMVL’94, pp. 240–249. IEEE Press, Los Alamitos (1994)
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
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Ansótegui, C., Bonet, M.L., Levy, J., Manyà, F. (2007). Mapping CSP into Many-Valued SAT. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)