Scarab: a SAT-based CP System
日本語ページはこちら．
Overview
This page details Scarab, a prototyping tool for developing SAT-based 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
- Download the latest jar (According to your Scala version select
appropriate one).
- (for Scala 2.12.*) use jars/scarab-v196-s212.jar
- (for Scala 2.11.*) use jars/scarab-v196-s211.jar
- (for Scala 2.10.*) use jars/scarab-v196-s210.jar
- For more detail (including source files), please refere the following Commit ID 30315e9 of https://github.com/TakehideSoh/Scarab
- 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._, dsl._ var n: Int = 5 for (i <- 0 until n; j <- 0 until n) int('x (i, j), 1, n) for (i <- 0 until n) { add(alldiff((0 until n).map(j => 'x (i, j)))) add(alldiff((0 until n).map(j => 'x (j, i)))) add(alldiff((0 until n).map(j => 'x (j, (i + j) % n)))) add(alldiff((0 until n).map(j => 'x (j, ((n - 1 + i - j)) % n)))) } if (find) for (i <- 0 until n) println((0 until n).map { j => solution.intMap('x (i, j)) }.mkString(" "))
- 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
- It will print the followings:
3 4 5 1 2 5 1 2 3 4 2 3 4 5 1 4 5 1 2 3 1 2 3 4 5
More resources
- you can find more examples “example” page.
- you can also find more documents “documents” page.
Note
- This software is distributed under the BSD License. See LICENSE file.
- scarab-<version>.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).
Publications
- Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
- 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 | SAT solver in Java, which Scarab adopts! |
| Sugar | SAT-based CSP Solver using order encoding. |
| Copris | Copris is a constraint programming DSL embedded in Scala. |
| It is also developed by our team! | |
| Numberjack | Constraint Programming System in Python |
| SCP | Constraint Programming in Scala using Z3 |
| scalasmt | SMT in Scala using Z3 |
| OscaR | OR in Scala |
| JaCoP | Constraint programming in Java and Scala |
| Choco | Constraint programming in Java |
| JSR 331 | Java Specification Requests: Constraint Programming API |
| BEE | a compiler which enables to encode finite domain constraint problems to CNF. |
| meSAT | Multiple Encodings of CSP to SAT |
Created: 2019-05-01 水 14:21