所属
大学院情報学研究科 情報システム学専攻 計算論 准教授
大学院担当
大学院情報学研究科
学部担当
情報学部 コンピュータ科学科
職名
准教授
ホームページ
外部リンク
ソウ タケヒデ
宋 剛秀
SOH Takehide
学位 1
-
博士 (情報学) （ 2011年9月 総合研究大学院大学 ）
研究キーワード 3
-
システム生物学
-
命題論理の充足可能性判定 (SAT)
-
制約プログラミング
研究分野 4
-
情報通信 / ソフトウェア
-
情報通信 / 情報学基礎論
-
情報通信 / 生命、健康、医療情報学
-
情報通信 / 知能情報学
経歴 5
-
名古屋大学 大学院情報学研究科 情報システム学専攻 准教授
2025年8月 - 現在
-
神戸大学 DX・情報統括本部 准教授
2022年4月 - 2025年7月
-
神戸大学 情報基盤センター 准教授
2019年4月 - 2022年3月
-
神戸大学 助教
2012年4月 - 2019年3月
-
サントリー株式会社
2006年4月 - 2008年3月
学歴 3
-
総合研究大学院大学
2008年4月 - 2011年9月
-
神戸大学 大学院自然科学研究科 電気電子工学専攻
2004年4月 - 2006年3月
-
神戸大学 工学部 電気電子工学科
2002年4月 - 2004年3月
国名： 日本国
所属学協会 4
-
人工知能学会
-
情報処理学会
-
日本ソフトウェア科学会
-
電子情報通信学会
委員歴 40
-
プログラミングおよびプログラミング言語ワークショップ プログラム共同委員長
2026年
-
プログラミングおよびプログラミング言語ワークショップ プログラム委員
2025年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2025年
-
人工知能学会 全国大会 オーガナイズドセッション: AI と制約プログラミング オーガナイザ
2024年
-
International Symposium on Combinatorial Search (SoCS) Program Committee
2024年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2024年
-
人工知能学会 全国大会 オーガナイズドセッション: AI と制約プログラミング オーガナイザ
2023年
-
International Symposium on Combinatorial Search (SoCS) Program Committee
2023年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2023年
-
人工知能学会 全国大会 オーガナイズドセッション: AI と制約プログラミング オーガナイザ
2022年
-
プログラミングおよびプログラミング言語ワークショップ プログラム委員
2022年
-
International Symposium on Combinatorial Search (SoCS) Program Committee
2022年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2022年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2022年
-
Annual AAAI Conference on Artificial Intelligence (AAAI) Program Committee
2022年
-
人工知能学会 全国大会 オーガナイズドセッション: AI と制約プログラミング オーガナイザ
2021年
-
International Symposium on Combinatorial Search (SoCS) Program Committee
2021年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2021年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2021年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2020年
-
日本ソフトウェア科学会 編集委員
2019年4月 - 現在
-
情報処理学会・論文誌プログラミング 編集委員
2019年4月 - 2023年3月
-
情報処理学会・プログラミング研究会 運営委員
2019年4月 - 2023年3月
-
International Workshop on Pragmatics of SAT (PoS) Program Committee
2019年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2019年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2018年
-
プログラミングおよびプログラミング言語ワークショップ プログラム委員
2017年
-
International Workshop on Pragmatics of SAT (PoS) Program Committee
2017年
-
International Joint Conferences on Artificial Intelligence (IJCAI) Program Committee
2017年
-
Doctoral Consortium of International Conference on Logic Programming Program Committee
2017年
-
人工知能学会 全国大会 オーガナイズドセッション: SAT 技術の理論，実装，応用 オーガナイザ
2016年
-
International Conference on Theory and Applications of Satisfiability Testing (SAT) Program Committee
2016年
-
Doctoral Consortium of International Conference on Logic Programming Program Committee
2016年
-
人工知能学会 全国大会 オーガナイズドセッション: SAT 技術の理論，実装，応用 オーガナイザ
2015年
-
プログラミングおよびプログラミング言語ワークショップ プログラム委員
2015年
-
International Workshop on Pragmatics of SAT (PoS) Program Committee
2015年
-
Doctoral Consortium of International Conference on Logic Programming Program Committee
2015年
-
人工知能学会 全国大会 オーガナイズドセッション: SAT 技術の理論，実装，応用 オーガナイザ
2014年
-
Doctoral Consortium of International Conference on Logic Programming Program Committee
2014年
-
人工知能学会 全国大会 オーガナイズドセッション: SAT 技術の理論，実装，応用 オーガナイザ
2013年
受賞 18
-
2023 XCSP23 Main CSP部門 準優勝
2023年8月 XCSP Competition Organization Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura
-
10-year Test-of-Time Award (ICLP 2023)
2023年7月 International Conference on Logic Programming ICLP 2023
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue and Torsten Schaub
-
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
-
PPL2017発表賞（一般の部）
2017年3月 日本ソフトウェア科学会 プログラミング論研究会 SATソルバーの最新動向と利用技術
宋 剛秀, 田村 直之
-
2016年度全国大会優秀賞
2017年3月 人工知能学会 SAT型制約ソルバーによるナンバーリンクの解法とその評価
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
-
第20回研究論文賞
2016年3月 日本ソフトウェア科学会 パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
-
最優秀賞
2015年8月 情報処理学会DAシンポジウム2015 SAT型制約ソルバーを用いたナンバーリンクの求解と解の最適化
迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
-
アルゴリズムデザインコンテスト2015 最優秀賞 (DAシンポジウム2015)
2015年8月 情報処理学会 SLDM研究会 iSugar+GlueMiniSat
迫 龍哉, 川原 征大, 田村 直之, 番原 睦則, 宋 剛秀, 鍋島 英知
-
第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月 人工知能学会 モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
宋 剛秀
論文 46
-
The ASP-based Nurse Scheduling System at the University of Yamanashi Hospital 査読有り 国際共著
In Martin Gebser, Daniela Inclezan, Francesco Ricca, Manuel Carro and Miroslaw Truszczynski: Proceedings 41st International Conference on Logic Programming (ICLP 2025), Rende, Italy, 12-19th September 2025, Electronic Proceedings in Theoretical Computer Science 439 巻 頁： 334 - 348 2026年1月
-
SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints 査読有り 国際共著
Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, Naoyuki Tamura
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) 頁： 24:1 - 24:10 2025年8月
-
ASP-Based Large Neighborhood Prioritized Search for Course Timetabling 査読有り 国際共著
Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
Proceedings of the 17th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2024) 15245 巻 頁： 57 - 70 2025年
-
A SAT-based Method for Counting All Singleton Attractors in Boolean Networks 査読有り 国際共著
Rei Higuchi, Takehide Soh, Daniel Le Berre, Morgan Magnin, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2025) 頁： 2601 - 2609 2025年
-
Dominating Set Reconfiguration with Answer Set Programming 査読有り 国際共著
Masato Kato, Mutsunori Banbara, Torsten Schaub, Takehide Soh, Naoyuki Tamura
Theory and Practice of Logic Programming 24 巻 ( 4 ) 頁： 755 - 771 2024年7月
-
Proceedings of the International Symposium on Combinatorial Search 17 巻 頁： 285 - 286 2024年6月
-
Scalable Hard Instances for Independent Set Reconfiguration. 査読有り
22nd International Symposium on Experimental Algorithms(SEA) 頁： 26 - 15 2024年
-
A Study on Production Scheduling Methods for Ready-Made Meal Industries. 査読有り
APMS (2) 頁： 266 - 277 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月
-
ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems. 査読有り
CPAIOR 頁： 167 - 183 2023年
-
35th IEEE International Conference on Tools with Artificial Intelligence(ICTAI) 頁： 294 - 302 2023年
-
SAF: SAT-Based Attractor Finder in Asynchronous Automata Networks 査読有り 国際共著
Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the International Conference on Computational Methods in Systems Biology (CMSB 2023) 14137 巻 頁： 175 - 183 2023年
-
Towards CEGAR-based Parallel SAT Solving 査読有り
Proceedings of the Pragmatics of SAT 2021 2021年7月
-
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符号化手法 査読有り
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
コンピュータソフトウェア 35 巻 ( 3 ) 頁： 65 - 78 2018年8月
-
SATソルバーの最新動向と利用技術 査読有り
宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
コンピュータ ソフトウェア 35 巻 ( 4 ) 頁： 72 - 92 2018年
-
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 ) 頁： 1 - 29 2017年2月
-
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年
-
宋 剛秀, 番原 睦則, 田村 直之
コンピュータ ソフトウェア 34 巻 ( 1 ) 頁： 1_67 - 1_80 2017年
-
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年
-
An incremental SAT solving library and its applications 査読有り
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解法ライブラリとその応用 査読有り
迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知, 井上 克巳
コンピュータソフトウェア 33 巻 ( 4 ) 頁： 16 - 29 2016年7月
-
Teaspoon: Solving the curriculum-based course timetabling problems with answer set programming 査読有り 国際共著
PATAT 2016 - Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling 頁： 13 - 32 2016年
-
A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings 査読有り
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
Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, Lexington, KY, USA, September 27-30, 2015. Proceedings 9345 巻 頁： 112 - 126 2015年
-
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月
-
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
コンピュータソフトウェア 31 巻 ( 1 ) 頁： 116 - 130 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 8761 巻 頁： 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) 頁： 1020 - 1027 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) 論文集 15 巻 2013年3月
-
System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems⋆ 査読有り 国際共著
In the Proceedings of Pragmatics of SAT 2013 (PoS-13) 頁： 1 - 14 2013年
-
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年
-
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月
-
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月
-
モデル生成を用いた代謝ネットワークにおける極小活性パスウェイの列挙 査読有り
宋剛秀
人工知能学会論文誌 27 巻 ( 3 ) 頁： 204 - 212 2012年
-
Analyzing pathways using ASP-based approaches 査読有り 国際共著
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6479 巻 頁： 167 - 183 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月
-
高速SATソルバーの原理 査読有り
鍋島英知, 宋剛秀
人工知能学会論文誌(解説論文) 25 巻 ( 1 ) 頁： 68 - 76 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年
-
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem 査読有り
Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 451 巻 ( 16 ) 頁： 25 - 39 2008年12月
-
A competitive and cooperative approach to propositional satisfiability 査読有り
DISCRETE APPLIED MATHEMATICS 154 巻 ( 16 ) 頁： 2291 - 2306 2006年11月
-
Lemma Reusing for SAT based Planning and Scheduling 査読有り
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月
MISC 8
-
The ASP-based Nurse Scheduling System at the University of Yamanashi Hospital 国際誌
abs/2506.13600 巻 2025年6月
-
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/2405.11305 巻 頁： 11p. 2024年5月
-
Core Challenge 2022: Solver and Graph Descriptions. 国際誌
CoRRabs/2208.02495 巻 2022年9月
-
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年
-
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年
-
SAT技術の進化と応用 〜パズルからプログラム検証まで〜：2．SATとパズル -問題をいかにSATソルバーで解くか-
田村 直之, 宋 剛秀, 番原 睦則
情報処理57 巻 ( 8 ) 頁： 710 - 715 2016年7月
-
番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence28 巻 ( 2 ) 頁： 343 - 348 2013年3月
-
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月
講演・口頭発表等 76
-
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 2007年9月26日 スケジューリング学会
-
SugarTracer: SAT型制約ソルバーSugarのトレースツール
吉玉 元和, 寸田 智也, 南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
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
-
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
-
ZDDを用いた組合せ遷移ソルバー
伊藤健洋, 川原純, 中畑裕, 宋剛秀, 鈴木顕, 照山順一, 戸田貴久
日本オペレーションズ・リサーチ学会秋季研究発表会アブストラクト集 2022年9月15日 日本オペレーションズ・リサーチ学会
-
インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 2016年3月 日本ソフトウェア科学会プログラミング論研究会
-
カリキュラムベースのコース時間割問題の擬似ブール最適化問題への符号化
鈴江 美奈, 田村 直之, 番原 睦則
日本ソフトウェア科学会大会論文集 2012年8月22日 [日本ソフトウェア科学会]
-
クラウド上のソフトウェア要素最適配置問題の解法 (特集 「命題論理の充足可能性問題SATと応用技術」および一般)
田村 直之, 井上 克巳, 鍋島 英知, 番原 睦則, 宋 剛秀
人工知能基本問題研究会 2016年3月27日 人工知能学会
-
ショップ・スケジューリング問題のSAT変換による解法
田村 直之, 多賀 明子, 番原 睦則, 宋 剛秀, 鍋島 英知, 井上 克巳
スケジューリング・シンポジウム2007講演論文集 2007年9月26日 スケジューリング学会
-
チャネリング制約を用いた alldifferent 制約の SAT 符号化
小菅脩司, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022年3月
-
ハミルトン閉路問題に対するCut-arc集合制約を用いたSAT型CEGAR解法
大橋瞭雅, 宋剛秀, 鍋島英知, 番原睦則, 井上克巳, 田村直之
第41回日本ソフトウェア科学会大会講演論文集 2024年9月9日 日本ソフトウェア科学会
-
パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
日本ソフトウェア科学会第30回大会 2013年9月 日本ソフトウェア科学会
-
ブール基数制約を経由した擬似ブール制約のSAT符号化手法
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会大会論文集 2017年9月18日 日本ソフトウェア科学会
-
ブール基数制約を経由した擬似ブール制約のSAT符号化法
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会研究会資料 人工知能基本問題研究会 2017年 一般社団法人 人工知能学会
-
モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
宋 剛秀, 井上 克巳
人工知能学会全国大会論文集 2010年 人工知能学会
-
ライフゲームを逆向きに動かす
足立啓一, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021年9月10日 日本ソフトウェア科学会
-
分子ネットワーク上の状態推定とその可視化による知識発見支援
平沼 祐人, 山本 泰生, 守屋 央朗, 宋 剛秀, 岩沼 宏治
第45回バイオ情報学研究発表会 2016年3月 情報処理学会
-
制約充足問題のASP符号化に関する一考察
坡山 直樹, 番原 睦則, 宋 剛秀, 田村 直之
人工知能学会全国大会論文集 2017年 一般社団法人 人工知能学会
-
制約充足問題のハイブリッド符号化に向けて
宋剛秀, 佐古田淳史, 番原睦則, 田村直之, 宋 剛秀, 佐古田 淳史, 番原 睦則, 田村 直之
人工知能学会人工知能基本問題研究会資料 2015年3月18日 人工知能学会
-
制約解集合プログラミングシステムの設計方式に関する考察
宋 剛秀, 則武 治樹, 番原 睦則
日本ソフトウェア科学会大会論文集 2014年9月7日 [日本ソフトウェア科学会]
-
効率的なSATプランニングとSATスケジューリングのための補題再利用
鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
電子情報通信学会技術研究報告. AI, 人工知能と知識処理 2006年5月11日 一般社団法人電子情報通信学会
-
効率的なSATプランニングとSATスケジューリングのための補題利用 (in English)
鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
信学技報, AI2006-4 2006年
-
周波数解析を用いた日本語母音の特性に関する研究
西田 茂生, 宋 剛秀, 馬島 了
奈良工業高等専門学校研究紀要 2002年 奈良工業高等専門学校
-
有界モデル検査による独立集合遷移問題の解法に関する考察
戸田 貴久, 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一
情報処理学会 研究報告アルゴリズム（AL） 2022年1月
-
正方形詰込み問題の制約モデルとSAT符号化を用いた解法
佐古田 淳史, 宋 剛秀, 番原 睦則, 田村 直之
2013年度人工知能学会全国大会 2013年6月 人工知能学会
-
正規制約に対するSAT符号化手法の提案と評価
生田 哲也, 田村 直之, 宋 剛秀, 番原 睦則
第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 2020年 日本ソフトウェア科学会 プログラミング論研究会
-
正規制約のSAT符号化とその性能評価
生田 哲也, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会 2018年8月
-
独立集合遷移問題に対する有界組合せ遷移の改良に関する一考察
桑原祥文, 宋剛秀, 盧暁南, 鍋島英知, 番原睦則, 井上克巳, 田村直之
第41回日本ソフトウェア科学会大会講演論文集 2024年9月9日 日本ソフトウェア科学会
-
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
佐古田 淳史, 宋 剛秀, 番原 睦則
人工知能学会全国大会論文集 2014年 人工知能学会
-
組合せテストケース生成問題に対する制約解集合プログラミングの適用
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
人工知能学会全国大会論文集 2015年 一般社団法人 人工知能学会
-
複数のSATソルバを用いたジョブショップスケジューリング問題の解法
宋 剛秀, 井上 克巳
電子情報通信学会技術研究報告. AI, 人工知能と知識処理 2004年6月14日 一般社団法人電子情報通信学会
-
複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査
宋 剛秀, 井上克巳
電子情報通信学会技術研究報告. AI, 人工知能と知識処理 2004年6月 社団法人電子情報通信学会
-
解集合ソルバーを用いた様相命題論理の充足可能性判定
飯野 有軌, 田村 直之, 宋 剛秀, 番原 睦則, 井上 克巳
第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020) 2020年 日本ソフトウェア科学会 プログラミング論研究会
-
解集合プログラミングによるカリキュラムベース・コース時間割編成 招待有り
番原 睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋 剛秀, 田村 直之, フィリップ ワンコ
第29回RAMPシンポジウム論文集 2017年 日本オペレーションズ・リサーチ学会 常設研究部会数理計画
-
解集合プログラミングによる様相命題論理Kの充足可能性判定
飯野 有軌, 田村 直之, 宋 剛秀, 番原 睦則, 井上 克巳
人工知能学会全国大会論文集 2020年 一般社団法人 人工知能学会
-
解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価
桑原和也, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022年3月
-
解集合プログラミングを用いた制約組合せテストケース生成
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, 沖本 天太
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 2016年3月
-
解集合プログラミングを用いた多層ナンバーリンクの解法
坡山 直樹, 川原 征大, 迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
宋剛秀, 番原睦則, 田村直之, 宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウエア科学会大会講演論文集(CD-ROM) 2015年9月9日 日本ソフトウェア科学会
-
SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー) 招待有り
宋 剛秀
人工知能学会 第9回AIツール入門講座 2015年12月 人工知能学会
-
SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用
宋 剛秀, Berre Daniel Le, Roussel Stéphanie, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2014年 一般社団法人 人工知能学会
-
SATソルバーの使い方 —問題をSATに符号化する方法—
田村 直之, 宋 剛秀, 番原 睦則
第58回プログラミング・シンポジウム予稿集 2017年1月 情報処理学会
-
SATソルバーの最新動向と利用技術
宋 剛秀, 田村 直之
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017年3月 日本ソフトウェア科学会 プログラミング論研究会
-
SATソルバーを用いた一層平面配置配線問題の解法に関する考察
三嶋哲平, 宋剛秀, 田村直之
日本ソフトウェア科学会第37回大会ポスター発表 2020年9月10日 日本ソフトウェア科学会
-
SATソルバーを用いた制約プログラミングシステムとその応用
宋 剛秀
第57回プログラミング・シンポジウム 2016年1月 情報処理学会
-
SATソルバーを用いた様相命題論理S4の充足可能性判定
飯野 有軌, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会 2018年8月
-
SATソルバーを用いた部分グラフ探索のための制約モデル
川原 征大, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2016年 一般社団法人 人工知能学会
-
SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
川原征大, 宋剛秀, 番原睦則, 田村直之, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウエア科学会大会講演論文集(CD-ROM) 2015年9月9日 日本ソフトウェア科学会
-
SAT問題への変換を用いたフィードバックを含むパスウェイの解析
宋 剛秀, 井上 克巳
論文集 2009年 人工知能学会
-
SAT型制約ソルバーによるナンバーリンクの求解と解の最適化
迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
DAシンポジウム2015 2015年
-
SAT型制約ソルバーによるナンバーリンクの解法とその評価
迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
人工知能学会全国大会論文集 2016年 一般社団法人 人工知能学会
-
SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
寸田 智也, 南 雄之, 宋 剛秀, 田村 直之
DAシンポジウム2017 2017年8月 情報処理学会システムとLSIの設計技術研究会
-
SAT型制約ソルバーを用いたナンバーリンクの解法
田村 直之, 宋 剛秀, 番原 睦則, 鍋島 英知
DAシンポジウム2014論文集 2014年8月21日 情報処理学会システムとLSIの設計技術研究会
-
SAT型制約ソルバーを用いた多層ナンバーリンクの解法
寸田 智也, 南 雄之, 吉玉 元和, 宋 剛秀
DAシンポジウム2016 2016年9月 情報処理学会 システムとLSIの設計技術研究会（SLDM）
-
SAT技術を用いたペトリネットのデッドロック検出手法の提案
寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2017年 一般社団法人 人工知能学会
-
Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について
宋 剛秀, 番原 睦則, 田村 直之, Daniel Le Berre, Stéphanie Roussel
日本ソフトウェア科学会第30回大会 2013年9月 日本ソフトウェア科学会
-
Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
宋 剛秀, 馬場 知哉
日本ソフトウェア科学会第32回大会 2015年9月 日本ソフトウェア科学会
-
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
宋 剛秀, 番原 睦則, 田村 直之
日本ソフトウェア科学会大会論文集 2014年9月7日 [日本ソフトウェア科学会]
-
Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール
宋 剛秀, 田村 直之, 番原 睦則
第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 2013年3月 日本ソフトウェア科学会
-
Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
宋 剛秀, 番原 睦則, 田村 直之
第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015) 2015年3月 日本ソフトウェア科学会プログラミング論研究会
-
Predicting Gene Knockout Effects on E. coli by Minimal Active Pathway Enumeration
SOH Takehide, INOUE Katsumi, BABA Tomoya, TAKADA Toyoyuki, SHIROISHI Toshihiko
情報処理学会研究報告(CD-ROM) 2012年2月15日
-
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) 2010年
-
heulingo: 組合せ最適化のための解集合プログラミングに基づく優先度付き巨大近傍探索の実装
杉森 唯瑠未, 宋 剛秀, 田村 直之, 井上 克巳, 鍋島 英知, 番原 睦則
第26回プログラミングおよびプログラミング言語ワークショップ (PPL 2024) 2024年
-
Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー
宋 剛秀, 番原 睦則, 田村 直之
第58回プログラミング・シンポジウム予稿集 2017年1月 情報処理学会
-
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
-
CEGARと反例の共有を用いたSAT型CSPソルバーの並列化方法の考察 (特集 「命題論理の充足可能性問題SATの最新動向」および一般)
宋 剛秀, 鍋島 英知, 番原 睦則, 田村 直之, 井上 克巳
人工知能基本問題研究会 2020年3月8日 人工知能学会
-
CDCL型SATソルバーの内部動作可視化ツール
堀岡真未, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021年9月10日 日本ソフトウェア科学会
-
Answer Set Programming as a Modeling Language for Course Timetabling
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
第16回プログラミングおよびプログラミング言語ワークショップ 2014年3月 日本ソフトウェア科学会プログラミング論研究会
-
An Implementation of Model-based Abduction and its Application to Systems Biology 国際会議
Takehide Soh, Katsumi Inoue
The 3rd Franco-Japanese Symposium on Knowledge Discovery in Systems Biology (FJ'09), Bastia, France 2009年
-
alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用
大野周亮, 番原睦則, 宋剛秀, 田村 直之
人工知能学会研究会資料 2019年3月 人工知能学会
-
A-7-4 Dual-CPU上におけるBlock Lanczos法の並列実装(A-7.情報セキュリティ,基礎・境界)
宋 剛秀, 桑門 秀典, 森井 昌克, 田中 初一
電子情報通信学会ソサイエティ大会講演論文集 2005年9月7日 一般社団法人電子情報通信学会
-
A SAT-based Method for Analyzing Metabolic Pathways 国際会議
Takehide Soh, Katsumi Inoue
Poster presentation at: Systems Biochemistry 2010 2010年
-
A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
宋 剛秀, Le Berre Daniel, 番原 睦則, 田村 直之
人工知能学会全国大会論文集 2019年 一般社団法人 人工知能学会
-
A SAT-based Approach for Analyzing Biochemical Pathways 国際会議
Takehide Soh, Katsumi Inoue
The 2nd Franco-Japanese Symposium on Knowledge Discovery in Systems Biology (FJ'08), Takayama, Japan 2008年
-
(2H3-3)SAT問題への変換を用いたフィードバックを含むパスウェイの解析
宋 剛秀, 井上克巳
人工知能学会全国大会 2009年6月
-
iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳, 迫 龍哉, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知, 井上 克巳
日本ソフトウエア科学会大会講演論文集(CD-ROM) 2015年9月9日 日本ソフトウェア科学会
科研費 14
-
解集合プログラミングに基づく組合せ遷移問題の汎用解法と遷移最適化への拡張
研究課題/研究課題番号：25K03097 2025年4月 - 2028年3月
日本学術振興会 科学研究費助成事業 基盤研究(B)
番原 睦則, 鍋島 英知, 宋 剛秀
資金種別：競争的資金
-
解空間の形状に着目した組合せ遷移の理論：計算量解析の高精細化とソルバー新技法
研究課題/研究課題番号：24H00686 2024年4月 - 2028年3月
日本学術振興会 科学研究費助成事業 基盤研究(A)
伊藤 健洋, 宋 剛秀, 小林 靖明, 野崎 雄太
資金種別：競争的資金
-
SAT技術を用いた制約最適化ソルバーの高速化
研究課題/研究課題番号：23K11047 2023年4月 - 2027年3月
日本学術振興会 科学研究費助成事業 基盤研究(C)
宋 剛秀
担当区分：研究代表者
配分額：4160000円 （ 直接経費：3200000円 、 間接経費：960000円 ）
近年, 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年4月 - 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)
宋 剛秀
担当区分：研究代表者
配分額：4290000円 （ 直接経費：3300000円 、 間接経費：990000円 ）
近年， 命題論理式の充足可能性判定問題 (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ソルバーを用いたハミルトン閉路問題への応用を研究し， 査読付き国際ワークショップで発表を行った． -
先進的な知識表現および推論技術を基盤とした多目的最適化ソルバーの研究開発
研究課題/研究課題番号：18K11242 2018年4月 - 2021年3月
日本学術振興会 学術研究助成基金助成金／基盤研究(C) 基盤研究(C)
番原 睦則, 宋 剛秀, 田村 直之
資金種別：競争的資金
-
ハイブリッド符号化を用いた高性能なSAT型制約プログラミングシステム
研究課題/研究課題番号：16K16036 2016年4月 - 2019年3月
日本学術振興会 学術研究助成基金助成金／若手研究(B) 若手研究(B)
宋 剛秀
担当区分：研究代表者 資金種別：競争的資金
-
SATを基盤とした新しい制約プログラミングシステムの研究開発
研究課題/研究課題番号：16H02803 2016年4月 - 2019年3月
日本学術振興会 科学研究費補助金／基盤研究(B) 基盤研究(B)
田村 直之, 番原 睦則, 宋 剛秀, 井上 克巳, 鍋島 英知
資金種別：競争的資金
-
SAT符号化を用いた制約解集合プログラミングに関する研究開発
研究課題/研究課題番号：15K00099 2015年4月 - 2018年3月
日本学術振興会 学術研究助成基金助成金／基盤研究(C) 基盤研究(C)
番原 睦則, 田村 直之, 宋 剛秀, 井上 克巳
資金種別：競争的資金
-
代謝パスウェイ解析のための制約プログラミングシステムの研究開発
研究課題/研究課題番号：25730042 2013年4月 - 2016年3月
文部科学省 科学研究費補助金(若手研究(B)) 若手研究(B)
宋 剛秀
担当区分：研究代表者 資金種別：競争的資金
配分額：2340000円 （ 直接経費：1800000円 、 間接経費：540000円 ）
近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライ
-
命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現
研究課題/研究課題番号：24300007 2012年4月 - 2015年3月
文部科学省 科学研究費補助金(基盤研究(B)) 基盤研究(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
-
言語工学（-15）
（神戸大学）
-
Theory of Programming Languages
（Kobe University）
-
プログラミング言語特論
（神戸大学）
-
プログラミング言語論及び演習（-15）
（神戸大学）
-
情報基礎
（神戸大学）
-
情報基礎特論
（神戸大学）
-
言語工学
（神戸大学）
-
Advanced Theory of Informatics
（Kobe University）
-
Advanced Course on Programming Languages
（Kobe University）
-
Introduction to Computer Literacy
（Kobe University）
-
Paradigm of Programming Languages and Practice
（Kobe University）