zbMATH — the first resource for mathematics

meSAT: multiple encodings of CSP to SAT. (English) Zbl 1316.90049
Summary: One approach for solving Constraint Satisfaction Problems (CSP) (and related Constraint Optimization Problems (COP)) involving integer and Boolean variables is reduction to propositional satisfiability problem (SAT). A number of encodings (e.g., direct, log, support, order) for this purpose exist as well as specific encodings for some constraints that are often encountered (e.g., cardinality constraints, global constraints). However, there is no single encoding that performs well on all classes of problems and there is a need for a system that supports multiple encodings. We present a system that translates specifications of finite linear CSP problems into SAT instances using several well-known encodings, and their combinations. We also present a methodology for selecting a suitable encoding based on simple syntactic features of the input CSP instance. Thorough evaluation has been performed on large publicly available corpora and our encoding selection method improves upon the efficiency of existing encodings and state-of-the-art tools used in comparison.

90C30 Nonlinear programming
90C11 Mixed integer programming
Full Text: DOI
[1] Amadini, R., Gabbrielli, M., Mauro, J. (2013). An empirical evaluation of portfolios approaches for solving CSPs. In CoRR 2013, LNCS 7874 (pp. 316-324). Springer. · Zbl 1382.68219
[2] Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E. (2009). Cardinality networks and their applications. In SAT 2009, LNCS 5584 (pp. 167-180). Springer. · Zbl 1247.68244
[3] Banbara, M., Matsunaka, H., Tamura, N., Inoue, K. (2010). Generating combinatorial test cases by efficient SAT encodings suitable for CDCL SAT solvers. In LPAR (Yogyakarta), LNCS 6397 (pp. 112-126). Springer. · Zbl 1306.68182
[4] Beldiceanu, N., Carlsson, M., Rampon, J.-X. (2005). Global constraint catalog Technical report. SICS. · Zbl 1182.68272
[5] Ben-Haim, Y., Ivrii, A., Margalit, O., Matsliah, A. (2012). Perfect hashing and CNF encodings of cardinality constraints. In SAT 2012, LNCS 7317 (pp. 397-409). Springer. · Zbl 1273.68315
[6] Biere, A., Heule, M. J. H., van Maaren, H., Walsh, T., (eds.) (2009). Handbook of satisfiability, volume 185 of frontiers in artificial intelligence and applications. IOS Press. · Zbl 1183.68568
[7] Bofill, M., Suy, J., Villaret, M. (2010). A system for solving constraint satisfaction problems with smt. In SAT 2010, LNCS 6175 (pp. 300-305). Springer. · Zbl 1306.68153
[8] Cadoli, M., Palopoli, L., Schaerf, A., Vasile, D. (1999). NP-SPEC: An executable specification language for solving all problems in NP. In PADL 1999, LNCS 1551 (pp. 16-30). Springer. · Zbl 0995.68025
[9] Cadoli, M; Andrea, S, SPEC2SAT: compiling problem specifications into SAT, Artificial Intelligence, 162, 89-120, (2005) · Zbl 1132.68693
[10] Chen, J. (2010). A new SAT encoding of the at-most-one constraint. In Proceedings of the 9th international workshop on constraint modelling and reformulation. · Zbl 1192.68831
[11] Codish, M., & Zazon-Ivry, M. (2010). Pairwise cardinality networks. In LPAR (Dakar), LNCS 6355 (pp. 154-172). Springer. · Zbl 1253.68112
[12] Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In SAT 2003, LNCS 2919 (pp. 502-518). Springer. · Zbl 1192.68831
[13] Gavanelli, M. The log-support encoding of CSP into SAT. In CP 2007, LNCS 4741 (pp. 815-822). · Zbl 1145.68512
[14] Van Gelder, A, Another look at graph coloring via propositional satisfiability, Discrete Applied Mathematics, 156, 230-243, (2008) · Zbl 1131.05090
[15] Gent, I.P. (2002). Arc consistency in SAT. In ECAI 2002 (pp. 121-125). IOS Press.
[16] Horbach, A, A Boolean satisfiability approach to the resource-constrained project scheduling problem, Annals OR, 181, 89-107, (2010) · Zbl 1209.90170
[17] Huang, J. (2008). Universal booleanization of constraint models. In CP 2008, LNCS 5202, (pp. 144-158). Springer.
[18] Hutter, F; Hoos, HH; Leyton-Brown, K; Stützle, T, Paramils: an automatic algorithm configuration framework, Journal of Artificial Intelligence Research (JAIR), 36, 267-306, (2009) · Zbl 1192.68831
[19] Janičić, P, Uniform reduction to SAT., Logical Methods in Computer Science, 8, 1-39, (2012) · Zbl 1248.68456
[20] Kiziltan, Z., Mandrioli, L., Barry, OS., Mauro, J. (2011). A classification-based approach to manage a solver portfolio for csps. In Proceedings of the 22nd Irish conference on artificial intelligence and cognitive science, AICS-2011.
[21] Malitsky, Y., & Sellmann, M. (2012). Instance-specific algorithm configuration as a method for non-model-based portfolio generation. In CPAIOR 2012, LNCS 7298 (pp. 244-259). Springer.
[22] Marić, F., & Janičić, P. (2010). URBIVA: Uniform reduction to bit-vector arithmetic. In IJCAR 2010, LNCS 6173 (pp. 346-352). Springer. · Zbl 1291.68361
[23] Metodi, A; Codish, M, Compiling finite domain constraints to SAT with BEE, TPLP, 12, 465-483, (2012) · Zbl 1260.68081
[24] Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G. Minizinc: Towards a standard CP modelling language. In CP 2007 (pp. 529-543).
[25] Nikolić, M. (2010). Statistical methodology for comparison of sat solvers. In SAT 2010, LNCS 6175 (pp. 209-222). Springer. · Zbl 1306.68171
[26] Nikolić, M., Marić, F., Janičić, P. (2009). Instance-based selection of policies for SAT solvers. In SAT 2009, LNCS 5584 (pp. 326-340).
[27] Nikolić, M; Marić, F; Janičić, P, Simple algorithm portfolio for SAT., Artificial Intelligence Review, 40, 457-465, (2011)
[28] Ohrimenko, O; Stuckey, PJ; Codish, M, Propagation via lazy clause generation, Constraints, 14, 357-391, (2009) · Zbl 1192.68654
[29] O’Mahony, E., Hebrard, E., Holland, A., Nugent, C., O’Sullivan, B. (2008). Using case-based reasoning in an algorithm portfolio for constraint solving. In Proceedings of the 19th Irish conference on artificial intelligence and cognitive science. AICS-2008.
[30] Rossi, F., van Beek, P., Walsh, T., (eds.) (2006). Handbook of constraint programming. Elsevier. · Zbl 1175.90011
[31] Roussel, O., & Lecoutre, C. (2009). XML representation of constraint networks: format XCSP 2.1. CoRR, abs/0902.2362. · Zbl 1192.68654
[32] Sinz, C. (2005). Towards an optimal CNF encoding of boolean cardinality constraints. In CP 2005, LNCS 3709 (pp. 827-831). Springer. · Zbl 1153.68488
[33] Soh, T; Inoue, K; Tamura, N; Banbara, M; Nabeshima, H, A SAT-based method for solving the two-dimensional strip packing problem, Fundamental Information, 102, 467-487, (2010) · Zbl 1214.68374
[34] Tamura, N., & Banbara, M. (2008). Sugar: A CSP to sat translator based on order encoding. In Proceedings of the third constraint solver competition (pp. 65-69).
[35] Tamura, N; Taga, A; Kitagawa, S; Banbara, M, Compiling finite linear CSP into SAT, Constraints, 14, 254-272, (2009) · Zbl 1186.68076
[36] Tanjo, T., Tamura, N., Banbara, M. (2011). A compact and efficient SAT-encoding of finite domain CSP. In SAT 2011, LNCS 6695 (pp. 375-376). Springer.
[37] Tanjo, T., Tamura, N., Banbara, M. Azucar: A SAT-based CSP solver using compact order encoding - (tool presentation). In: SAT 2012, LNCS 7317 (pp. 456-462). · Zbl 1209.90170
[38] Tomovic, A; Janicic, P; Keselj, V, N-Gram-based classification and unsupervised hierarchical clustering of genome sequences, Computer Methods and Programs in Biomedicine, 81, 137-153, (2006)
[39] Tseitin, G. S. (1983). On the complexity of derivation in propositional calculus. In Automation of reasoning 2: Classical papers on computational logic 1967-1970 (pp. 466-483). Springer.
[40] van Hoeve, W. J. (2001). The alldifferent constraint: A survey. CoRR, cs.PL/0105015.
[41] Walsh, T. (2000). SAT vs CSP. In Dechter, R. (ed.), CP 2000, LNCS 1894 (pp. 441-456). Springer. · Zbl 1044.68808
[42] Xu, L; Hutter, F; Hoos, HH; Leyton-Brown, K, Satzilla: portfolio-based algorithm selection for SAT, Journal of Artificial Intelligence Research (JAIR), 32, 565-606, (2008) · Zbl 1182.68272
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.