所属
大学院情報学研究科 情報システム学専攻 計算論 准教授
大学院担当
大学院情報学研究科
学部担当
情報学部 コンピュータ科学科
職名
准教授
外部リンク
ソウ タケヒデ
宋 剛秀
SOH Takehide
研究キーワード 15
-
推論技術
-
国際情報交換
-
命題論理
-
動的制約
-
制約最適化
-
制約充足
-
制約プログラミング
-
充足可能性判定問題
-
充足可能性判定
-
フランス
-
ハミルトン閉路問題
-
ドメイン特化言語
-
システム生物学
-
SAT技術
-
SAT
研究分野 4
-
情報通信 / 知能情報学
-
情報通信 / 生命、健康、医療情報学
-
情報通信 / 情報学基礎論
-
情報通信 / ソフトウェア
経歴 2
-
神戸大学 情報基盤センター 准教授
2019年4月 - 現在
-
神戸大学 助教
2012年4月
学歴 1
-
総合研究大学院大学
- 2011年9月
所属学協会 4
-
電子情報通信学会
-
日本ソフトウェア科学会
-
情報処理学会
-
人工知能学会
受賞 16
-
2022 XCSP3 Competition 逐次CSPソルバー部門準優勝
2022年8月 XCSP3 Competition Organization Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura
-
2019 XCSP3 Competition 逐次CSPソルバー部門準優勝
2019年10月 XCSP3 Competition Organization Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura
-
第７回解説論文賞 (2018年度)
2019年8月 日本ソフトウェア科学会 SAT型制約プログラミングシステムと周辺技術
宋 剛秀, 番原 睦則, 田村 直之
-
2019年度全国大会優秀賞
2019年 人工知能学会 A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
宋 剛秀, Le Berre Daniel, 番原 睦則, 田村 直之
-
情報処理学会 2018 年度特選論文
2018年9月 情報処理学会 SAT技術を用いたペトリネットのデッドロック検出手法の提案
寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
-
2018 XCSP3 Competition 2部門優勝 (逐次CSPソルバー部門, 並列CSPソルバー部門)
2018年8月 XCSP3 Competition Organization sCOP
Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
-
2016年度全国大会優秀賞
2017年3月 人工知能学会 SAT型制約ソルバーによるナンバーリンクの解法とその評価
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
-
PPL2017発表賞（一般の部）
2017年3月 日本ソフトウェア科学会 プログラミング論研究会 SATソルバーの最新動向と利用技術
宋 剛秀, 田村 直之
-
第20回研究論文賞
2016年3月 日本ソフトウェア科学会 パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
-
アルゴリズムデザインコンテスト2015 最優秀賞 (DAシンポジウム2015)
2015年8月 情報処理学会 SLDM研究会 iSugar+GlueMiniSat
迫 龍哉, 川原 征大, 田村 直之, 番原 睦則, 宋 剛秀, 鍋島 英知
-
最優秀賞
2015年8月 情報処理学会DAシンポジウム2015 SAT型制約ソルバーを用いたナンバーリンクの求解と解の最適化
迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
-
第31回大会高橋奨励賞
2014年9月 日本ソフトウェア科学会 Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
宋 剛秀
-
アルゴリズムデザインコンテスト2014 最優秀賞 (DAシンポジウム2014・SWEST16)
2014年8月 情報処理学会 SLDM研究会 Sugar+GlueMiniSat
田村 直之, 宋 剛秀, 番原 睦則, 鍋島 英知
-
アルゴリズムデザインコンテスト2014 最優秀賞
2014年8月 情報処理学会DAシンポジウム2014 SAT型制約ソルバーを用いたナンバーリンクの解法
田村直之, 宋剛秀, 番原睦則, 鍋島英知
-
学長賞
2010年4月 総合研究大学院大学 SATとASPを用いた生物学におけるパスウェイの解析
宋 剛秀
-
２００９年度全国大会優秀賞
2009年9月 人工知能学会 モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
宋 剛秀
論文 83
-
ASP-Based Large Neighborhood Prioritized Search for Course Timetabling
Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
2025年
-
Takehide Soh, Tomoya Tanjo, Yoshio Okamoto, Takehiro Ito
Proceedings of the International Symposium on Combinatorial Search 17 巻 頁： 285 - 286 2024年6月
-
A Study on Production Scheduling Methods for Ready-Made Meal Industries.
Hinari Hamada, Nobutada Fujii, Shunsuke Watanabe, Takehide Soh, Ruriko Watanabe, Kohei Nakayama, Yuji Mishima, Kazuo Yoshinaga
APMS (2) 頁： 266 - 277 2024年
-
Scalable Hard Instances for Independent Set Reconfiguration. Open Access
Takehide Soh, Takumu Watanabe, Jun Kawahara, Akira Suzuki, Takehiro Ito
22nd International Symposium on Experimental Algorithms(SEA) 頁： 26 - 15 2024年
-
Hamiltonian Cycle Reconfiguration with Answer Set Programming 査読有り 国際共著 国際誌
Takahiro Hirate, Mutsunori Banbara, Katsumi Inoue, Xiao-Nan Lu, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura
In: S. Gaggl et al. (eds.), Logics in Artificial Intelligence, Proceedings of the 18th European Conference (JELIA 2023), Lecture Notes in Artificial Intelligence 14281 巻 頁： to appear - 16p. 2023年9月
-
SAT-Based Method for Finding Attractors in Asynchronous Multi-Valued Networks 査読有り
Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the 16th International Joint Conference on Biomedical Engineering Systems and Technologies 頁： 163 - 174 2023年3月
-
SAF: SAT-Based Attractor Finder in Asynchronous Automata Networks 査読有り
Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
2023年
-
ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems. 査読有り
Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
CPAIOR 頁： 167 - 183 2023年
-
Takahisa Toda, Takehiro Ito, Jun Kawahara, Takehide Soh, Akira Suzuki, Junichi Teruyama
35th IEEE International Conference on Tools with Artificial Intelligence(ICTAI) 頁： 294 - 302 2023年
-
ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems. 査読有り
Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
CoRR abs/2207.13959 巻 2022年12月
-
Core Challenge 2022: Solver and Graph Descriptions.
Takehide Soh, Yoshio Okamoto, Takehiro Ito
CoRR abs/2208.02495 巻 2022年9月
-
チャネリング制約を用いた alldifferent 制約の SAT 符号化 Open Access
小菅脩司, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022年3月
-
解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価 Open Access
桑原和也, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022年3月
-
有界モデル検査による独立集合遷移問題の解法に関する考察 Open Access
戸田 貴久, 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一
情報処理学会 研究報告アルゴリズム（AL） 2022-AL-186 巻 ( 5 ) 頁： 1 - 7 2022年1月
-
Towards CEGAR-based Parallel SAT Solving 査読有り
Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue
Pragmatics of SAT 2021 2021年7月
-
CEGARと反例の共有を用いたSAT型CSPソルバーの並列化方法の考察 (特集 「命題論理の充足可能性問題SATの最新動向」および一般) Open Access
宋 剛秀, 鍋島 英知, 番原 睦則, 田村 直之, 井上 克巳
人工知能基本問題研究会 112 巻 頁： 6 - 11 2020年3月
-
解集合プログラミングによる様相命題論理Kの充足可能性判定 Open Access
飯野 有軌, 田村 直之, 宋 剛秀, 番原 睦則, 井上 克巳
人工知能学会全国大会論文集 2020 巻 ( 0 ) 頁： 2N5OS17b05 - 2N5OS17b05 2020年
-
alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用 Open Access
大野周亮, 番原睦則, 宋剛秀, 田村 直之
人工知能学会研究会資料 SIG-FPAI-B803 巻 頁： 6 - 11 2019年3月
-
A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition Open Access
宋 剛秀, Le Berre Daniel, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2019 巻 ( 0 ) 頁： 1E2OS3a03 - 1E2OS3a03 2019年
-
Solver Description of Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura
Solver Descriptions of XCSP3 Competition 2019 (XCSP19) 頁： 1 - 2 2019年
-
teaspoon : solving the curriculum-based course timetabling problems with answer set programming. 査読有り
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
Annals OR 275 巻 ( 1 ) 頁： 3 - 37 2019年
-
SAT技術を用いたペトリネットのデッドロック検出手法の提案 Open Access
寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
情報処理学会論文誌 59 巻 ( 9 ) 頁： 1749 - 1760 2018年9月
-
ブール基数制約を経由した擬似ブール制約のSAT符号化手法 査読有り Open Access
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
コンピュータソフトウェア = Computer software 35 巻 ( 3 ) 頁： 65 - 78 2018年8月
-
SATソルバーの最新動向と利用技術 査読有り Open Access
宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
コンピュータ ソフトウェア 35 巻 ( 4 ) 頁： 72 - 92 2018年
-
sCOP: SAT-based Constraint Programming System
Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
Solver Descriptions of XCSP3 Competition 2018 (XCSP18) 頁： 1 - 2 2018年
-
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会大会論文集 34 巻 頁： 393 - 404 2017年9月
-
Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings 査読有り
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS 26 巻 ( 1 ) 2017年2月
-
Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー Open Access
宋 剛秀, 番原 睦則, 田村 直之
第58回プログラミング・シンポジウム予稿集 頁： 71 - 74 2017年1月
-
ブール基数制約を経由した擬似ブール制約のSAT符号化法 Open Access
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会研究会資料 頁： 18 - 23 2017年1月
-
SATソルバーの使い方 —問題をSATに符号化する方法— Open Access
田村 直之, 宋 剛秀, 番原 睦則
第58回プログラミング・シンポジウム予稿集 頁： 165 - 172 2017年1月
-
catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming. 査読有り
Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
The 14th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR-17) 頁： 265 - 278 2017年
-
ブール基数制約を経由した擬似ブール制約のSAT符号化法 Open Access
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会研究会資料 人工知能基本問題研究会 103 巻 頁： 4 - 4 2017年
-
Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation. 査読有り
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Daniel Le Berre
Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017) 10416 巻 頁： 596 - 614 2017年
-
SAT技術を用いたペトリネットのデッドロック検出手法の提案 Open Access
寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2017 巻 ( 0 ) 頁： 1M1OS02a2 - 1M1OS02a2 2017年
-
SAT型制約プログラミングシステムと周辺技術 査読有り Open Access
宋 剛秀, 番原 睦則, 田村 直之
コンピュータ ソフトウェア 34 巻 ( 1 ) 頁： 1_67 - 1_80 2017年
-
制約充足問題のASP符号化に関する一考察 Open Access
坡山 直樹, 番原 睦則, 宋 剛秀, 田村 直之
人工知能学会全国大会論文集 2017 巻 ( 0 ) 頁： 1M1OS02a4 - 1M1OS02a4 2017年
-
解集合プログラミングによるカリキュラムベース・コース時間割編成 招待有り
番原 睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋 剛秀, 田村 直之, フィリップ ワンコ
第29回RAMPシンポジウム論文集 頁： 73 - 88 2017年
-
An incremental SAT solving library and its applications 査読有り Open Access
Tatsuya Sako, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima, Katsumi Inoue
Computer Software 33 巻 ( 4 ) 頁： 16 - 29 2016年11月
-
Implementing efficient all solutions SAT solvers 査読有り
Takahisa Toda, Takehide Soh
ACM Journal of Experimental Algorithmics 21 巻 ( 1 ) 頁： 1 - 44 2016年10月
-
インクリメンタルSAT解法ライブラリとその応用 査読有り Open Access
迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知, 井上 克巳
コンピュータソフトウェア 33 巻 ( 4 ) 頁： 16 - 29 2016年7月
-
クラウド上のソフトウェア要素最適配置問題の解法 (特集 「命題論理の充足可能性問題SATと応用技術」および一般) Open Access
田村 直之, 井上 克巳, 鍋島 英知, 番原 睦則, 宋 剛秀
人工知能基本問題研究会 100 巻 頁： 19 - 24 2016年3月
-
分子ネットワーク上の状態推定とその可視化による知識発見支援 Open Access
平沼 祐人, 山本 泰生, 守屋 央朗, 宋 剛秀, 岩沼 宏治
第45回バイオ情報学研究発表会 11 巻 頁： 1 - 6 2016年3月
-
解集合プログラミングを用いた制約組合せテストケース生成 査読有り
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, 沖本 天太
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) カテゴリC1 巻 2016年3月
-
SATソルバーを用いた制約プログラミングシステムとその応用 Open Access
宋 剛秀
第57回プログラミング・シンポジウム 頁： 1 - 10 2016年1月
-
SATソルバーを用いた部分グラフ探索のための制約モデル Open Access
川原 征大, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2016 巻 ( 0 ) 頁： 1D4OS02a4 - 1D4OS02a4 2016年
-
Teaspoon: Solving the curriculum-based course timetabling problems with answer set programming 査読有り
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
PATAT 2016 - Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling 頁： 13 - 32 2016年
-
SAT型制約ソルバーによるナンバーリンクの解法とその評価 Open Access
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
人工知能学会全国大会論文集 2016 巻 ( 0 ) 頁： 1D4OS02a3 - 1D4OS02a3 2016年
-
iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー Open Access
迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知, 井上 克巳
日本ソフトウェア科学会第32回大会 頁： 1 - 12 2015年9月
-
Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について Open Access
宋 剛秀, 馬場 知哉
日本ソフトウェア科学会第32回大会 頁： 1 - 8 2015年9月
-
SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価 Open Access
川原 征大, 宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会第32回大会 32 巻 頁： 1 - 9 2015年9月
-
順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化 Open Access
宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会第32回大会 頁： 1 - 11 2015年9月
-
制約充足問題のハイブリッド符号化に向けて Open Access
宋 剛秀, 佐古田 淳史, 番原 睦則, 田村 直之
第第97回人工知能基本問題研究会．人工知能学会研究会資料 頁： 65 - 73 2015年3月
-
A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings 査読有り
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015) 2016-January 巻 頁： 421 - 428 2015年
-
aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming. 査読有り
Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
CoRR abs/1312.6113 巻 頁： 112 - 126 2015年
-
Implementing Efficient All Solutions SAT Solvers. 査読有り
Takahisa Toda, Takehide Soh
CoRR abs/1510.00523 巻 2015年
-
組合せテストケース生成問題に対する制約解集合プログラミングの適用 Open Access
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
人工知能学会全国大会論文集 2015 巻 ( 0 ) 頁： 2H5OS03b5 - 2H5OS03b5 2015年
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール Open Access
宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会第31回大会講演論文集 頁： 1 - 15 2014年9月
-
制約解集合プログラミングシステムの設計方式に関する考察 Open Access
宋 剛秀, 則武 治樹, 番原 睦則, 田村 直之, 井上 克巳
日本ソフトウェア科学会第31回大会講演論文集 頁： 1 - 15 2014年9月
-
SAT型制約ソルバーを用いたナンバーリンクの解法 Open Access
田村 直之, 宋 剛秀, 番原 睦則, 鍋島 英知
DAシンポジウム2014論文集 2014 巻 ( 2014 ) 頁： 215 - 220 2014年8月
-
Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the 5th International Workshop on Pragmatics of SAT (PoS 2014) 頁： 1 - 12 2014年7月
-
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法 Open Access
佐古田 淳史, 宋 剛秀, 番原 睦則, 田村 直之
第28回人工知能学会全国大会論文集 頁： 1 - 4 2014年5月
-
Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem 査読有り
Takehide Soh, Daniel Le Berre, Stephanie Roussel, Mutsunori Banbara, Naoyuki Tamura
LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2014 8761 巻 頁： 684 - 693 2014年
-
SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用 Open Access
宋 剛秀, Berre Daniel Le, Roussel Stéphanie, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2014 巻 ( 0 ) 頁： 1D5OS11b6i - 1D5OS11b6i 2014年
-
Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura
Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings 頁： 684 - 693 2014年
-
PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding 査読有り
Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013) 2013年11月
-
Answer set programming as a modeling language for course timetabling 査読有り
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
THEORY AND PRACTICE OF LOGIC PROGRAMMING 13 巻 ( 4/5 ) 頁： 783 - 798 2013年7月
-
SAT符号化を用いたパッキング配列の構成 査読有り
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集 2013年3月
-
Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems. 査読有り
Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings 7962 巻 頁： 429 - 436 2013年
-
System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems⋆
Soh, Takehide, Tamura, Naoyuki, Banbara, Mutsunori, Le Berre, Daniel, Roussel, St{\'e}phanie
2013年
-
Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration
SOH Takehide, INOUE Katsumi, BABA Tomoya, TAKADA Toyoyuki, SHIROISHI Toshihiko
International Journal On Advances in Life Sciences 4(3-4):154-165 巻 2012年12月
-
カリキュラムベースのコース時間割問題の擬似ブール最適化問題への符号化
鈴江 美奈, 田村 直之, 番原 睦則
日本ソフトウェア科学会大会論文集 29 巻 頁： 495 - 502 2012年8月
-
Predicting Gene Knockout Effects by Minimal Pathway Enumeration
Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada, Toshihiko Shiroishi
The 4th International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies 頁： 11 - 19 2012年3月
-
Analyzing pathways using ASP-based approaches 査読有り
Oliver Ray, Takehide Soh, Katsumi Inoue
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6479 巻 頁： 167 - 183 2012年
-
モデル生成を用いた代謝ネットワークにおける極小活性パスウェイの列挙 査読有り
宋剛秀
人工知能学会論文誌 27 巻 ( 3 ) 頁： 204 - 212 2012年
-
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem 査読有り
Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
Fundamenta Informaticae 102(3-4): 467-487 巻 2010年11月
-
A SAT-based Method for Analyzing Metabolic Pathways 査読有り
Takehide Soh, Katsumi Inoue
Poster presentation at: Systems Biochemistry 2010 2010年
-
Finding Minimal Reaction Sets in Large Metabolic Pathways 査読有り
Takehide Soh, Katsumi Inoue
Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010) 頁： 54 - 54 2010年
-
(2H3-3)SAT問題への変換を用いたフィードバックを含むパスウェイの解析 Open Access
宋 剛秀, 井上克巳
人工知能学会全国大会 2009年6月
-
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem 査読有り
Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
In Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2008年12月
-
A competitive and cooperative approach to propositional satisfiability 査読有り
Katsumi Inoue, Takehide Soh, Seiji Ueda, Yoshito Sasaura, Mutsunori Banbara, Naoyuki Tamura
DISCRETE APPLIED MATHEMATICS 154 巻 ( 16 ) 頁： 2291 - 2306 2006年11月
-
Lemma Reusing for SAT based Planning and Scheduling 査読有り Open Access
Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, Koji Iwanuma
In the proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006) 頁： 103 - 112 2006年
-
Experimental results for solving job-shop scheduling problems with multiple SAT solvers 査読有り
Takehide Soh, Katsumi Inoue, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing (held in conjunction with CP'05) pp.25-38 巻 2005年10月
-
複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査
宋 剛秀, 井上克巳
電子情報通信学会技術研究報告. AI, 人工知能と知識処理 104 巻 ( 133 ) 頁： 19 - 24 2004年6月
MISC 49
-
Large Neighborhood Prioritized Search for Combinatorial Optimization with Answer Set Programming 国際共著 国際誌
Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
CoRRabs/2403.07885 巻 頁： 11p. 2024年5月
-
ハミルトン閉路問題に対するCut-arc集合制約を用いたSAT型CEGAR解法
大橋瞭雅, 宋剛秀, 鍋島英知, 番原睦則, 井上克巳, 田村直之
日本ソフトウェア科学会大会講演論文集(Web)41st 巻 2024年
-
独立集合遷移問題に対する有界組合せ遷移の改良に関する一考察
桑原祥文, 宋剛秀, 盧暁南, 鍋島英知, 番原睦則, 井上克巳, 田村直之
日本ソフトウェア科学会大会講演論文集(Web)41st 巻 2024年
-
ZDDを用いた組合せ遷移ソルバー
伊藤健洋, 川原純, 中畑裕, 宋剛秀, 鈴木顕, 照山順一, 戸田貴久
日本オペレーションズ・リサーチ学会秋季研究発表会アブストラクト集2022 巻 2022年
-
CDCL型SATソルバーの内部動作可視化ツール
堀岡真未, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021年9月
-
ライフゲームを逆向きに動かす
足立啓一, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021年9月
-
SATソルバーを用いた一層平面配置配線問題の解法に関する考察
三嶋哲平, 宋剛秀, 田村直之
日本ソフトウェア科学会第37回大会ポスター発表 2020年9月
-
SAT技術の進化と応用 〜パズルからプログラム検証まで〜：2．SATとパズル -問題をいかにSATソルバーで解くか-
田村 直之, 宋 剛秀, 番原 睦則
情報処理57 巻 ( 8 ) 頁： 710 - 715 2016年7月
-
制約充足問題のハイブリッド符号化に向けて
宋剛秀, 佐古田淳史, 番原睦則, 田村直之
人工知能学会人工知能基本問題研究会資料97th 巻 頁： 65 - 73 2015年3月
-
Scala上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
宋剛秀, 馬場知哉
日本ソフトウエア科学会大会講演論文集(CD-ROM)32nd 巻 頁： ROMBUNNO.SOFUTOWEA1 2015年
-
SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
川原征大, 宋剛秀, 番原睦則, 田村直之
日本ソフトウエア科学会大会講演論文集(CD-ROM)32nd 巻 頁： ROMBUNNO.PPL3-1 2015年
-
iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
日本ソフトウエア科学会大会講演論文集(CD-ROM)32nd 巻 頁： ROMBUNNO.PPL6-1 2015年
-
組合せテストケース生成問題に対する制約解集合プログラミングの適用
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
人工知能学会全国大会論文集2015 巻 ( 0 ) 頁： 2H5OS03b5 - 2H5OS03b5 2015年
-
順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
宋剛秀, 番原睦則, 田村直之
日本ソフトウエア科学会大会講演論文集(CD-ROM)32nd 巻 頁： ROMBUNNO.PPL6-3 2015年
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会大会論文集31 巻 頁： 217 - 231 2014年9月
-
宋 剛秀, 則武 治樹, 番原 睦則
日本ソフトウェア科学会大会論文集31 巻 頁： 140 - 154 2014年9月
-
Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
SOH Takehide, LE BERRE Daniel, ROUSSEL Stephanie, BANBARA Mutsunori, TAMURA Naoyuki
Lect Notes Comput Sci8761 巻 頁： 684 - 693 2014年
-
制約解集合プログラミングシステムの設計方式に関する考察
宋剛秀, 則武治樹, 番原睦則, 田村直之, 井上克巳
日本ソフトウエア科学会大会講演論文集(CD-ROM)31st 巻 頁： ROMBUNNO.PPL2-3 2014年
-
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
コンピュータソフトウェア31 巻 ( 1 ) 頁： 116 - 130 2014年
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
宋剛秀, 番原睦則, 田村直之
日本ソフトウエア科学会大会講演論文集(CD-ROM)31st 巻 頁： ROMBUNNO.SOFUTO1-1 2014年
-
SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用
宋 剛秀, Berre Daniel Le, Roussel Stéphanie, 番原 睦則, 田村 直之
人工知能学会全国大会論文集2014 巻 ( 0 ) 頁： 1D5OS11b6i - 1D5OS11b6i 2014年
-
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
佐古田 淳史, 宋 剛秀, 番原 睦則
人工知能学会全国大会論文集28 巻 頁： 1 - 4 2014年
-
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
佐古田淳史, 宋剛秀, 番原睦則, 田村直之
人工知能学会全国大会論文集(CD-ROM)28th 巻 頁： ROMBUNNO.1D5-OS-11B-7 2014年
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会大会論文集30 巻 頁： 237 - 245 2013年9月
-
則武 治樹, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会大会論文集30 巻 頁： 79 - 92 2013年9月
-
Answer set programming as a modeling language for course timetabling
BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI, SCHAUB TORSTEN
Theor Pract Log Program13 巻 ( 4/5 ) 頁： 783 - 798 2013年7月
-
番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence28 巻 ( 2 ) 頁： 343 - 348 2013年3月
-
番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence28 巻 ( 2 ) 頁： 343 - 348 2013年3月
-
田村 直之, 番原 睦則, 平山 勝敏, 宋 剛秀
コンピュータソフトウェア30 巻 ( 1 ) 頁： 16 - 19 2013年1月
-
正方形詰込み問題の制約モデルとSAT符号化を用いた解法
佐古田 淳史, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会全国大会論文集2013 巻 ( 0 ) 頁： 2E5OS09b1 - 2E5OS09b1 2013年
-
パッキング配列問題の制約モデリングとSAT符号化
則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
日本ソフトウエア科学会大会講演論文集(CD-ROM)30th 巻 頁： 79 - 92 2013年
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
宋剛秀, 番原睦則, 田村直之, LE BERRE Daniel, ROUSSEL Stephanie
日本ソフトウエア科学会大会講演論文集(CD-ROM)30th 巻 頁： 237 - 245 2013年
-
Predicting Gene Knockout Effects on E. coli by Minimal Active Pathway Enumeration
SOH Takehide, INOUE Katsumi, BABA Tomoya, TAKADA Toyoyuki, SHIROISHI Toshihiko
情報処理学会研究報告(CD-ROM)2011 巻 ( 5 ) 頁： ROMBUNNO.ICS-165,NO.7 2012年2月
-
Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems(Foundations of AI,<Special Issue>Doctorial Theses on Aritificial Intelligence)
宋 剛秀
人工知能学会誌27 巻 ( 1 ) 頁： 84 - 84 2012年1月
-
高速SATソルバーの原理(<特集>最近のSAT技術の発展)
鍋島 英知, 宋 剛秀
人工知能学会誌25 巻 ( 1 ) 頁： 68 - 76 2010年1月
-
Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation 査読有り
Takehide Soh, Katsumi Inoue
The Sixth Conference on Prestigious Applications of Intelligent Systems (PAIS 2010)215 巻 頁： 277 - 282 2010年
-
モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
宋 剛秀, 井上 克巳
人工知能学会全国大会論文集24 巻 頁： 1 - 4 2010年
-
高速SATソルバーの原理 査読有り
鍋島英知, 宋 剛秀
人工知能学会論文誌(解説論文)25 巻 ( 1 ) 頁： 68 - 76 2010年
-
SAT問題への変換を用いたフィードバックを含むパスウェイの解析
宋 剛秀, 井上 克巳
論文集23 巻 頁： 1 - 4 2009年
-
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem 査読有り
Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
The 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2008年12月
-
Solving Shop Scheduling Problems by SAT encoding (in Japanese)
Naoyuki Tamura, Akiko Taga, Mutsunori Banbara, Takehide Soh, Hidetomo Nabeshima, Katsumi Inoue
Proceedings of the Scheduling Symposium 2007 頁： 97 - 102 2007年
-
ショップ・スケジューリング問題のSAT変換による解法
田村 直之, 多賀 明子, 番原 睦則, 宋 剛秀, 鍋島 英知, 井上 克巳
スケジューリング・シンポジウム2007講演論文集 頁： 97 - 102 2007年
-
Effective SAT Planning and SAT Scheduling by Lemma Reusing
NABESHIMA Hidetomo, SOH Takehide, INOUE Katsumi, IWANUMA Koji
電子情報通信学会技術研究報告106 巻 ( 38(AI2006 1-11) ) 頁： 19 - 24 2006年5月
-
効率的なSATプランニングとSATスケジューリングのための補題再利用
鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
電子情報通信学会技術研究報告. AI, 人工知能と知識処理106 巻 ( 38 ) 頁： 19 - 24 2006年5月
-
効率的なSATプランニングとSATスケジューリングのための補題利用 (in English)
鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
信学技報, AI2006-4 頁： 19 - 24 2006年
-
Experimental Results for Solving Job-shop Scheduling Problems with Multiple SAT Solvers 査読有り
Takehide Soh, Katsumi Inoue, Mutsunori Banbara, Naoyuki Tamura
In the Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing 頁： 25 - 38 2005年10月
-
A-7-4 Dual-CPU上におけるBlock Lanczos法の並列実装(A-7.情報セキュリティ,基礎・境界)
宋 剛秀, 桑門 秀典, 森井 昌克, 田中 初一
電子情報通信学会ソサイエティ大会講演論文集2005 巻 頁： 177 - 177 2005年9月
-
複数のSATソルバを用いたジョブショップスケジューリング問題の解法
宋 剛秀, 井上 克巳
電子情報通信学会技術研究報告. AI, 人工知能と知識処理104 巻 ( 133 ) 頁： 19 - 24 2004年6月
-
西田 茂生, 宋 剛秀, 馬島 了
奈良工業高等専門学校研究紀要 ( 38 ) 頁： 29 - 34 2002年
講演・口頭発表等 22
-
解集合プログラミングを用いた多層ナンバーリンクの解法
坡山 直樹, 川原 征大, 迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
解集合ソルバーを用いた様相命題論理の充足可能性判定
飯野 有軌, 田村 直之, 宋 剛秀, 番原 睦則, 井上 克巳
第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 2020年 日本ソフトウェア科学会 プログラミング論研究会
-
正規制約のSAT符号化とその性能評価
生田 哲也, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会 2018年8月
-
正規制約に対するSAT符号化手法の提案と評価
生田 哲也, 田村 直之, 宋 剛秀, 番原 睦則
第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 2020年 日本ソフトウェア科学会 プログラミング論研究会
-
正方形詰込み問題の制約モデルとSAT符号化を用いた解法
佐古田 淳史, 宋 剛秀, 番原 睦則, 田村 直之
2013年度人工知能学会全国大会 2013年6月 人工知能学会
-
パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
日本ソフトウェア科学会第30回大会 2013年9月 日本ソフトウェア科学会
-
インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 2016年3月 日本ソフトウェア科学会プログラミング論研究会
-
Towards Incremental SAT-based CSP Solving: Experimental Results for the Hamiltonian Cycle Problem 国際会議
SOH Takehide, FUNAKOSHI Taisuke, TAMURA Naoyuki, BANBARA Mutsunori
The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks 2012年11月 CRIL, NII
-
teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming 国際会議
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
The 28th International Conference on Automated Planning and Scheduling, (ICAPS 2018) 2018年6月
-
System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems 国際会議
Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, Stéphanie Roussel
The 4th International Workshop on Pragmatics of SAT 2013年7月 PoS
-
SugarTracer: SAT型制約ソルバーSugarのトレースツール
吉玉 元和, 寸田 智也, 南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
宋 剛秀, 番原 睦則, 田村 直之
第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015) 2015年3月 日本ソフトウェア科学会プログラミング論研究会
-
Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール
宋 剛秀, 田村 直之, 番原 睦則
第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 2013年3月 日本ソフトウェア科学会
-
Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について
宋 剛秀, 番原 睦則, 田村 直之, Daniel Le Berre, Stéphanie Roussel
日本ソフトウェア科学会第30回大会 2013年9月 日本ソフトウェア科学会
-
SAT型制約ソルバーを用いた多層ナンバーリンクの解法
寸田 智也, 南 雄之, 吉玉 元和, 宋 剛秀
DAシンポジウム2016 2016年9月 情報処理学会 システムとLSIの設計技術研究会（SLDM）
-
SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
寸田 智也, 南 雄之, 宋 剛秀, 田村 直之
DAシンポジウム2017 2017年8月 情報処理学会システムとLSIの設計技術研究会
-
SATソルバーを用いた様相命題論理S4の充足可能性判定
飯野 有軌, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会 2018年8月
-
SATソルバーの最新動向と利用技術
宋 剛秀, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー) 招待有り
宋 剛秀
人工知能学会 第9回AIツール入門講座 2015年12月 人工知能学会
-
PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding 国際会議
Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
The 4th International Workshop on Pragmatics of SAT 2013年7月 PoS
-
CSPSAT Projects and their SAT Related Tools 国際会議
Naoyuki Tamura, Takehide Soh, Mutsunori Banbara, Katsumi Inoue
The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Combined tool demo and poster session 2013年7月 SAT
-
Answer Set Programming as a Modeling Language for Course Timetabling
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
第16回プログラミングおよびプログラミング言語ワークショップ 2014年3月 日本ソフトウェア科学会プログラミング論研究会
科研費 12
-
SAT技術を用いた制約最適化ソルバーの高速化
研究課題/研究課題番号：23K11047 2023年4月 - 2027年3月
日本学術振興会 科学研究費助成事業 基盤研究(C)
宋 剛秀
近年, SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない, 制約充足問題 (CSP) をSAT問題に符号化(SAT符号化)して解くSAT型CSPソルバーが成功している. 本研究では,対象を CSP から制約最適化問題 (COP) へ発展させる.
本研究の目的は, SATソルバーを用いた高速なSAT型COPソルバーを実現することである. そのために2つの方法を研究する.1つは,目的関数を表す線形比較制約の MDD (Multi‐valued Decision Diagram) を用いた表現とその符号化方法である.もう1つの方法は極小モデル生成を用いた新しい最適化方法である.
具体的な研究課題は4つある．(A) MDD を用いた線形比較制約の符号化の研究開発, (B) 極小モデル生成の研究開発, (C) 提案方法を用いたSAT型COPソルバーの実装, (D) 提案SAT型COPソルバーの特長的なアプリケーションの研究開発. それぞれの研究課題は密接に関係しているため逐次的に進めるのではなく同時並行的に取り組む計画である.2023年度は (A), (B), (C), (D) それぞれに取り組んだ．(A) については，MDDと似た圧縮データ構造である ZDD を用いた疑似ブール制約の符号化について研究を行い，発表した．(B) については，適用できる問題は限定されるものの符号化を用いた極小モデル生成方法を考案することができた．得られた成果を発表する準備を現在行っている．(C) については，また最新の制約への対応を実装したソルバーsCOPが国際ソルバー競技会XCSP3で準優勝 (CSP部門)という成績を収めた．(D) についてはシステム生物学および組合せ遷移問題の解法を研究し，国際会議で4件論文発表した． -
制約充足問題に対する新しいSAT解法技術の研究開発
研究課題/研究課題番号：22K11973 2022年4月 - 2025年3月
日本学術振興会 科学研究費助成事業 基盤研究(C)
田村 直之, 宋 剛秀, 番原 睦則
-
SAT技術に基づく系統的探索と確率的探索の統合的技法の研究開発
研究課題/研究課題番号：21K11828 2021年4月 - 2024年3月
日本学術振興会 科学研究費助成事業 基盤研究(C)
番原 睦則, 田村 直之, 宋 剛秀
近年，SAT技術の適用範囲を Beyond NP に拡大しようとする試みが国際的に活発化し，その重要課題として「モデル計数」，「知識コンパイラ」，「高階ソルバー」，「最適化や極小問題等への対応」が挙げれている．本研究では，「最適化や極小問題等への対応」に着目し，SAT技術を用いて系統的探索と確率的局所探索を統合的かつ効率的に扱うアルゴリズム技法およびソルバーの研究開発を行う．
<BR>
3年計画の初年度である2021年度は，国際ワークショップ発表1件，国内学会の大会での発表6件，国内研究会での発表4件，学生奨励賞受賞1件の成果を得た．
<BR>
組合せ最適化問題に対して系統的探索と確率的局所探索を統合的に適用する探索手法である優先度付き巨大近傍探索 (LNPS: Large Neighborhood Prioritized Search) を改良し，解集合プログラミング (Answer Set Programming; ASP) システム上に実装した．提案手法の有効性を評価するために，カリキュラムベース・コース時間割問題集(全61問)を用いて実験を行った．その結果，提案手法は61問中11問について，既知の最良値を更新することに成功した．また，通常の ASP 解法と比較して，既知の最良値との比を+472%から+53%に大幅に改善することができた．さらに，提案手法の特長的なアプリケーションの開発に向けて，時間割問題に加え，配電網問題，車両装備仕様問題などへの応用研究も行なった． -
工学アプローチによる組合せ遷移の展開：配電切替を足がかりとして汎用ソルバーへ
研究課題/研究課題番号：20H05794 2020年10月 - 2023年3月
日本学術振興会 科学研究費助成事業 学術変革領域研究(B)
川原 純, 飯岡 大輔, 戸田 貴久, 宋 剛秀, 鈴木 顕, 照山 順一, 中畑 裕
本研究では組合せ遷移の実装技術の構築とその産業応用に向けて、研究開発の共通基盤となるソフトウェア開発を目標とする。初年度にあたる本年度は、広く知られているグラフの独立集合の遷移問題（独立集合遷移問題）に対して、4種のアプローチを検討した。1つ目は、組合せ遷移の技法を用いたアルゴリズムの設計であり、主に、状態空間の部分探索の手法を検討した。2つ目は、SAT（充足可能性問題）ソルバーを活用するアプローチである。有限整数領域上の制約を命題論理式へと変換する SAT 符号化を行い、SATソルバーの強力な推論性能を用いて独立集合遷移問題を解くソルバーを開発した。3つ目は、ゼロサプレス型二分決定グラフ (ZDD) を活用するアプローチである。当初予定では、ZDD を上記2手法に援用した高速化を想定していたが、本研究において、ZDD が表す独立集合族を直接遷移させるアルゴリズムの開発に成功したため、ZDD を単独で用いて独立集合遷移問題を解くことが可能になった。4つ目の手法は、当初は予定していない新たな構想であるが、モデル検査と呼ばれる、システムの形式的な検査を可能にする技術を用いた手法である。入力グラフと開始、目標独立集合が与えられた際に、開始集合から目標集合に遷移可能ではないことを検証する記述をモデル検査ソルバーに与え、遷移可能な場合は反例として解となる遷移列を出力する。
以上の4つの技法について、アルゴリズム設計と実装を行った。アルゴリズムの比較実験のためには、適切な入力データが必要であるが、組合せ遷移問題に対する広く知られたベンチマークデータは存在しないため、入力データの作成整備を行った。
配電切替への組合せ遷移技術の適用についても研究を行い、配電切替を全域木遷移問題として定式化し、4つの技法の適用を検討して、実装を行っている。 -
MDDを用いたSAT型CSPソルバーの高速化
研究課題/研究課題番号：20K11748 2020年4月 - 2023年3月
日本学術振興会 科学研究費助成事業 基盤研究(C) 基盤研究(C)
宋 剛秀
近年， 命題論理式の充足可能性判定問題 (SAT問題) を解くプログラムであるSATソルバーの飛躍的な進歩にともない， 制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している． 本研究の目的は， SAT型CSPソルバーの高速化であり, そのために MDD (Multi-valued Decision Diagram) を用いたCSPの正規化と， MDD が表す制約 (MDD制約) のSAT符号化を研究開発する． 本研究の意義は, SAT型CSPソルバーの新しい一方式を開拓できる点， 既存のCSPソルバーでは求解困難な問題に対して， より高性能な推論基盤を提供できる点である． CSPソルバーはスケジューリング問題, パッキング問題, 時間割問題, クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く， 研究成果の産業分野への応用も期待できる．
<BR>
2021年度は研究計画に記載された「(B) MDD 制約の SAT 符号化の研究開発」の研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った． (C) については， CEGAR (Counterexample-guided Abstraction Refinement) の並列化とSATソルバーを用いたハミルトン閉路問題への応用を研究し， 査読付き国際ワークショップで発表を行った． -
先進的な知識表現および推論技術を基盤とした多目的最適化ソルバーの研究開発
2018年4月 - 2021年3月
学術研究助成基金助成金／基盤研究(C)
番原 睦則
資金種別：競争的資金
-
SATを基盤とした新しい制約プログラミングシステムの研究開発
2016年4月 - 2019年3月
科学研究費補助金／基盤研究(B)
田村 直之
資金種別：競争的資金
-
ハイブリッド符号化を用いた高性能なSAT型制約プログラミングシステム
2016年4月 - 2019年3月
学術研究助成基金助成金／若手研究(B)
宋 剛秀
担当区分：研究代表者 資金種別：競争的資金
-
SAT符号化を用いた制約解集合プログラミングに関する研究開発
2015年4月 - 2018年3月
学術研究助成基金助成金／基盤研究(C)
番原 睦則
資金種別：競争的資金
-
代謝パスウェイ解析のための制約プログラミングシステムの研究開発
2013年 - 2015年
文部科学省 科学研究費補助金(若手研究(B))
宋 剛秀
担当区分：研究代表者 資金種別：競争的資金
配分額：2340000円 （ 直接経費：1800000円 、 間接経費：540000円 ）
近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライ
-
命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現
2012年 - 2014年
文部科学省 科学研究費補助金(基盤研究(B))
田村 直之
資金種別：競争的資金
当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進めた．「A. フレキシブル制約に関する研究開発」については，フレキシブル制約のSAT符号化で重要になる擬似ブール制約の符号化方法の研究，PBSugarシステムの開発，および論文発表を行った．「B. 動的な制約変更に関する研究開発」については，動的な制約変更が可能なScarabシステムの開発および論文発表を行った．「C. ドメイン拡張に関する研究開発」については，記号推論が可能な解集合プログラミングシステム上で整数上の制約記述を可能にするプロトタイプシステムを開発し，性能評価を行った．「D. 応用研究開発」については，各種問題の評価を進めた．特に，時間割問題について優れた結果を得，論文発表を行った．また，「論理と推論の理論，実装，応用に関する合同セミナー」のERATO
-
SAT変換を用いた制約充足問題の解法とシステム生物学への応用
研究課題/研究課題番号：10J02321 2010年 - 2011年
日本学術振興会 科学研究費助成事業 特別研究員奨励費
宋 剛秀
最終年度の報告として、これまでの研究成果について以下にまとめる。
本研究では化学反応法則を満たしつつ入力代謝物集合から出力代謝物集合を生成可能なパスウェイを活性パスウェイ呼び、特にその包含関係において極小なものを極小活性パスウェイと呼ぶ。研究ではまず極小活性パスウェイを列挙する問題を極小活性パスウェイ同定問題として定義を行った。代謝パスウェイの解析を行う際には既存のデータから問題を構築する必要がある。そこで更新頻度において優れていることから、生物学的知識のデータベースEcoCyc(http://ecocyc.org/)から問題を構成して評価を行った。このデータから構成した問題をSAT技術によって解くために本研究では次の枠組みを用いた:(1)まず問題を命題論理式に符号化する、(2)SATソルバを漸増的に適用するインクリメンタルSAT解法を用いて符号化された命題論理式から極小モデルを計算する、(3)得られた極小モデルを逆符号化することで問題の解である極小活性パスウェイを得る。
提案した問題および解法の評価のためにEcoCycのデータから極小活性パスウェイ同定問題を構成し、SAT技術を用いて解を求めた。結果として9個の極小活性パスウェイを同定し、その中の2個が生物学における既存の知識と一致したパスウェイ(参照パスウェイ)であることを確認している。また専門家との議論で提案された制約を命題論理式に追加することでより精緻なパスウェイを計算することに成功した。この成果は国内雑誌論文として発表を行った。また代謝パスウェイに対する解集合プログラミングを用いた解析研究についても国際会議の会議録で発表を行った。
さらにより具体的な生物学の問題に適用するために、大腸菌における単一遺伝子ノックアウトの影響予測を極小活性パスウェイの同定によって行う手法の研究を国立遺伝学研究所の研究チームと共同して進めた。大腸菌の解糖系に対して計算機実験を行った結果,提案手法の予測が生物実験の結果とよく一致することを確認した。この成果は国際会議において発表を行った。
担当経験のある科目 (本学以外) 11
-
Advanced Course on Programming Languages
（Kobe University）
-
言語工学（-15）
（神戸大学）
-
言語工学
（神戸大学）
-
情報基礎特論
（神戸大学）
-
情報基礎
（神戸大学）
-
プログラミング言語論及び演習（-15）
（神戸大学）
-
プログラミング言語特論
（神戸大学）
-
Theory of Programming Languages
（Kobe University）
-
Paradigm of Programming Languages and Practice
（Kobe University）
-
Introduction to Computer Literacy
（Kobe University）
-
Advanced Theory of Informatics
（Kobe University）