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\) のマス目に
記入する問題です.但し,以下の制約を満たす必要があります.
- 各行,各列,各汎対角線において,全ての数字がちょうど一回だけ表 れる.
- 汎対角線ラテン方陣問題は \(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
- 実行後,以下が出力されるはずです.
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
その他の情報
- Scarab のプログラム例についてはこちらを御覧ください “example” page.
- Scarab のドキュメントについてはこちらを御覧ください “documents” page.
リリースノート
- 英語ページを参照してください.
論文
- 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.