解集合プログラミングの実用化に向けた並列解法に関する研究開発
Table of Contents
研究概要
解集合プログラミング (Answer Set Programming; ASP) は，論理プログラミングと制約プログラミングを融合したパラダイムであり，その記述言語は論理プログラミング由来の優れた知識表現・モデリング能力を持つとともに，SAT 技術に基づく高速な処理系が開発されている．これにより，人工知能分野における様々な問題への応用が急速に拡大している．
本研究では，ASP のための実用的な並列解法の実現に向けて，以下の研究課題に取り組む．
- 再現性のある並列 ASP ソルバーの実現
- ASPにおける並列解法のスループットの改善
- ASP における極小充足不能アトム集合の並列解法
研究資金と期間
- 資金：2024年度 国立情報学研究所 公募型共同研究・自由提案公募型
- 期間：2024年4月から2025年3月
共同研究者
| 氏名 | 担当 | 所属 |
|---|---|---|
| 鍋島 英知 | 研究代表者 | 山梨大学・総合研究部・准教授 |
| 井上 克巳 | 研究分担者 | 国立情報学研究所・情報学プリンシプル研究系・教授 |
| 田村 直之 | 研究分担者 | 神戸大学・名誉教授 |
| 番原 睦則 | 研究分担者 | 名古屋大学・情報学研究科・教授 |
| 宋 剛秀 | 研究分担者 | 神戸大学・DX・情報統括本部・准教授 |
| 盧 暁南 | 研究分担者 | 岐阜大学・工学部・准教授 |
| 森山 総太 | 研究分担者 | 東京工業大学・情報理工学院・知能情報コース・大学院生 |
| 菅原 孝太 | 研究分担者 | 山梨大学・大学院医工農学総合教育部・大学院生 |
| 桂 献一郎 | 研究分担者 | 山梨大学・大学院医工農学総合教育部・大学院生 |
| 伊藤 碧己 | 研究分担者 | 名古屋大学・大学院情報学研究科・情報システム学専攻・大学院生 |
| 杉森 唯瑠未 | 研究分担者 | 名古屋大学・大学院情報学研究科・情報システム学専攻・大学院生 |
| 桑原 祥文 | 研究分担者 | 神戸大学・大学院システム情報学研究科・大学院生 |
第１回研究会合
開催情報
- 日程: 2024年6月26日（水）9時開始，6月27日（木）12時終了 (予定)
- 用務地：〒390-0811 長野県松本市中央１丁目２３−１
- 用務先：松本商工会議所 303会議室
プログラム
発表の進行状況に合わせて「柔軟」に進めたいと思います．
2024年6月26日(水) 09:00 - 11:00 ASP の定式化・解法に関するディスカッション 11:00 - 12:00 菅原 孝太 ASPを用いたナーススケジューリング問題におけるMUS列挙の検討 13:00 - 13:30 Nguyen Quoc, Tuan (NII) Rule learning in the form of program matrices 13:30 - 14:00 Federico Leuze (Aalto University) The Importance of Symbolic Generated Dataset for Machine Learning 14:00 - 14:15 Break 14:15 - 15:00 Meghyn Bienvenu (University of Bordeaux/LaBRI) Update on ASP implementation of logic-based entity resolution 15:00 - 15:45 Nelson Higuera (TU Wien) Large Neighborhood Search for Answer Set Programming Optimization 15:45 - 16:00 Break 16:00 - 16:30 Irumi Sugimori (Nagoya University) Large Neighborhood Prioritized Search for Combinatorial Optimization with Answer Set Programming 16:30 - 17:00 Sota Moriyama (Tokyo Institute of Technology/NII) MaxSAT Solving with the Satisfiability based Graph Attention Network 17:00 - 17:30 大橋 瞭雅 (神戸大学) SAT型CEGARを用いたハミルトン閉路問題の解法の改良の試み 17:30 - 18:00 桑原 祥文 (神戸大学) 組合せ遷移問題における遷移長圧縮の試み
- 懇親会 (18:30 - )
- 場所：ばんざい家（松本市中央1丁目3-18）
- 食事：5500円飲放題付きコース
- 予算：教員7000円，学生4000円 の予定
| 2024年6月27日(木) | |
|---|---|
| 09:30 - 10:00 | 竹村 彰浩 (NII) |
| ASPを用いた決定木モデルからの説明生成 | |
| 10:00 - 10:30 | 樋口 黎 (神戸大学) |
| SATソルバーを用いたSBML-qualモデルにおけるアトラクタの計算 | |
| 10:30 - 11:00 | 桂 献一郎 (山梨大学) |
| 再現性のある並列ASP ソルバーの実現に向けた静的同期法の実装 | |
| 11:00 - 15:00 | 今後の方針に関する打合わせ |
参加予定者 (敬称略,順不同)
- 井上 克巳（NII）
- 田村 直之 (神戸大学)
- 番原 睦則 (名古屋大学)
- 宋 剛秀 (神戸大学)
- 盧 暁南（岐阜大学）
- 鍋島 英知 (山梨大)
- Meghyn Bienvenu (University of Bordeaux/LaBRI)
- Nguyen Quoc, Tuan (NII)
- Nelson Higuera (TU Wien, D3)
- Federico Leuze (Aalto University, M2)
- 竹村 彰浩 (NII)
- 森山 総太 (東京工業大学, M2)
- 杉森 唯瑠未 (名古屋大学, M1)
- 大橋 瞭雅 (神戸大学, M2)
- 桑原 祥文 (神戸大学, M2)
- 樋口 黎 (神戸大学, M2)
- 菅原 孝太 (山梨大学, M2)
- 桂 献一郎 (山梨大学, M1)
The 2nd NII Collaborative Research Meeting
General information
- Date: October 28-29, 2024
- Venue: Room 588, 5th floor, IB Building South, Higashiyama Campus, Nagoya University (Furo-cho, Chikusa-ward, Nagoya-city, 464-8601)
- Access: https://en.nagoya-u.ac.jp/access/
Main program (tentative)
| October 28 Monday | Day 1 |
|---|---|
| 12:50 - 13:00 | Opening |
| 13:00 - 14:00 | Keynote talk |
| ASP in Industry, here and there: Torsten Schaub | |
| 14:10 - 15:40 | Session 1 |
| ASP based Nurse Scheduling System at the University of Yamanashi Hospital: Hidetomo Nabeshima | |
| Towards a Reproducible Parallel ASP Solver Based on Static Synchronization: Kenichiro Katsura | |
| Symbolic Parameter Learning in Probabilistic Answer Set Programming: Elisabetta Gentili | |
| 15:40 - 16:00 | Break |
| 16:00 - 17:30 | Session 2 |
| Pareto-optimal Combinatorial Reconfiguration considering Cost and Length based on Answer Set Programming: Kazuki Takada | |
| A SAT-based Method for Counting All Singleton Attractors in Boolean Networks: Rei Higuchi | |
| 17:30 - 18:00 | Project meeting (member only) |
| 19:00 - | Dinner |
| October 29 Tuesday | Day 2 |
|---|---|
| 09:30 - 11:30 | Session 3 |
| Large Neighborhood Prioritized Search for Combinatorial Optimization with Answer Set Programming: Irumi Sugimori | |
| Logical Framework for Collective Entity Resolution: Meghyn Bienvenu | |
| ASPEN: ASP-Based System for Collective Entity Resolution: Zhiliang Xiang | |
| Dominating Set Reconfiguration with Answer Set Programming: Takehide Soh | |
| 11:30 - 11:40 | Closing |
| 13:00 - 17:00 | Personal discussion |
Personal discussion with Torsten Schaub
- October 29 Tuesday 13:00 - 17:00
- Meghyn Bienvenu and Zhiliang Xiang, Collective Entity Resolution (tentative)
- Hidetomo Nabeshima and Takehide Soh, Nurse scheduling problem (tentative)
- Hidetomo Nabeshima and Takehide Soh, Deterministic parallel ASP solving (tentative)
Personal discussion
- October 29 Tuesday 13:00 - 17:00
- Masahiko Sakai and Hidetomo Nabeshima, PB solver (tentative)
- October 30 Wednesday 10:00 - 12:00
- Takehide Soh and Mutsunori Banbara
Participants (*: attendance at dinner)
- Torsten Schaub* (University of Potsdam), 1 accompany person*
- Katsumi Inoue (NII)
- Meghyn Bienvenu* (LaBRI CNRS)
- Zhiliang Xiang* (Leon) (Cardiff University)
- Elisabetta Gentili (University of Ferrara)
- Hidetomo Nabeshima* (University of Yamanashi)
- Kenichiro Katsura* (University of Yamanashi, M1)
- Xiao-Nan Lu* (Gifu University)
- Takehide Soh* (Kobe Universiy)
- Rei Higuchi* (Kobe Universiy, M2)
- Masahiko Sakai* (Nagoya university)
- Mutsunori Banbara* (Nagoya university)
- Aoi Ito (Nagoya university, M2)
- Kazuki Takada* (Nagoya university, M2)
- Irumi Sugimori* (Nagoya university, M1)
- Makoto Nagayama (Nagoya university, B4)
- Ayumu Hirasawa (Nagoya university, B4)
- Tomohiro Mizowaki (Nagoya university, B4)
Dinner for faculty and guests
- Date: Start at 19:00 on October 28
- Venue: しら河 浄心本店 (Shirakawa Joshin)
- Access: Google Map (2 minutes walk from Joshin station of Subway Tsurumai line)
- Participants: 9 people
- Fee: 8,000 yen/person
Dinner for Japanese students
- Date: Start at 19:00 on October 28
- Venue: 金鯱酒場 錦店
- Participants: 4 people
第３回研究会合
開催情報
- 日程: 2024年12月23日（月）9時開始，12月24日（火）12時終了
- 用務地：〒760-0023 香川県高松市寿町2丁目4-20
- 用務先：高松センタービル 10階1005号室
プログラム
- 発表の進行状況に合わせて「柔軟」に進めたいと思います．
| 2024年12月23日(月) | |
|---|---|
| 09:00 - 12:00 | ASP の定式化・解法に関するディスカッション |
| 13:00 - 13:30 | Zhiliang Xiang (Cardiff University) |
| ASP-based Entity Resolution: Alternative Optimality and Local Semantics | |
| 13:30 - 14:00 | Elisabetta Gentili (University of Ferrara) |
| Logic Programming for Knowledge Graph Completion (provisional) | |
| 14:00 - 14:15 | Break |
| 14:15 - 14:45 | Nguyen Quoc Tuan (NII) |
| Stable model computation as an optimization problem and possible extensions | |
| 14:45 - 15:15 | 森山総太 (東京科学大学) |
| GNN based Heuristics for MaxSAT Solving (tentative) | |
| 15:15 - 15:30 | Break |
| 15:30 - 16:30 | 橋本健二 (香川大学) — キャンセル |
| TBA | |
| 今後の研究計画に関する打合わせ |
- 懇親会 (18:00 - )
- 場所：高松 骨付鳥 居酒屋 ぴかでり屋（香川県高松市福田町9-5）
- 食事：5880円飲放題付きコース
- 予算：教員8000円，学生4000円 の予定
| 2024年12月24日(火) | |
|---|---|
| 09:30 - 10:00 | 中野良春 (山梨大学) |
| 決定的並列 SAT ソルバーにおける UNSAT 証明の並列検証器の実装 | |
| 10:00 - 10:30 | 船木泰平 (神戸大学) |
| Rust 言語を用いた順序符号化の高速実装に向けて | |
| 10:30 - 11:00 | 浅尾健太 (神戸大学) |
| 様々なベンチマークを用いた At-most-one 制約のSAT符号化の再評価 | |
| 11:00 - 12:00 | 今後の会議開催に関する打合わせ |
参加者 (敬称略, 順不同, *印は懇親会の参加者):
- 井上克巳 (NII)*
- 番原睦則 (名古屋大学)*
- 盧暁南 (岐阜大学)*
- 鍋島英知 (山梨大学)*
- 橋本健二 (香川大学) — 欠席
- 中野良春 (山梨大学)*
- Zhiliang Xiang (Cardiff University)*
- Elisabetta Gentili (University of Ferrara)
- Nguyen Quoc Tuan (NII)
- 森山総太 (東京科学大学)*
- 船木泰平 (神戸大学)*
- 浅尾健太 (神戸大学)*
- 宋剛秀 (神戸大学)*