Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Azucar: A SAT-Based CSP Solver Using Compact Order Encoding
(Tool Presentation)
verfasst von : Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara
Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2012
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.