Java Scala Other
Switch branches/tags
Nothing to show
Clone or download
soh
Latest commit 64f49b3 May 26, 2018

README.md

<script type="text/javascript"> var _gaq = _gaq || []; _gaq.push(['_setAccount', 'UA-6313627-2']); _gaq.push(['_trackPageview']); (function() { var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true; ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js'; var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s); })(); </script>
Home Examples Documents Advanced Usage Apps

Overview

This page details Scarab, a prototyping tool for developing SAT-based CP systems. Features of Scarab are follows:

  • Expressiveness Rich constraint modeling language.
  • Efficiency Optimized order encoding and native handling of BC/PB on Sat4j.
  • Customizability Its core part is written in around 1000 lines of Scala.
  • Portability Run on JVM.

How to use it

img

  • Write your own Scarab program. For instance, let’s write a program solving Pandiagonal Latin Square PLS(n).
    • a problem of placing different (n) numbers into (n \times n) matrix
    • such that each number is occurring exactly once
    • for each row, column, diagonally down right, and diagonally up right.

import jp.kobe_u.scarab._
import dsl._

var n: Int = 5
for (i <- 1 to n; j <- 1 to n)  int('x(i,j),1,n) 
for (i <- 1 to n) {
  add(alldiff((1 to n).map(j => 'x(i,j))))
  add(alldiff((1 to n).map(j => 'x(j,i))))
  add(alldiff((1 to n).map(j => 'x(j,(i+j-1)%n+1))))
  add(alldiff((1 to n).map(j => 'x(j,(i+(j-1)*(n-1))%n+1))))}

if (find)  println(solution.intMap)
  • Sava this program as pls.sc.

  • To run pls.sc, just execute it as follows, that’s all !

    scala -cp scarab-$VERSION.jar pls.sc

More resources

Note

  • This software is distributed under the BSD License. See LICENSE file.
  • scarab-.jar includes Sat4j package and Sugar for the ease of use.
    • We really appreciate the developers of Sat4j and Sugar!
    • Sat4j used for inference engine.
    • Sugar used for preprocessor (from 1.5.4).

Release Note

  • [2015.11.01] Sat4j and Sat4j-PB (Rev2428) are included.

  • [2015.06.14] ZIP of Scarab Package – Version 1.6.9 is released.

    • changes will be updated soon.
  • [2015.05.25] JAR of Scarab – Version 1.6.8 is released.

    • changes will be updated soon.
  • [2015.02.08] JAR of Scarab – Version 1.5.7 is released.

    • To run this version, Scala 2.11.* or higher is required.
    • Addition of new functions.
      • UNSAT Core dectection in CSP level.
      • Nested commit.
      • Built-in optimization function.
    • Refactoring for some parts.
  • [2015.01.09] JAR of Scarab – Version 1.5.6 is released.

    • To run this version, Scala 2.11.* or higher is required.
    • Support non-contiguous domain.
    • Performance improvement.
      • Order Encoding Module is tuned.
      • Native PB Constraint is tuned.
  • See history until 2014 here.

Publications

  • Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (Tool Paper)
    • Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
    • In the Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), LNCS 7962, pp. 429-436, 2013.
  • System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems
    • Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stéphanie Roussel
    • In the Proceedings of Pragmatics of SAT 2013 (PoS-13), 14 pages, July 2013.

Links for Related Tool

[Sat4j](http://www.sat4j.org) SAT solver in Java, which Scarab adopts!
[Sugar](http://bach.istc.kobe-u.ac.jp/sugar/) SAT-based CSP Solver using order encoding.
[Copris](http://bach.istc.kobe-u.ac.jp/copris/) Copris is a constraint programming DSL embedded in Scala.
  It is also developed by our team!
[Numberjack](http://numberjack.ucc.ie) Constraint Programming System in Python
[SCP](http://lara.epfl.ch/web2010/scp) Constraint Programming in Scala using Z3
[scalasmt](http://code.google.com/p/scalasmt/) SMT in Scala using Z3
[OscaR](https://bitbucket.org/oscarlib/oscar) OR in Scala
[JaCoP](http://jacop.osolpro.com/) Constraint programming in Java and Scala
[Choco](http://www.emn.fr/x-info/choco-solver/) Constraint programming in Java
[JSR 331](http://jcp.org/en/jsr/detail?id%3D331) Java Specification Requests: Constraint Programming API
[BEE](http://amit.metodi.me/research/bee/) a compiler which enables to encode finite domain constraint problems to CNF.