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)
- Version 1.13 (released June 27, 2008)
- Version 1.12 (released May 30, 2008)
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.
- 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
Links
- SAT Solvers
- International CSP Solver Competition
Naoyuki Tamura
(
Last modified: Sun Nov 13 18:18:05 2011 JST
,
Since Feb 22, 2008
)