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

[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.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
  • 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
  • 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

1. 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)
2. Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, Mutsunori Banbara: Compiling Finite Linear CSP into SAT, CP'06
   • The number of clauses O(d²)+O(md) appeared in page 596 of the CP'06 proceedings is wrong. We corrected the number to O(m d²) in in the above PDF document.
3. Naoyuki Tamura and Mutsunori Banbara: Sugar: A CSP to SAT Translator Based on Order Encoding,
   in Proceedings of the Second International CSP Solver Competition
4. N. Tamura, A. Taga, M. Banbara, T. Soh, H. Nabeshima, and K. Inoue: Solving Shop Scheduling Problems by SAT encoding, Scheduling Symposium 2007 (in Japanese)
5. Naoyuki Tamura, Tomoya Tanjo, and Mutsunori Banbara: System Description of a SAT-based CSP Solver Sugar,
   in Proceedings of the Third International CSP Solver Competition
   • presentation slides
6. Tomoya Tanjo, Naoyuki Tamura, and Mutsunori Banbara: Sugar++: A SAT-based Max-CSP/COP Solver,
   in Proceedings of the Third International CSP Solver Competition
   • presentation slides

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: Tue Jun 29 13:45:38 2010 JST ,    Since Feb 22, 2008 )