CSPSAT プロジェクト

最新ニュース

2012年4月16日 [CSPSAT]

第4回CSPSAT&ASP講演会の情報を追加しました．

2012年3月2日 [CSPSAT]

第12回CSPSAT研究会の情報を追加しました．

2011年11月15日 [CSPSAT]

第3回CSPSAT&ASP講演会の情報を追加しました．

第11回CSPSAT研究会の情報を追加しました．

2011年6月22日 [COMPETITION]

2011 SAT Competition で鍋島先生の glueminisat (Application, UNSAT, CPU time) が金メダルを獲得しました． 他に銀メダル2個も獲得．

2011 Max-SAT Evaluation で越村先生の QMaxSat が Partial Max-SAT, Application で1位， Partial Max-SAT, Crafted で2位 になりました．

2011年4月1日 [CSPSAT]

プロジェクトが最終年(4年目)に突入!

バックナンバー

• 2010年度ニュース
• 2009年度ニュース
• 2008年度ニュース

プロジェクト概要

背景

CSPとは，与えられた制約条件を満たす解あるいは最適解を探索する問題です． CSPは，近年のSCMやERP等に代表される企業経営最適化を始めとした様々な産業分野に応用されているだけでなく， 求解が非常に困難(NP困難)な問題としてソフトウェアにおける重要な研究課題となっており， 欧米を中心として活発に研究が進められています． また，CSPを解くためのCSPソルバーも， フランスILOG社のソルバーを始めとして，欧米の大学等の研究機関で活発に研究開発が進められています． CSPの並列ソルバーについては， 分散CSPに関する理論的研究は進展していますが， 高速な求解を実現するための実装技術については， CSPに関する国際会議の発表等を見ても まだ研究が進んでいるとは言えません．

一方，近年になって 命題論理の充足可能性判定問題(SAT問題)を 解く高速なSATソルバー(MiniSAT等)が開発されています． これを契機として， スケジューリング問題，プランニング問題， ハードウェア検証， ソフトウェア検証等の問題をSAT問題に変換して解くSAT変換の研究が盛んになり， 大きな成功をおさめています． 例えば，プランニング問題について現在最速のソルバーの1つは SAT変換に基づくSATPLANです． 並列SATソルバーについては，CSPよりも問題が単純であることもあり， Rice大学のGridSATを始めとして徐々に研究が始まっており， 有望なアプローチと考えられています． しかし，CSPのSAT変換結果であるSAT問題の並列処理方法については， まだ未知な部分の多い研究課題といえます．

具体的な研究テーマ (予定)

(A) SAT変換の研究

(A1) CSPのSAT変換

(A2) 動的CSPのSAT変換

(A3) 命題時相論理のSAT変換

(A4) 分散CSPのSAT変換

(B) SATソルバーの研究

(B1) DPLLに基づくSATソルバー

(B2) モデル生成に基づくSATソルバー

(C) 共有メモリ型並列ソルバーの研究

(C1) 学習節再利用方式の共有メモリ型並列ソルバー

(C2) アルゴリズム並列方式の共有メモリ型並列ソルバー

(D) 分散型並列ソルバーの研究

(D1) 学習節再利用方式の分散型並列ソルバー

(D2) 問題分割方式の分散型並列ソルバー

学術的な特色

2001年のChaff，2003年のMiniSat等，SATソルバーの速度向上には目を見張るものがあり， SAT変換を用いた問題解決手法がプランニング問題，スケジューリング問題， ハードウェア検証，ソフトウェア検証等の分野で成功をおさめつつあります． その意味で， SAT問題は求解が困難な問題に対するアセンブリ言語として位置付けられようになってきました． したがって，本プロジェクトの目的は， 求解が困難な問題に対する並列求解方法について，有望なアプローチを提示することとも考えることができます．

SAT変換に基づくCSPソルバーを，従来からのCSPソルバーと比較した場合， 現状では，適用分野の拡大，大規模な問題への対応が問題となり， 本プロジェクトでは，それらを重要な研究課題ととらえています． しかし，両者の研究内容は相反するものではなく， 最近のCSPソルバーとSATソルバーの比較研究 (Dimopoulos他 ``Propagation In CSP and SAT'', Proc. CP2006)にも見られる ように， 将来的には両者の技術の融合が進むものと考えられます．

メンバー (順不同)

田村直之， 神戸大学・情報基盤センター・教授

井上克巳， 国立情報学研究所・情報学プリンシプル研究系・教授

岩沼宏治， 山梨大学・ 医学工学総合研究部・教授

長谷川隆三，九州大学・システム情報科学研究院・教授

横尾真， 九州大学・システム情報科学研究院・教授

上田和紀， 早稲田大学・理工学術院情報理工学科・教授

Narendra Jussien， Ecole des Mines de Nantes

藤田博，九州大学・システム情報科学研究院・准教授

鍋島英知，山梨大学・医学工学総合研究部・准教授

平山勝敏， 神戸大学・海事科学研究科・准教授

越村三幸，九州大学・システム情報科学研究院・助教

山本 泰生， 山梨大学・医学工学総合研究部・助教

番原睦則， 神戸大学・情報基盤センター・准教授

講演会スケジュール

2012年度

第4回CSPSAT&ASP講演会 [詳細]

日時：2012年5月21日(月) 〜 22日(火)

講演者： Michael Codish (Ben-Gurion University of the Negev) and Chitta Baral (Arizona State University)

用務先：神戸大学 自然科学総合研究棟3号館(東)4F 渕野グループ プレゼンテーション室(421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

2011年度

第3回CSPSAT&ASP講演会 [終了] [詳細]

日時：2011年11月21日(月) 〜 22日(火)

講演者：Torsten Schaub 氏ほか

用務先：神戸大学 自然科学総合研究棟3号館(東)4F 渕野グループ プレゼンテーション室(421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

2010年度

第2回CSPSAT講演会 [終了] [詳細]

日時：2010年11月8日(月) 〜 9日(火)

講演者：Pavel Surynek 氏

用務先：神戸大学 自然科学総合研究棟3号館(東)4F 渕野グループ プレゼンテーション室(421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

2009年度

第1回CSPSAT講演会 [終了] [詳細]

日時：2010年2月4日(木) 15:00 〜

講演者：Reiner Hähnle教授，Niklas Sörensson氏

用務先：神戸大学 自然科学総合研究棟3号館(東)4F 新井プロジェクト プレゼンテーション室(421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

研究会スケジュール

2011年度

第10回CSPSAT研究会[終了] [詳細]

日時：2011年8月17日(水) 〜 19日(金)

用務先： 九州大学西新プラザ・中会議室

用務地：〒814-0002 福岡市早良区西新2-16-23

第11回CSPSAT研究会[終了] [詳細]

日時：2011年11月30日(水) 〜 12月02日(金)

用務先：下呂市民会館 第2，第3研修室

用務地：〒509-2202 岐阜県下呂市森801-10

第12回CSPSAT研究会[終了] [詳細]

日時：2012年3月19日(月) 〜 21日(水)

用務先：由布市 湯布院公民館 視聴覚室

用務地：〒879-5102 大分県由布市湯布院町川上3758-1

2010年度

第7回CSPSAT研究会 [終了] [詳細]

日時：2010年7月26日(月) 〜 28日(水)

用務先：横谷温泉旅館

用務地：〒391-0301 長野県茅野市北山5513

第8回CSPSAT研究会 [終了] [詳細]

日時：2010年12月21日(火) 〜 23日(木)

用務先： 九州大学西新プラザ・中会議室

用務地：〒814-0002 福岡市早良区西新2-16-23

第9回CSPSAT研究会 [終了] [詳細]

日時：2011年3月17日(木) 〜 3月19日(土)

用務先：神戸大学 自然科学総合研究棟3号館(東) 4F， 渕野グループ，プレゼンテーション室 (421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

2009年度

第4回CSPSAT研究会 [終了] [詳細]

日時：2009年7月28日(火) 〜 30日(木)

用務先：ホテルニューアワジ プラザ淡路島 会議室 (アクセス方法)

用務地：〒656-0542 兵庫県南あわじ市阿万吹上

第5回CSPSAT研究会 [終了] [詳細]

日時：2009年11月30日(月) 〜 12月02日(水)

用務先：レイクランドホテル みづのさと

用務地：〒401-0302 山梨県南都留郡富士河口湖町小立1070

第6回CSPSAT研究会 [終了] [詳細]

日時：2010年3月28日(日) 〜 3月30日(火)

用務先：鹿児島県市町村自治会館

用務地：〒890-0064 鹿児島市鴨池新町7番4号(県庁前)

2008年度

第1回CSPSAT研究会 [終了] [詳細]

日時：2008年8月21日(木) 〜 22日(金)

用務先：神戸大学 自然科学総合研究棟3号館(東)4F 新井プロジェクト プレゼンテーション室(421号室) (アクセス方法)

用務地：〒657-8501 兵庫県神戸市灘区六甲台町1-1

最寄り駅：(JR東海道・山陽本線)六甲道 or (阪急神戸本線)六甲

第2回CSPSAT研究会 [終了] [詳細]

日時：2008年12月1日(月) 〜 2日(火)

用務先：国立情報学研究所(NII) 会議室(1210, 203) (アクセス方法)

用務地：〒101-8430 東京都千代田区一ツ橋2-1-2

最寄り駅： 東京メトロ半蔵門線・都営地下鉄三田線・新宿線「神保町」A8出口， or 東京メトロ東西線「竹橋」1b出口

第3回CSPSAT研究会 [終了] [詳細]

日時：2009年3月12日(木) 〜 14日(土)

用務先： 九州大学西新プラザ・中会議室

用務地：〒814-0002 福岡市早良区西新2-16-23

研究資金

科学研究費補助金 基盤研究(A)

研究課題名：制約最適化問題のSAT変換による解法とその並列分散処理に関する研究

研究期間：2008年度 〜 2011年度

課題番号：20240003

研究代表者：田村直之

研究分担者：井上克巳，岩沼宏治，鍋島英知，横尾真，長谷川隆三， 越村三幸，平山勝敏，番原睦則

研究分担者 (2010年度から)：上田和紀，藤田博，山本泰生

ソフトウェア

• Sugar: SAT変換による制約ソルバー

研究業績

• 研究業績リスト

参考文献一覧 (2009年11月5日版)

• HTMLファイル
• BibTeXファイル (文字コードEUC)

その他

• 内部資料 (管理者only)