Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-18T15:48:13.768Z Has data issue: false hasContentIssue false
  • English
  • Français

Compiling finite domain constraints to SAT with BEE*

Published online by Cambridge University Press:  05 September 2012

AMIT METODI  and
MICHAEL CODISH
AMIT METODI
Affiliation:
Department of Computer Science, Ben-Gurion University, Israel
MICHAEL CODISH
Affiliation:
Department of Computer Science, Ben-Gurion University, Israel
Get access Rights & Permissions [Opens in a new window]

Abstract

We present BEE, a compiler which enables to encode finite domain constraint problems to CNF. Using BEE both eases the encoding process for the user and also performs transformations to simplify constraints and optimize their encoding to CNF. These optimizations are based primarily on equi-propagation and on partial evaluation, and also on the idea that a given constraint may have various possible CNF encodings. Often, the better encoding choice is made after constraint simplification. BEE is written in Prolog and integrates directly with a SAT solver through a suitable Prolog interface. We demonstrate that constraint simplification is often highly beneficial when solving hard finite domain constraint problems. A BEE implementation is available with this paper.

Keywords

SAT encodingFD constraintsequi-propagationpartial evaluation
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 4-5: 28th International Conference on Logic Programming , July 2012 , pp. 465 - 483
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ansótegui, C., del Val, A., Dotú, I., Fernández, C. and Manyà, F. 2004. Modeling choices in quasigroup completion: SAT vs. CSP. In AAAI, McGuinness, D. L. and Ferguson, G., Eds. AAAI Press/ The MIT Press, San Jose, California, USA, 137–142.Google Scholar
Asín, R., Nieuwenhuis, R., Oliveras, A. and Rodríguez-Carbonell, E. 2011. Cardinality networks: a theoretical and empirical study. Constraints 16, 2, 195–221.CrossRefGoogle Scholar
Bailleux, O. and Boufkhad, Y. 2003. Efficient CNF encoding of Boolean cardinality constraints. In CP, Rossi, F., Ed. LNCS, vol. 2833. Springer, Kinsale, Ireland, 108–122.Google Scholar
Batcher, K. E. 1968. Sorting networks and their applications. In AFIPS Spring Joint Computing Conference. AFIPS Conference Proceedings, vol. 32. Thomson Book Company, Washington D.C., Atlantic City, NJ, USA, 307–314.Google Scholar
Cadoli, M. and Schaerf, A. 2005. Compiling problem specifications into SAT. Artificial Intelligence 162, 1-2, 89–120.CrossRefGoogle Scholar
Chen, J. 2010. A new sat encoding of the at-most-one constraint. Workshop on Constraint Modeling and Reformulation (ModRef 2010) http://www.it.uu.se/research/group/astra/ModRef10/programme.html.Google Scholar
Codish, M., Lagoon, V. and Stuckey, P. J. 2008. Logic programming with satisfiability. TPLP 8, 1, 121–128.Google Scholar
Codish, M. and Zazon-Ivry, M. 2010. Pairwise cardinality networks. In LPAR (Dakar), Clarke, E. M. and Voronkov, A., Eds. Lecture Notes in Computer Science, vol. 6355. Springer, 154–172.Google Scholar
Crawford, J. M. and Baker, A. B. 1994. Experimental results on the application of satisfiability algorithms to scheduling problems. In AAAI, Hayes-Roth, B. and Korf, R. E., Eds. vol. 2. AAAI Press/ The MIT Press, Seattle, WA, USA, 1092–1097.Google Scholar
Eén, N. and Sörensson, N. 2003. An extensible SAT-solver. In SAT, Giunchiglia, E. and Tacchella, A., Eds. LNCS, vol. 2919. Springer, Santa Margherita Ligure, Italy, 502–518.Google Scholar
Eén, N. and Sörensson, N. 2006. Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 2, 1-4, 1–26.CrossRefGoogle Scholar
Feldman, A., Provan, G., de Kleer, J., Robert, S. and van Gemund, A. 2010. Solving model-based diagnosis problems with max-sat solvers and vice versa. https://www.phmsociety.org/events/workshop/dx/10/proceedings.Google Scholar
Frisch, A. M. and Giannaros, P. A. 2010. SAT encodings of the at-most-k constraint: Some old, some new, some fast, some slow. Workshop on Constraint Modeling and Reformulation (ModRef 2010) http://www.it.uu.se/research/group/astra/ModRef10/programme.html.Google Scholar
Frutos, A. G., Liu, Q., Thiel, A. J., Sanner, A. M. W., Condon, A. E., Smith, L. M. and Corn, R. M. 1997. Demonstration of a word design strategy for DNA computing on surfaces. Journal of Nucleic Acids Research 25, 23, 4748–4757.CrossRefGoogle ScholarPubMed
Gallian, J. A. 2011. A dynamic survey of graph labeling. The Electronic Journal of Combinatorics 18.Google Scholar
Gavanelli, M. 2007. The log-support encoding of csp into sat. In CP, Bessiere, C., Ed. LNCS, vol. 4741. Springer, Providence, RI, USA, 815–822.Google Scholar
Gomes, C. P., Selman, B. and Crato, N. 1997. Heavy-tailed distributions in combinatorial search. In CP, Smolka, G., Ed. LNCS, vol. 1330. Springer, 121–135.Google Scholar
Jäger, G. 2010. An effective sat encoding for magic labeling. In CTW, Faigle, U., Schrader, R., and Herrmann, D., Eds. 97–100.Google Scholar
MacDougall, J., Miller, M., Slamin, M. and Wallis, W. 2002. Vertex-magic total labelings of graphs. Utilitas Mathematica 61, 3–21.Google Scholar
Mancini, T., Micaletto, D., Patrizi, F. and Cadoli, M. 2008. Evaluating ASP and commercial solvers on the CSPLib. Constraints 13, 4, 407–436.CrossRefGoogle Scholar
Metodi, A. 2012. BEE. http://amit.metodi.me/research/bee/.Google Scholar
Metodi, A., Codish, M., Lagoon, V. and Stuckey, P. J. 2011. Boolean equi-propagation for optimized SAT encoding. In CP, Lee, J. H.-M., Ed. LNCS, vol. 6876. Springer, 621–636.Google Scholar
Metodi, A., Stern, R., Kalech, M. and Codish, M. 2012. Compiling Model-based Diagnosis to Boolean Satisfaction. Techical rep., Department of Computer Science, Ben-Gurion University. URL: www.cs.bgu.ac.il/~mcodish/Papers/Sources/satMBD.pdf.Google Scholar
Nethercote, N., Stuckey, P. J., Becket, R., Brand, S., Duck, G. J. and Tack, G. 2007. MiniZinc: Towards a standard CP modelling language. In Principles and Practice of Constraint Programming, Bessiere, C., Ed. LNCS, vol. 4741. Springer-Verlag, 529–543.Google Scholar
Régin, J.-C. 1994. A filtering algorithm for constraints of difference in csps. In AAAI, Hayes-Roth, B. and Korf, R. E., Eds. AAAI Press/ The MIT Press, 362–367.Google Scholar
Reiter, R. 1987. A theory of diagnosis from first principles. Artificial Intelligence 32, 1, 57–96.CrossRefGoogle Scholar
Smith, A., Veneris, A., Ali, M. F. and Viglas, A. 2005. Fault diagnosis and logic debugging using Boolean satisfiability. IEEE TRANS. ON CAD 24, 1606–1621.CrossRefGoogle Scholar
Soos, M. 2010. CryptoMiniSAT, v2.5.1. http://www.msoos.org/cryptominisat2.Google Scholar
Tamura, N., Taga, A., Kitagawa, S. and Banbara, M. 2009. Compiling finite linear CSP into SAT. Constraints 14, 2, 254–272.CrossRefGoogle Scholar
van Hentenryck, P. 1999. The OPL Optimization Programming Language. MIT Press.Google Scholar