Azucar: A SAT-Based CSP Solver Using Compact Order Encoding. 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.

References in zbMATH (referenced in 5 articles )

Showing results 1 to 5 of 5.
Sorted by year (citations)

  1. Surynek, Pavel: Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems (2017)
  2. Bischl, Bernd; Kerschke, Pascal; Kotthoff, Lars; Lindauer, Marius; Malitsky, Yuri; Fréchette, Alexandre; Hoos, Holger; Hutter, Frank; Leyton-Brown, Kevin; Tierney, Kevin; Vanschoren, Joaquin: ASlib: a benchmark library for algorithm selection (2016)
  3. Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014) ioport
  4. Stojadinović, Mirko; Marić, Filip: meSAT: multiple encodings of CSP to SAT (2014)
  5. Tanjo, Tomoya; Tamura, Naoyuki; Banbara, Mutsunori: Azucar: a SAT-based CSP solver using compact order encoding (tool presentation) (2012) ioport