Abstract
We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empirically on a set of benchmarks with state-of-the-art SAT solvers. Our results provide empirical evidence that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.
Research partially supported by projects TIC2001-1577-C03-03 and TIC2003-00950 funded by the Ministerio de Ciencia y Tecnología. We thank Carla Gomes for allowing us to use computational resources of the Intelligent Information Systems Institute (Cornell University).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alsinet, T., Béjar, R., Cabiscol, A., Fernández, C., Manyà, F.: Minimal and redundant SAT encodings for the all-interval-series problem. In: Escrig, M.T., Toledo, F.J., Golobardes, E. (eds.) CCIA 2002. LNCS (LNAI), vol. 2504, pp. 139–144. Springer, Heidelberg (2002)
Ansótegui, C., Béjar, R., Cabiscol, A., Li, C.M., Manyà, F.: Resolution methods for many-valued CNF formulas. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002, Cincinnati, USA, pp. 156–163 (2002)
Ansótegui, C., Larrubia, J., Li, C.M., Manyà, F.: Mv-Satz: A SAT solver for many-valued clausal forms. In: 4th International Conference Journées de L’Informatique Messine, JIM 2003, Metz, France (2003)
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., Béjar, R., Gomes, C.: Solving many-valued SAT encodings with local search. In: Proceedings of the Workshop on Probabilistics Approaches in Search, 18th National Conference on Artificial Intelligence, AAAI 2002, Edmonton, Canada (2002)
Baaz, M., Fermüller, C.G.: Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computation 19, 353–391 (1995)
Beckert, B., Hähnle, R., Manyà, F.: Transformations between signed and classical clause logic. In: Proceedings, International Symposium on Multiple-Valued Logics, ISMVL 1999, Freiburg, Germany, pp. 248–255. IEEE Press, Los Alamitos (1999)
Beckert, B., Hähnle, R., Manyà, F.: The SAT problem of signed CNF formulas. In: Basin, D., D’Agostino, M., Gabbay, D., Matthews, S., Viganò, L. (eds.) Labelled Deduction. Applied Logic Series, vol. 17, pp. 61–82. Kluwer, Dordrecht (2000)
Béjar, R., Cabiscol, A., Fernández, C., Manyà, F., Gomes, C.P.: Capturing structure with satisfiability. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 137–152. Springer, Heidelberg (2001)
Béjar, R., Hähnle, R., Manyà, F.: A modular reduction of regular logic to classical logic. In: Proceedings, 31st International Symposium on Multiple-Valued Logics (ISMVL), Warsaw, Poland, pp. 221–226. IEEE CS Press, Los Alamitos (2001)
Béjar, R., Manyà, F.: A comparison of systematic and local search algorithms for regular CNF formulas. In: Hunter, A., Parsons, S. (eds.) ECSQARU 1999. LNCS (LNAI), vol. 1638, pp. 22–31. Springer, Heidelberg (1999)
Culberson, J.: Graph coloring page: The flat graph generator (1995) See, http://web.cs.ualberta.ca/~joe/Coloring/Generators/flat.html
Escalada-Imaz, G., Manyà, F.: The satisfiability problem for multiple-valued Horn formulæ. In: Proceedings, International Symposium on Multiple-Valued Logics, ISMVL1994, Boston/MA, USA, pp. 250–256. IEEE Press, Los Alamitos (1994)
Frisch, A.M., Peugniez, T.J.: Solving non-boolean satisfiability problems with stochastic local search. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI 2001, pp. 282–288 (2001)
Hähnle, R.: Towards an efficient tableau proof procedure for multiple-valued logics. In: Schönfeld, W., Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol. 533, pp. 248–260. Springer, Heidelberg (1991)
Hähnle, R.: Automated Deduction in Multiple-Valued Logics. In: International Series of Monographs in Computer Science, vol. 10. Oxford University Press, Oxford (1994)
Hähnle, R.: Advanced many-valued logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 2. Kluwer, Dordrecht (2001)
Manyà, F.: Proof Procedures for Multiple-Valued Propositional Logics. PhD thesis, Universitat Autònoma de Barcelona (1996)
Manyà, F.: The 2-SAT problem in signed CNF formulas. Multiple-Valued Logic. An International Journal 5(4), 307–325 (2000)
Manyà, F., Béjar, R., Escalada-Imaz, G.: The satisfiability problem in regular CNF-formulas. Soft Computing: A Fusion of Foundations, Methodologies and Applications 2(3), 116–123 (1998)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: 39th Design Automation Conference (2001)
Murray, N.V., Rosenthal, E.: Resolution and path-dissolution in multiple-valued logics. In: Raś, Z.W., Zemankova, M. (eds.) ISMIS 1991. LNCS (LNAI), vol. 542, pp. 570–579. Springer, Heidelberg (1991)
Prestwich, S.D.: Local search on SAT-encoded colouring problems. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 105–109. Springer, Heidelberg (2004)
Smith, B., Dyer, M.: Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence 81, 155–181 (1996)
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
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ansótegui, C., Manyà, F. (2005). Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_1
Download citation
DOI: https://doi.org/10.1007/11527695_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27829-0
Online ISBN: 978-3-540-31580-3
eBook Packages: Computer ScienceComputer Science (R0)