# 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

• 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


### Note

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