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


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

Experimental Evaluation



  • 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


A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings

  • 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

Author: Takehide Soh

Created: 2016-03-27 日 11:08

Emacs 24.3.1 (Org mode 8.2.10)