| English | Japanese | CSPSAT (until FY2011) |
|
| ニュース | プロジェクト概要 | 講演会 ＆研究会 |
研究成果物 (論文・ソフトウェア等) |
プロジェクト概要
近年，高性能な推論を必要とする種々の分野において，命題論理の推論手法で あるSAT技術の利用が大きな成功を収めている．本プロジェクト（CSPSAT2）の前身であるCSPSATプロジェクトではSAT技術を制約充足問題に適用する研究を進め，世界最高速の制約プログラミングシステムを実現するなど世界トップクラスの研究成果を得た．本プロジェクトは，このSAT型制約プログラミングシステムの研究開発を発展させ，ソフト制約への対応，動的な制約の追加・削除への対応，実数ドメイン上や記号ドメイン上の制約への対応などを行い，高性能かつ柔軟な制約プログラミングシステムを実現するものであり，既存SAT技術では解くことが困難あるいは不可能だった応用に対し高性能な推論基盤を提供することが目的である．この意味で，本プロジェクトはSATおよび制約プログラミングに関する技術を大きく発展させるものと位置づけられる．
背景
制約充足問題および制約最適化問題（以下まとめてCSPと呼ぶ） は，与えられた制約条件を満たす解あるいは最適解を探索する問題である．制約プログラミングシステムは，CSPの記述言語（制約モデリング言語）およびそれを求解するソルバー（制約ソルバー）からなるソフトウェアシステムである．制約プログラミング（CP）システムは，国内での研究開発は活発ではないが，欧米を中心として様々な産業分野に応用されている．例えば，サッカーのJリーグの対戦スケジュールは，IBM社のILOGCP上で開発されている．CSPSATプロジェクトではSAT技術を用いたSAT型制約プログラミングシステムであるSugarを開発し，後述のように既存の制約プログラミングシステムを凌ぐ世界最高速の性能を得た．Sugarは，与えられたCSPをSATに符号化（encode）した後，高速なSATソルバーを用いて解を探索し，SATソルバーの解から元のCSPの解を得る方法を用いている．Sugarに代表されるSAT型制約プログラミングシステムは，SAT技術の発展に裏付けられ，CSPの求解に関して高い性能を実現しているが，以下のような限界も存在していた．
- フレキシブル制約への対応: 必ずしも満たさなくて良いソフト制約への対応が不十分である．
- 動的な制約変更への対応: 動的な制約の追加や削除への対応がなされていない．
- ドメインの拡張: 実数や記号等の整数以外のドメインへの対応がなされていない．
- 動的な制約変更への対応: 動的な制約の追加や削除への対応がなされていない．
具体的な研究テーマ (予定)
上記に挙げたSAT型制約プログラミングシステムの限界を乗り越える ために，本プロジェクトでは以下の研究テーマに取り組む．
- A．フレキシブル制約への対応
- Max-CSP の SAT 符号化
- 重み付き CSP の SAT 符号化
- インクリメンタル解法の導入
- 重み付き CSP の SAT 符号化
- B．動的制約変更への対応
- 制約の追加・削除への対応
- インクリメンタル解法の導入
- C．ドメインの拡張
- 実数ドメイン
- 記号ドメイン
- D．応用
- 混合整数計画問題 (MIP)
- システム検証
- プランニング問題
- スケジューリング問題
- システム生物学
- システム検証
学術的な特色
SAT技術は既に推論基盤として広く利用され，国内外の大学や企業で活発に研究・応用が進められている． CSPSATプロジェクトでは，これらのSAT技術の発展を背景としてSAT型制約プログラミングシステムの開発を行い，既存のものを超える世界最高速の制約プログラミングシステムを実現した．本研究は，このSAT型制約プログラミングシステムの研究開発を発展させ，ソフト制約への対応，動的な制約の追加・削除への対応，実数ドメイン上や記号ドメイン上の制約への対応などを行い，高性能かつ柔軟な制約プログラミングシステムを実現するものであり，既存SAT技術では解くことが困難あるいは不可能だった応用に対し高性能な推論基盤を提供することが可能となる．たとえば，ソフト制約への対応，動的な制約の追加・削除への対応，実数上の制約への対応などである．この意味で，本プロジェクトはSATおよび制約プログラミングに関する技術を大きく発展させるものと位置づけられる．また，制約プログラミングシステムは，すでに多くの実際的な応用が存在し，開発したシステムの産業界等での利用が期待できる．
メンバー (順不同)
| 田村直之 | 研究代表者 | 神戸大学・情報基盤センター・教授 |
| 井上克巳 | 研究分担者 | 国立情報学研究所・情報学プリンシプル研究系・教授 |
| 番原睦則 | 研究分担者 | 神戸大学・情報基盤センター・准教授 |
| 鍋島英知 | 研究分担者 | 山梨大学・医学工学総合研究部・准教授 |
| 宋剛秀 | 研究分担者 | 神戸大学・情報基盤センター・助教 |
| 沖本天太 | 連携研究者 | 神戸大学大学院・海事科学研究科 |
| 丹生智也 | 連携研究者 | 新領域融合研究センター・融合プロジェクト特任研究員 |
| Laurent Simon | 研究協力者 | LRI, University Paris 11, Associate Professor |
研究資金
- 科学研究費補助金 基盤研究(B)
- 研究課題名：命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現
- 研究期間：2012年度 〜 2014年度
- 課題番号：24300007
- 研究期間：2012年度 〜 2014年度
その他
内部資料 (管理者only)
 |
Tamura Lab.T. Soh |