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)
- 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)
- Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, Mutsunori Banbara:
Compiling Finite Linear CSP into SAT,
CP'06
- The number of clauses O(d2)+O(md) appeared in
page 596 of the CP'06 proceedings is wrong.
We corrected the number to O(m d2) in
in the above PDF document.
- Naoyuki Tamura and Mutsunori Banbara:
Sugar: A CSP to SAT Translator Based on Order Encoding,
in
Proceedings of the Second International CSP Solver Competition
- 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)
- 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
- Tomoya Tanjo, Naoyuki Tamura, and Mutsunori Banbara:
Sugar++: A SAT-based Max-CSP/COP Solver,
in
Proceedings of the Third International CSP Solver Competition
Related Projects
Links
- SAT Solvers
- International CSP Solver Competition
Naoyuki Tamura
(
Last modified: Tue Jun 29 13:45:38 2010 JST
,
Since Feb 22, 2008
)