| Home | Examples | Documents | Advanced Usage | Apps |
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.
- Download the latest version.
- 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
- you can find more examples “example” page.
- you can also find more documents “documents” page.
- 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).
-
[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.
- 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.
| [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. |