Abstract
While the efficiency and scalability of modern SAT technology offers an intriguing alternative approach to constraint solving via translation to SAT, previous work has mostly focused on the translation of specific types of constraints, such as pseudo Boolean constraints, finite integer linear constraints, and constraints given as explicit listings of allowed tuples. By contrast, we present a translation of constraint models to SAT at language level, using the recently proposed constraint modeling language MiniZinc, such that any satisfaction or optimization problem written in the language (not involving floats) can be automatically Booleanized and solved by one or more calls to a SAT solver. We discuss the strengths and weaknesses of such a universal constraint solver, and report on a large-scale empirical evaluation of it against two existing solvers for MiniZinc: the finite domain solver distributed with MiniZinc and one based on the Gecode constraint programming platform. Our results indicate that Booleanization indeed offers a competitive alternative, exhibiting superior performance on some classes of problems involving large numbers of constraints and complex integer arithmetic, in addition to, naturally, problems that are already largely Boolean.
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
Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003)
Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: [16], pp. 827–831
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 191–200 (2006)
Silva, J.P.M., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: [17], pp. 483–497
Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 590–603. Springer, Heidelberg (2006)
Hawkins, P., Lagoon, V., Stuckey, P.J.: Solving set constraint satisfaction problems using ROBDDs. Journal of Artificial Intelligence Research 24, 109–156 (2005)
Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: Minizinc: Towards a standard CP modelling language. In: [17], pp. 529–543
G12: MiniZinc distribution, version rotd-2008-03-03, http://www.g12.csse.unimelb.edu.au/minizinc/
Huang, J.: A case for simple SAT solvers. In: [17], pp. 839–846
Stuckey, P.J., de la Banda, M.J.G., Maher, M.J., Marriott, K., Slaney, J.K., Somogyi, Z., Wallace, M., Walsh, T.: The G12 project: Mapping solver independent models to efficient solutions. In: [16], pp. 13–16.
SAT: The Annual SAT Competitions, http://www.satcompetition.org/
Katsirelos, G., Bacchus, F.: Generalized nogoods in CSPs. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 390–396. AAAI Press / The MIT Press (2005)
Schulte, C., Lagerkvist, M., Tack, G.: Gecode, http://www.gecode.org/
Brand, S., Duck, G.J., Puchinger, J., Stuckey, P.J.: Flexible, rule-based constraint model linearisation. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol. 4902, pp. 68–83. Springer, Heidelberg (2008)
van Beek, P. (ed.): Principles and Practice of Constraint Programming - CP 2005. LNCS, vol. 3709. Springer, Heidelberg (2005)
Bessière, C. (ed.): Principles and Practice of Constraint Programming – CP 2007. LNCS, vol. 4741. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huang, J. (2008). Universal Booleanization of Constraint Models. In: Stuckey, P.J. (eds) Principles and Practice of Constraint Programming. CP 2008. Lecture Notes in Computer Science, vol 5202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85958-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-85958-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85957-4
Online ISBN: 978-3-540-85958-1
eBook Packages: Computer ScienceComputer Science (R0)