Copris: Constraint Programming in Scala

Table of Contents

Overview

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

It uses Sugar as a default back-end constraint solver which is an award-winning solver in global categories of 2008 and 2009 International CSP Solver Competitions.

You can also use SMT solvers supporting QF_LIA theory (such as Z3) and JSR 331 solvers (such as Choco) from Copris.

copris.png

What's New

  • 2021-01-03 Sun Release of version 2.3.2.
  • 2019-03-18 Mon Release of version 2.3.1.
  • 2018-03-19 Mon Release of version 2.2.8.
  • 2014-07-06 Sun Release of version 2.2.5.
  • 2013-12-01 Sun Release of version 2.2.4.
  • 2013-10-13 Sun Release of version 2.2.2 which runs on Scala 2.10.3
  • 2013-09-10 Tue
  • 2013-09-01 Sun Release of version 2.2.0.
  • 2013-09-01 Sun "Puzzle Solvers in Copris" page is released.
  • 2013-08-25 Sun Release of version 2.1.0. Sugar version 2.1.0 and Sat4j verion 2.3.5 are included in the Copris package. Thanks to Sat4j team!
  • 2013-02-18 Mon Release of version 2.0.0. Sat4j verion 2.3.3 is now included in Copris package. Thanks to Sat4j team!
  • 2013-02-16 Sat First release of Nonogram Solver in Copris.
  • 2013-02-01 Fri We released Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems which can be used as a tiny version of Copris for proptotyping.

Examples

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:  }

Requirements

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

  • Java JRE: Java JRE 8 or higher
  • Scala: Scala version 2.12
    • Other Scala versions are not binary compatible with version 2.12. You need to compile Copris from the source when you want to run it on these versions.
  • Sugar: Copris uses Sugar (a SAT-based Constraint Solver) 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. Jar file of Sat4j is included in Copris package. If you want to use SAT solver other than Sat4j, please install at least one of the followings.

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.

Downloads

How to install Copris

  1. Check the version of your Scala 
    $ scala -version
Scala code runner version 2.12.5 -- Copyright 2002-2018, LAMP/EPFL and Lightbend, Inc.

    Copris can run on Scala version 2.12 (not on other versions).

  2. Clone the git repository 
    $ git clone https://gitlab.com/cspsat/prog-copris.git
  3. Move to Copris examples directory 
    $ cd prog-copris/examples
  4. Compile Examples.scala 
    # Mac OS X, Linux
$ scalac -cp ../build/copris-all_2.12-2.3.2.jar Examples.scala

# Windows
> scalac -cp ..\build\copris-all_2.12-2.3.2.jar Examples.scala
  5. Run the program 
    # Mac OS X, Linux
$ scala -cp .:../build/copris-all_2.12-2.3.2.jar FirstStep
Solution(Map(x -> 4, y -> 3),Map())

# Windows
> scala -cp .;..\build\copris-all_{2.12-2.3.2.jar FirstStep
Solution(Map(x -> 4, y -> 3),Map())

Using Copris in Scala REPL

You can use Copris in Scala REPL as follows. 

$ scala -cp ../build/copris-all_2.12-2.3.2.jar
Welcome to Scala version 2.10.3 (OpenJDK 64-Bit Server VM, Java 1.7.0_65).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import jp.kobe_u.copris._
import jp.kobe_u.copris._

scala> import jp.kobe_u.copris.dsl._
import jp.kobe_u.copris.dsl._

scala> int('x, 0, 7)
res0: jp.kobe_u.copris.Var = x

scala> int('y, 0, 7)
res1: jp.kobe_u.copris.Var = y

scala> add('x + 'y === 7)

scala> add('x * 2 + 'y * 4 === 20)

scala> find
res4: Boolean = true

scala> solution
res5: jp.kobe_u.copris.Solution = Solution(Map(x -> 4, y -> 3),Map())

Documents

Documents in Japanese

  • Introduction to Constraint Programming in Copris (in Japanese, HTML, PDF)
  • Naoyuki Tamura, Tomoya Tanjo, and Mutsunori Banbara: "Domain-Specific Language Copris for Constraint Programming in Scala" (in Japanese, J-Stage)
  • Naoyuki Tamura, Tomoya Tanjo, and Mutsunori Banbara: "A SAT-based constraint solver Sugar and its Scala interface" (in Japanese, PDF slide)

License

This software is distributed under the BSD 3-Clause License.

Related projects

Links

Date: 2021-01-04 02:26:44 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 25

Validate XHTML 1.0