Scarab: a SAT-based CP Systems

日本語ページはこちら

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

image

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

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

Author: Takehide Soh

Created: 2016-07-03 日 18:02

Validate