Scarab: SAT型制約プログラミングシステム

Scarab の日本語のページ.

概要

このページではSAT型システムのためのツール (SAT型制約プログラミングシステム) Scarab について説明します．Scarab の特長は以下になります:

表現性 制約記述のためのドメイン固有言語と汎用プログラミング言語であるScalaの両方を用いて，与えられた問題を記述することが可能である．
効率性 対数符号化，最適化された順序符号化，組込みのBC/PB制約を用いて問題を符号化し，SATソルバーSat4jを使って解くという点で効率的である．
拡張性 \scarab のソースコードは全体で1000行ほどであり，ユーザが \scarab 自身を拡張することが可能．
可搬性 Sat4j と共に Java 仮想マシン上で動きます．

使い方

使用している Scala のバージョンに応じて，以下から適切な jar を選択してダウンローそしてください．
- (for Scala 2.12.*) use scarab-v196-s212.jar
- (for Scala 2.11.*) use scarab-v196-s211.jar
- (for Scala 2.10.*) use scarab-v196-s210.jar
ソース・ファイルを含む全ての情報は https://github.com/TakehideSoh/Scarab の以下のコミット番号を参照してください．
- 30315e9

Scarab プログラムを書きます．例として，汎対角線ラテン方陣 PLS(n) を解くことを考えます．
- 汎対角線ラテン方陣問題は \(n\) 個の数字を \(n \times n\) のマス目に記入する問題です．但し，以下の制約を満たす必要があります．
  - 各行，各列，各汎対角線において，全ての数字がちょうど一回だけ表れる．

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(" "))

上記のプログラム pls.sc として保存してください．
pls.sc を実行するには以下のコマンドを実行するだけです!

scala -cp scarab<$version>.jar pls.sc

実行後，以下が出力されるはずです．

その他の情報

Scarab のプログラム例についてはこちらを御覧ください “example” page.
Scarab のドキュメントについてはこちらを御覧ください “documents” page.

ライセンス

このソフトウェアは BSD ライセンスで配布されます．詳細は LICENSE ファイルをご覧ください．
scarab-<version>.jar は Sat4j パッケージを含んでいます．

リリースノート

英語ページを参照してください．

論文

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.