Copris: Constraint Programming in Scala

Copris provides a constraint programming DSL (Domain-Specific Language) embedded in Scala language.

The following is an example program using Copris.

 1:  import jp.kobe_u.copris._
 2:  import jp.kobe_u.copris.dsl._
 3:  
 4:  object FirstStep {
 5:    def main(args: Array[String]) = {
 6:      val x = int('x, 0, 7)
 7:      val y = int('y, 0, 7)
 8:      add(x + y === 7)
 9:      add(x * 2 + y * 4 === 20)
10:      if (find) {
11:        println(solution)
12:      }
13:    }
14:  }

• The sixth line declares a CSP variable x ∈ {0,1,2,…,7}, and assigns it to the Scala variable x.
• The seventh line declares a CSP variable y ∈ {0,1,2,…,7}, and assigns it to the Scala variable y.
• The eighth line adds a CSP constraint x + y = 7.
• The ninth line adds a CSP constraint 2x + 4y = 20.
• The tenth line finds a first solution, and the next line displays the solution as follows.

  Solution(Map(x -> 4, y -> 3),Map())
  

• Java JRE: Java JRE 6 or higher
• Scala: Scala version 2.9 or higher
• Sugar: Copris uses Sugar (A SAT-based Constraint Solver) version 1.15 or higher as a default constraint solver. It is included in Copris package.
• SAT solver: Sugar is a SAT-based Constraint solver, therefore it requires a SAT solver to be installed. Please install at least one of the followings.
  • Sat4j core (Java based)
  • MiniSat
  • PrecoSAT
  • glucose
  • GlueMiniSat
  • Any other SAT solver participated to SAT competitions

Here are some remarks how to choose SAT solver.

• We recommend to use SAT solvers which have a good performance on the Application category in SAT competitions.
• Sat4j is a Java-based SAT solver, therefore it is called from Copris through Java API, and there are no overheads of process invocation. However it maybe two or three times slower than other SAT solvers.
• SAT solvers other than Sat4j is invoked as an external process from Copris, and therefore there are some overheads of external process invocation. However they are usually much faster, and suitable to solver difficult problems.

• copris-v1-0-0.zip (version 1.0.0, released 2011-08-28 Sun)

1. Download Copris package

   $ wget http://bach.istc.kobe-u.ac.jp/copris/copris-v1-0-0.zip
   

2. Unzip Copris package

   $ unzip copris-v1-0-0.zip
   

3. Download Sat4j core package from Sat4j web page
4. Unzip Sat4j core package

   $ unzip sat4j-core-v20110329.zip
   

5. Copy Sat4j core jar file to Copris library directory

   $ cp org.sat4j.core.jar copris-v1-0-0/lib
   

6. Move to Copris examples directory

   $ cd copris-v1-0-0/examples
   

7. Compile Examples.scala

   $ ./coprisc Examples.scala
   

   The coprisc command just invokes Scala compiler with class path setting. You can directly compile the program as follows.

   $ scalac -cp ../lib/copris-v1-0-0.jar:../lib/sugar-v1-15-0.jar:../lib/org.sat4j.core.jar -d classes Examples.scala
   

8. Run the program

   $ ./copris FirstStep
   

   The copris command just invokes Scala with class path setting. You can directly run the program as follows.

   $ scala -cp classes:../lib/copris-v1-0-0.jar:../lib/sugar-v1-15-0.jar:../lib/org.sat4j.core.jar FirstStep
   

• Copris API (version 1.0.0)
• Naoyuki Tamura, Tomoya Tanjo, and Mutsunori Banbara: "A SAT-based constraint solver Sugar and its Scala interface" (in Japanese, PDF)
• Papers/presentations on Sugar

This software is distributed under the BSD Lincense.

• Sugar: A SAT-based Constraint Solver
• Cream: Class Library for Constraint Programming in Java