Sugar: a SAT-based Constraint Solver

Table of Contents

Overview

Sugar is a SAT-based Constraint Solver. Constraint Satisfaction Problem (CSP) is encoded to a Boolean CNF formula, and it is solved by an external SAT solver. Sugar also can solve Constraint Optimization Problems (COP) and Max-CSP. Sugar is an award winning solver of global constraint categories at the International CSP Solver Competitions in 2008 and 2009, and of four categories at the 2008 International Max-CSP Solver Competition. See the results of Sugar in CSP Solver Competitions for more details.

What's New

Description

Sugar is a SAT-based constraint solver based on a SAT-encoding method named order encoding {TamuraTKB09}. In the order encoding, a comparison \(x \le a\) (alternatively \(x \ge a\)) is encoded by a different Boolean variable for each integer variable \(x\) and integer value \(a\). It is an extension of the encoding method proposed by Crawford and Baker for the Job-shop scheduling problems {CrawfordB94} to the finite-domain linear CSP (Constraint Satisfaction Problems). This encoding is proved to translate some tractable CSP to tractable SAT by Petke and Jeavons in {PetkeJ11}. There are some important related works: totalizer by Bailleux and Boufkhad for encoding Boolean cardinality constraints {BailleuxB03}, regular encoding by Ansótegui and Manyà {AnsoteguiM04}, ladder encoding by Gent and Nightingale {GentN04}, and lazy clause generation by Ohrimenko, Stuckey, and Codish {OhrimenkoSC09}.

  • Sugar can solve COP (Constraint Optimization Problems) and Max-CSP in addition to CSP.
  • Sugar can handle problems written in abridged notation of XCSP 2.1 format used at the International CSP and Max-CSP Solver Competitions.
  • Various CSP instances in XCSP format can be found at Benchmarks in XCSP 2.1.
  • Sugar became a winner in GLOBAL categories of 2008 and 2009 CSP Solver Competitions. See Promoting robust black-box solvers through competitions by Christophe Lecoutre, Olivier Roussel, and M. R. C. van Dongen.

Download

  • Version 2.3.4 (released 2021-01-03 Sun)
  • Version 2.3.3 (released 2018-03-19 Mon)
  • Version 2.3.2 (released 2016-12-25 Sun)
  • Version 2.2.1 (released 2014-07-06 Sun)
  • Version 2.2.0 (released 2014-06-28 Sat)
  • Version 2.1.3 (released 2013-12-01 Sun)
  • Version 2.1.2 (released 2013-10-13 Sun)
  • Version 2.1.0 (released 2013-08-25 Sun)
  • Version 2.0.0 (released 2013-02-18 Mon)
  • Version 1.15.1 (released 2012-06-08 Fri)
  • Version 1.15.0 (released 2011-08-28 Sun)
  • Version 1.14.7 (released 2010-06-29 Tue)
  • Version 1.14.6 (released 2009-09-06 Sun)
    • package/sugar-v1-14-6.zip (579181 bytes, md5sum 11a0a7198913d793b4946c8726572a04)
    • This version is the final version submitted to all categories of the 2009 International CSP Solver Competition
  • Version 1.13 (released 2008-06-27 Fri)
    • package/sugar-v1-13.zip (525853 bytes, md5sum 12d917fdd5c579ac796d70d22148a44d)
    • This version is the final version submitted to all categories of the 2008 International CSP and Max-CSP Solver Competitions
  • Version 1.12 (released 2008-05-30 Fri)

Documents

Technical Papers and Presentations

When you want to refer to our work in your technical paper, please cite our published paper rather than just quoting the URL of this web page.

  • Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, Mutsunori Banbara: Compiling Finite Linear CSP into SAT, Constraints, Volume 14, Number 2, pp.254–272, June, 2009.
    DOI 10.1007/s10601-008-9061-0 (Open Access, You can freely download the paper)

Evaluation Results

Some evaluation results can be found at the web page of CSP2SAT which is an early implementation of order encoding.

Links

Related Projects

SAT-based CSP Solvers and Related Pages

SAT Solvers and Related Pages

References

  • [TamuraTKB09] Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear CSP into SAT, Constraints, 14(2):254-272, 2009.
  • [PetkeJ11] Justyna Petke and Peter Jeavons. The order encoding: From tractable CSP to tractable SAT. In Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011), LNCS 6695, pages 371-372, 2011.
  • [CrawfordB94] James M. Crawford and Andrew B. Baker. Experimental results on the application of satisfiability algorithms to scheduling problems. In Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pages 1092-1097, 1994.
  • [BailleuxB03] Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of Boolean cardinality constraints. In Proceedings of the 9th International Joint Conference on Principles and Practice of Constraint Programming (CP 2003), LNCS 2833, pages 108-122, 2003.
  • [AnsoteguiM04] Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables into problems with Boolean variables. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), LNCS 3542, pages 1-15, 2004.
  • [GentN04] I. P. Gent and P. Nightingale. A new encoding of alldifferent into SAT. In Proceedings of the 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2004.
  • [OhrimenkoSC09] O. Ohrimenko, P.J. Stuckey, and M. Codish. Propagation via lazy clause generation. Constraints, 14(3):357-391, 2009.

Date: 2021-01-04 02:26:46 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 25

Validate XHTML 1.0