Copris: Constraint Programming in Scala

Copris provides a constraint programming DSL (Domain-Specific Language) embedded in Scala language. It uses Sugar as a constraint solver. Sugar an award-winning solver in global categories of 2008 and 2009 International CSP Solver Competitions.

The following is an example program using Copris.

 1:  object FirstStep {
 2:    import jp.kobe_u.copris._
 3:    import jp.kobe_u.copris.dsl._
 4:  
 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())
  

The following is an example program of solving 8-Queens. Don't you think it is very simple?

 1:  object Queens {
 2:    import jp.kobe_u.copris._; import jp.kobe_u.copris.dsl._
 3:    def queens(n: Int) = {
 4:      for (i <- 1 to n) int('q(i), 1, n)
 5:      add(Alldifferent((1 to n).map(i => 'q(i))))
 6:      add(Alldifferent((1 to n).map(i => 'q(i) + i)))
 7:      add(Alldifferent((1 to n).map(i => 'q(i) - i)))
 8:      if (find) {
 9:        do {
10:          println(solution)
11:        } while (findNext)
12:      }
13:    }
14:    def main(args: Array[String]) =
15:      queens(8)
16:  }

The following is an example program of solving a Sudoku puzzle.

 1:  object Sudoku {
 2:    import jp.kobe_u.copris._; import jp.kobe_u.copris.dsl._
 3:    def solve(m: Int, n: Int, puzzle: Seq[Seq[Int]]) = {
 4:      for (i <- 0 until n; j <- 0 until n)
 5:        int('x(i,j), 1, n)
 6:      for (i <- 0 until n)
 7:        add(Alldifferent((0 until n).map('x(i,_))))
 8:      for (j <- 0 until n)
 9:        add(Alldifferent((0 until n).map('x(_,j))))
10:      for (i <- 0 until n by m; j <- 0 until n by m) {
11:        val xs = for (di <- 0 until m; dj <- 0 until m) yield 'x(i+di,j+dj)
12:        add(Alldifferent(xs))
13:      }
14:      for (i <- 0 until n; j <- 0 until n; if puzzle(i)(j) > 0)
15:        add('x(i,j) === puzzle(i)(j))
16:      if (find) {
17:        for (i <- 0 until n)
18:          println((0 until n).map(j => solution('x(i,j))).mkString(" "))
19:      }
20:    }
21:    def main(args: Array[String]) = {
22:      /* http://puzzle.gr.jp */
23:      val puzzle = Seq(
24:        Seq(0, 0, 0, 0, 0, 0, 0, 0, 0),
25:        Seq(0, 4, 3, 0, 0, 0, 6, 7, 0),
26:        Seq(5, 0, 0, 4, 0, 2, 0, 0, 8),
27:        Seq(8, 0, 0, 0, 6, 0, 0, 0, 1),
28:        Seq(2, 0, 0, 0, 0, 0, 0, 0, 5),
29:        Seq(0, 5, 0, 0, 0, 0, 0, 4, 0),
30:        Seq(0, 0, 6, 0, 0, 0, 7, 0, 0),
31:        Seq(0, 0, 0, 5, 0, 1, 0, 0, 0),
32:        Seq(0, 0, 0, 0, 8, 0, 0, 0, 0))
33:      solve(3, 9, puzzle)
34:    }
35:  }

See Examples.scala for more examples.

When using Sat4j as a backend SAT solver, everything runs on JVM (Java Virtual Machine).

• 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 (default)
  • 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 recent SAT competitions or SAT races.
• Sat4j is a Java-based SAT solver, therefore it is directly called from Copris through Java API, and there are no overheads of process invocation. Sat4j is a good choice for many cases. 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, any of the SAT solvers listed above is a good choice to solve difficult problems.
• In many cases, enabling simplification preprocessing causes a small speed-down of solving. For example, please use MiniSat core instead of MiniSat simp.

• copris-v1-0-1.zip (version 1.0.1, released 2011-09-11 Sun)
  • See LICENSE and CHANGES
• 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-1.zip
   

2. Unzip Copris package

   $ unzip copris-v1-0-1.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-1/lib
   

6. Move to Copris examples directory

   $ cd copris-v1-0-1/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-1.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-1.jar:../lib/sugar-v1-15-0.jar:../lib/org.sat4j.core.jar FirstStep
   

• Copris API
• 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 License. See LICENSE file.

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

• Sat4j (SAT solver in Java)
• Kaplan (Constraint Programming in Scala)
• Asteroid (A Constraint-Based Local Search Engine written in Scala)
• Scampi (Scala Mathematical Programming Interface)
• JaCoP (Constraint programming in Java and Scala)
• Choco (Constraint programming in Java)
• JSR 331 (Java Specification Requests: Constraint Programming API)
  Using JSR 331 conformant solver from Copris is a future plan.
• Numberjack (Constraint programming in Python)
• scalasmt (SMT in Scala)