Sugar: A SAT-based Constraint Solver

Overview

Sugar is a SAT-based constraint solver based on a new SAT-encoding method named "order encoding". In the order encoding, a comparison x <= 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 to the finite-domain linear CSP (Constraint Satisfaction Problems).

• 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 obtained from Benchmarks in XCSP 2.1.

News

[Aug. 28, 2011]

Sugar version 1.15.0 and Copris (Constraint Programming in Scala) version 1.0.0 are released.

[Oct. 2, 2009]

Sugar version 1.14.6 became the winner in 3 categories out of 7 categories of the 2009 Fourth International CSP Solver Competition. See the results page for more details.

[Sep. 6, 2009]

Sugar version 1.14.6 is released.

[Sep. 22, 2008]

Sugar version 1.13 became the winner in 4 categories out of 10 categories of the 2008 Third International CSP and Max-CSP Solver Competitions. See the results page for more details.

Download

• Version 1.15.0 (released August 28, 2011)
  • sugar-v1-15-0.zip (602728 byte, md5sum be1fbb7e7b15b8aa52db507e56720bda)
  • Requirements: MiniSat or PicoSAT or PrecoSAT, Perl 5, Java 1.6
    Please use Perl 5.11 or lower. The behavior of split function is changed in Perl 5.12. We will fix the problem in the next release.
  • README, CHANGES, LICENSE (This software is distributed under the BSD Lincense)
  • CSP examples and Tool programs: including Job-Shop Scheduling Problems, Open-Shop Scheduling Problems, Two-dimensional Strip Packing Problems, Golomb ruler, Magic Squares, N-Queens Problem, Cryptarithmetic puzzles, Knight's Tour, Social Golfer Problems, etc.
  • Copris (Constraint Programming in Scala) is now avaiable as a separate package.
• Version 1.14.7 (released June 29, 2010)
  • sugar-v1-14-7.zip (580920 byte, md5sum 0960ddb011f8ea59f86a5b39832eab2d)
  • Requirements: MiniSat or PicoSAT or PrecoSAT, Perl 5, Java 1.6
    Please use Perl 5.11 or lower. The behavior of split function is changed in Perl 5.12. We will fix the problem in the next release.
  • README, CHANGES, LICENSE (This software is distributed under the BSD Lincense)
  • CSP examples and Tool programs: including Job-Shop Scheduling Problems, Open-Shop Scheduling Problems, Two-dimensional Strip Packing Problems, Golomb ruler, Magic Squares, N-Queens Problem, Cryptarithmetic puzzles, Knight's Tour, Social Golfer Problems, etc.
• Version 1.14.6 (released September 6, 2009)
  • sugar-v1-14-6.zip (579181 byte, md5sum 11a0a7198913d793b4946c8726572a04)
  • Requirements: MiniSat or PicoSAT, Perl 5, Java 1.5 or 1.6
    Please use Perl 5.11 or lower. The behavior of split function is changed in Perl 5.12. We will fix the problem in the next release.
  • README, CHANGES, LICENSE (This software is distributed under the BSD Lincense)
  • CSP examples and Tool programs: including Job-Shop Scheduling Problems, Open-Shop Scheduling Problems, Two-dimensional Strip Packing Problems, Golomb ruler, Magic Squares, N-Queens Problem, Cryptarithmetic puzzles, Knight's Tour, Social Golfer Problems, etc.
  • This version is the final version submitted to all categories of the CSP and Max-CSP competitions in the Fourth International CSP Solver Competition.
• Version 1.14 alpha1 experimental version (released July 8, 2008)
  • sugar-v1-14alpha1.zip (535156 byte, md5sum a773096569f06882f37318dab25e3eb2)
• Version 1.13 (released June 27, 2008)
  • sugar-v1-13.zip (525853 byte, md5sum 12d917fdd5c579ac796d70d22148a44d)
  • This version is the final version submitted to all categories of the CSP and Max-CSP competitions in the Third International CSP Solver Competition.
• Version 1.12 (released May 30, 2008)
  • sugar-v1-12.zip (524408 bytes, md5sum 4da26a467bdc3ed3f299c6d8fe295be4)

Documents

• Syntax of Sugar CSP
• Using Sugar on Microsoft Windows with Cygwin
• Using Sugar on Microsoft Windows with Cygwin (in Japanese)
• Solving Puzzles with Sugar Constraint Solver (in Japanese)
  Sudoku, Kakuro (Cross Sums), Akari (Light Up), Shikaku, Number Link, Masyu, Slitherlink, Nurikabe, Hashiwokakero, Hitori, Fillomino, Heyawake, Masyu, Nonogram, etc.

Technical Papers and Presentation Slides

• 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)
• Papers/presentations on Sugar
• Papers/presentations on Sugar and SAT (including Japanese)

Related Projects

• Cream: Class Library for Constraint Programming in Java
• CSPSAT Project (2008--, in Japanese)
• HECS Project (2002--2003, in Japanese)

Links

• SAT Solvers
  • MiniSat
  • PicoSAT
• International CSP Solver Competition
  • 2009 Fourth International Constraint Solver Competition (Results)
  • 2008 Third International CSP Solver Competition (Results)
  • 2006 Second International CSP Solver Competition (Results)
  • 2005 First International CSP Solver Competition (Results)
  • Benchmarks

( Last modified: Sun Nov 13 18:18:05 2011 JST ,    Since Feb 22, 2008 )