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

Scarab の日本語のページ.

概要

このページでは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._, 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.

ライセンス

  • このソフトウェアは 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.

Author: 宋 剛秀 (SOH Takehide)

Created: 2019-05-09 木 16:34

Validate