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

概要

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

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

使い方

image

  • Scarab プログラムを書きます.例として,汎対角線ラテン方陣 PLS(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.

ライセンス

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

リリースノート

論文

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

Author: 宋 剛秀 (SOH Takehide)

Created: 2016-02-19 金 09:11

Emacs 24.3.1 (Org mode 8.2.10)

Validate