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._ ; 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

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

Release Note

<2019-02-11 月> Organize web materials.
See history until 2016 here.

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