Diet-Sugar
A SAT-based CSP Solver Equipped with Hybrid Encoding integrating Order and Log Encodings.

Overview

Diet-Sugar is a SAT-based CSP Solver based on the Sugar solver, so it adopts XCSP format input including global constraints.
It can also accept Sugar CSP format.

The most appealing feature of Diet-Sugar is it uses hybrid encoding integrating the order and log encoding, which allows us to solve CSPs that contains small domain sized variable to large domain sized variables.

XCSP or Sugar CSP format can be used as the input of Diet-Sugar.
```
$ sugar -hybrid -o hy* -solver PBSOLVER file.csp
```
The following hybrid options are currently available
- encode all variables by order encoding
  - sugar -hybrid -o hy0 -solver PBSOLVER file.csp
- endode all variables by log encoding
  - sugar -hybrid -o hy1 -solver PBSOLVER file.csp
- encode 0-1 variables by log encoding and others are by order encoding.
  - sugar -hybrid -o hy2 -solver PBSOLVER file.csp
- apply hybrid encoding according to domain sizes (0-1 variables are log-encoded)
  - sugar -hybrid -o hy3=<threshold> -solver PBSOLVER file.csp
- apply hybrid encoding according to domain products (variables in 0-1 comparisons are log-encoded)
  - sugar -hybrid -o hy8=<threshold> -solver PBSOLVER file.csp

Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), to appear, IEEE Computer Society, 2015.

Sat4j	SAT solver in Java, which Scarab adopts!
Sugar	SAT-based CSP Solver using order encoding.
Copris	Copris is a constraint programming DSL embedded in Scala.
	It is also developed by our team!
Scarab	SAT-based CP system in Scala which is tightly integrated with SAT solvers.
BEE	a compiler which enables to encode finite domain constraint problems to CNF.
Numberjack	Constraint Programming System in Python
SCP	Constraint Programming in Scala using Z3
scalasmt	SMT in Scala using Z3
OscaR	OR in Scala
JaCoP	Constraint programming in Java and Scala
Choco	Constraint programming in Java
JSR 331	Java Specification Requests: Constraint Programming API