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. © 2012 Springer-Verlag.
CITATION STYLE
Tanjo, T., Tamura, N., & Banbara, M. (2012). Azucar: A SAT-based CSP solver using compact order encoding (Tool presentation). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 456–462). https://doi.org/10.1007/978-3-642-31612-8_37
Mendeley helps you to discover research relevant for your work.