概要
このページではSAT型システムのためのツール (SAT型制約プログラミングシステム) Scarab について説明します．Scarab の特長は以下になります:
- 表現性 制約記述のためのドメイン固有言語と汎用プログラミング言語で あるScalaの両方を用いて，与えられた問題を記述することが可能である．
- 効率性 対数符号化，最適化された順序符号化，組込みのBC/PB制約を用い て問題を符号化し，SATソルバーSat4jを使って解くという点で効率的である．
- 拡張性 \scarab のソースコードは全体で1000行ほどであり， ユーザが \scarab 自身を拡張することが可能．
- 可搬性 Sat4j と共に Java 仮想マシン上で動きます．
使い方
- 使用している Scala のバージョンに応じて，以下から適切な jar を選択
してダウンローそしてください．
- (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
- ソース・ファイルを含む全ての情報は
https://github.com/TakehideSoh/Scarab の以下のコミット番号を参照してください．
- 30315e9
- Scarab プログラムを書きます．例として，汎対角線ラテン方陣 PLS(n)
を解くことを考えます．
- 汎対角線ラテン方陣問題は \(n\) 個の数字を \(n \times n\) のマス目に
記入する問題です．但し，以下の制約を満たす必要があります．
- 各行，各列，各汎対角線において，全ての数字がちょうど一回だけ表 れる．
- 汎対角線ラテン方陣問題は \(n\) 個の数字を \(n \times n\) のマス目に
記入する問題です．但し，以下の制約を満たす必要があります．
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)
- 上記のプログラム pls.sc として保存してください．
- pls.sc を実行するには以下のコマンドを実行するだけです!
scala -cp scarab<$version>.jar pls.sc
その他の情報
- 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.