Abstract
This paper describes a SAT-based CSP solver Azucar. Azucar solves a finite CSP by encoding it into a SAT instance using the compact order encoding and then solving the encoded SAT instance with an external SAT solver. In the compact order encoding, each integer variable is represented by using a numeral system of base B ≥ 2 and each digit is encoded by using the order encoding. Azucar is developed as a new version of an award-winning SAT-based CSP solver Sugar. Through some experiments, we confirmed Azucar can encode and solve very large domain sized CSP instances which Sugar can not encode, and shows better performance for Open-shop scheduling problems and the Cabinet problems of the CSP Solver Competition benchmark.
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.
Similar content being viewed by others
References
Rossi, F., van Beek, P., Walsh, T.: Handbook of Constraint Programming. Elsevier Science Inc. (2006)
Prestwich, S.D.: CNF encodings. In: Handbook of Satisfiability, pp. 75–97. IOS Press (2009)
Tamura, N., Tanjo, T., Banbara, M.: System description of a SAT-based CSP solver Sugar. In: Proceedings of the 3rd International CSP Solver Competition, pp. 71–75 (2008)
Huang, J.: Universal Booleanization of Constraint Models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144–158. Springer, Heidelberg (2008)
Le Berre, D., Lynce, I.: CSP2SAT4J: A simple CSP to SAT translator. In: Proceedings of the 2nd International CSP Solver Competition, pp. 43–54 (2008)
Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254–272 (2009)
Soh, T., Inoue, K., Tamura, N., Banbara, M., Nabeshima, H.: A SAT-based method for solving the two-dimensional strip packing problem. Fundamenta Informaticae 102(3-4), 467–487 (2010)
Banbara, M., Matsunaka, H., Tamura, N., Inoue, K.: Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 112–126. Springer, Heidelberg (2010)
Petke, J., Jeavons, P.: The Order Encoding: From Tractable CSP to Tractable SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 371–372. Springer, Heidelberg (2011)
Tanjo, T., Tamura, N., Banbara, M.: A Compact and Efficient SAT-Encoding of Finite Domain CSP. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 375–376. Springer, Heidelberg (2011)
Tanjo, T., Tamura, N., Banbara, M.: Proposal of a compact and efficient SAT encoding using a numeral system of any base. In: Proceedings of the 1st International Workshop on the Cross-Fertilization Between CSP and SAT, CSPSAT 2011 (2011)
Tanjo, T., Tamura, N., Banbara, M.: Towards a compact and efficient SAT-encoding of finite linear CSP. In: Proceedings of the 9th International Workshop on Constraint Modelling and Reformulation, ModRef 2010 (2010)
Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: Proceedings of the IFIP 13th World Computer Congress, pp. 253–258 (1994)
de Kleer, J.: A comparison of ATMS and CSP techniques. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 1989), pp. 290–296 (1989)
Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artificial Intelligence 45(3), 275–286 (1990)
Gavanelli, M.: The Log-Support Encoding of CSP into SAT. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 815–822. Springer, Heidelberg (2007)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7(2–3), 56–64 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tanjo, T., Tamura, N., Banbara, M. (2012). Azucar: A SAT-Based CSP Solver Using Compact Order Encoding. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_37
Download citation
DOI: https://doi.org/10.1007/978-3-642-31612-8_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31611-1
Online ISBN: 978-3-642-31612-8
eBook Packages: Computer ScienceComputer Science (R0)