Copris: Constraint Programming in Scala

Table of Contents

Overview

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())
    

Requirements

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

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.

Downloads

How to use Copris

  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
    

Documents

License

This software is distributed under the BSD Lincense.

Links

Author: Naoyuki Tamura

Date: 2011-08-28 12:25:06 JST

HTML generated by org-mode 7.3 in emacs 23