巨大な制約充足問題を解くための SAT 型 CSP ソルバーの研究開発
概要
SAT 型 CSP ソルバーは，その性能向上に伴って，システム検証，システム生物学，クラウド計算，セキュリティ，組み合わせ数学など様々な応用分野で利用が進んでおり，その適用分野の拡大とともに，より巨大な問題を扱いたいという要求も増えている．本研究では，順序符号化に基づく SAT 型 CSP ソルバーにおいて巨大な問題を扱うことを可能にするため，以下の研究開発に取り組む．
- SAT ソルバーにおいて節集合を圧縮したまま推論する技術の研究開発
- CSP ソルバーが生成する SAT 問題の大きさを抑制する符号化方法に関する研究
情報
- プロジェクト名：巨大な制約充足問題を解くための SAT 型 CSP ソルバーの研究開発
- 研究資金：2020年度 国立情報学研究所 公募型共同研究・自由提案公募型
- 研究期間：2020年4月から2021年3月
メンバー（敬称略・順不同）
氏名 担当 所属 鍋島 英知 研究代表者 山梨大学・総合研究部・准教授 井上 克巳 共同研究者 国立情報学研究所・情報学プリンシプル研究系・教授 田村 直之 共同研究者 神戸大学・情報基盤センター・教授 番原 睦則 共同研究者 名古屋大学・情報学研究科・教授 宋 剛秀 共同研究者 神戸大学・情報基盤センター・准教授 早瀬 悠真 共同研究者 山梨大学・大学院医工農学総合教育部・修士課程学生 三嶋 哲平 共同研究者 神戸大学・大学院システム情報学研究科・博士課程前期課程学生 戸塚 悠太郎 共同研究者 東京工業大学・情報理工学院・修士課程学生
第１回研究会合
会議情報
- 日時：2020年9月3日(木) 13:00-16:30
- 場所：Zoom ミーティング
プログラム
プログラムは下記の通りですが，発表の進行状況に合わせて「柔軟」に進めたいと思います．
| 2020年9月3日(木) | |
|---|---|
| 13:00 - 13:15 | 研究目的・内容の確認 |
| 13:15 - 14:00 | 研究発表 SAT問題を圧縮したまま解くソルバー (スライド) |
| 早瀬 悠真，○鍋島 英知 | |
| 14:00 - 14:30 | 研究発表 解集合プログラミングを用いた配電網問題の解法に関する一考察 |
| ○山田 健太郎，湊 真一, 番原 睦則 | |
| 14:30 - 15:00 | 研究発表 車両装備仕様問題に対する解集合プログラミングの適用 |
| ○竹内 頼人，田村 直之, 番原 睦則 | |
| 15:00 - 15:30 | 研究発表 解集合プログラミングによる決定木アンサンブルからのルール抽出 |
| ○竹村 彰浩，井上 克巳 | |
| 15:30 - 16:30 | プロジェクト研究打合せ |
| - 今後の研究計画について | |
| - 予算執行について | |
| - 次回日程調整 |
参加者
- 国立情報学研究所
- 井上 克巳
- 神戸大学
- 田村 直之，宋 剛秀, 三嶋 哲平, 喜安 貴也, 山本 敦史, 足立 啓一, 堀岡 真未
- 名古屋大学
- 番原 睦則，山田 健太郎，竹内 頼人, 桑原 和也
- 総合研究大学院大学
- 竹村 彰浩
- 山梨大学
- 鍋島 英知
第２回研究会合
会議情報
- 日時：2020年11月30日(月) 10:00-12:00
- 場所：Zoom ミーティング
プログラム
プログラムは下記の通りですが，発表の進行状況に合わせて「柔軟」に進めたいと思います．
| 2020年11月30日(月) | |
|---|---|
| 10:00 - 10:05 | プログラムの確認 |
| 10:05 - 10:40 | 研究発表 SATソルバーの組合せデザイン問題への適用研究事例 |
| ○盧 暁南 | |
| 10:40 - 11:10 | 研究発表 圧縮 SAT 問題に対する高速な単位伝播手法の実装に向けて |
| ○早瀬 悠真，鍋島 英知 | |
| 11:10 - 11:40 | 研究発表 SATソルバーを用いた一層平面配置配線問題の解法に関する研究 |
| ○三嶋 哲平，宋 剛秀，田村 直之 | |
| 11:40 - 12:00 | 今後の研究計画 |
| その他 | |
| - 2021年度 NII 共同研究申請について | |
| - 次回日程調整 |
参加者
- 国立情報学研究所
- 井上 克巳，佐藤 泰介
- 神戸大学
- 田村 直之，宋 剛秀, 三嶋 哲平，喜安 貴也, 山本 敦史, 足立 啓一, 堀岡 真未
- 名古屋大学
- 番原 睦則
- 総合研究大学院大学
- 竹村 彰浩
- 東京工業大学
- 戸塚 悠太郎
- 山梨大学
- 鍋島 英知，盧 暁南，早瀬 悠真
第３回研究会合
会議情報
- 日時：2021年3月18日(木) 9:30-15:30
- 場所：Zoom ミーティング
プログラム
プログラムは下記の通りですが，発表の進行状況に合わせて「柔軟」に進めたいと思います．
| 2021年3月18日(木) | |
|---|---|
| 9:30 - 10:15 | 研究発表 圧縮したSAT 問題における高速・省メモリな単位伝播手法 |
| ○早瀬 悠真，鍋島 英知，盧 暁南（山梨大） | |
| 10:15 - 11:00 | 研究発表 解集合プログラミングに基づく系統的探索と確率的局所探索の統合的手法に関する一考察 |
| ○桑原和也（名大）, 田村直之（神戸大）, 番原睦則（名大） | |
| 11:00 - 11:30 | 研究発表 逆向きライフゲームのSAT型解法に関する研究 |
| ○足立啓一，宋剛秀，田村直之（神戸大） | |
| 11:30 - 12:00 | 研究発表 B進法に基づく新規変数の導入を用いたCSP-to-CSP変換に関する研究 |
| ○堀岡真未，宋剛秀，田村直之（神戸大） | |
| 12:00 - 13:00 | 昼食休憩 |
| 13:00 - 13:45 | 研究発表 MatSat: a matrix-based differentiable SAT solver |
| ○佐藤泰介（NII）、小島 諒介（京大） | |
| 13:45 - 14:30 | 研究発表 SATソルバーを用いた一層平面配置配線問題の解法に関する研究 |
| ○三嶋哲平，宋剛秀，田村直之（神戸大） | |
| 14:30 - 14:55 | 研究発表 クイーン支配問題の制約モデルの提案 |
| 山本敦史，宋剛秀，○田村直之（神戸大） | |
| 14:55 - 15:20 | 研究発表 Alldifferent制約のSAT符号化とその応用 |
| 喜安貴也，宋剛秀，○田村直之（神戸大） | |
| 15:30 - 15:30 | 今後の方針に関する議論 |
参加者
- 国立情報学研究所
- 井上 克巳，佐藤 泰介
- 神戸大学
- 田村 直之，宋 剛秀, 三嶋 哲平, 足立 啓一, 堀岡 真未
- 名古屋大学
- 番原 睦則，平手 貴大，山田 悠也，竹内 頼人，山田 健太郎，桑原 和也
- 総合研究大学院大学
- 竹村 彰浩
- 東京工業大学
- 戸塚 悠太郎
- 山梨大学
- 鍋島 英知，盧 暁南，早瀬 悠真，久保 悠，田中 綜司，池田 佳貴， 小山 貴史，田光 宏章，吹上 翼