Updated on 2025/10/22
推論技術
国際情報交換
命題論理
動的制約
制約最適化
制約充足
制約プログラミング
充足可能性判定問題
充足可能性判定
フランス
ハミルトン閉路問題
ドメイン特化言語
システム生物学
SAT技術
SAT
Informatics / Intelligent informatics
Informatics / Biological, health, and medical informatics
Informatics / Information theory
Informatics / Software
神戸大学 情報基盤センター 准教授
2019.4
Kobe University Assistant Professor
2012.4
The Graduate University for Advanced Studies School of Multidisciplinary Sciences
- 2011.9
電子情報通信学会
日本ソフトウェア科学会
情報処理学会
人工知能学会
2022 XCSP3 Competition Sequential CSP Solver track 2nd place
2022.8 Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura
2019 XCSP3 Competition Sequential CSP Solver 2nd Place
2019.10 XCSP3 Competition Organization Fun-sCOP
Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura
7th Best Review Paper Award (2018)
2019.8 Japan Society for Software Science and Technology SAT-based Constraint Programming Systems and Related Technologies
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
JSAI Annual Conference Award 2019
2019 The Japanese Society for Artificial Intelligence A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
情報処理学会 2018 年度特選論文
2018.9 情報処理学会 SAT技術を用いたペトリネットのデッドロック検出手法の提案
寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
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型制約ソルバーによるナンバーリンクの解法とその評価
迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
PPL2017発表賞（一般の部）
2017.3 日本ソフトウェア科学会 プログラミング論研究会 SATソルバーの最新動向と利用技術
SOH TAKEHIDE, TAMURA NAOYUKI
第20回研究論文賞
2016.3 日本ソフトウェア科学会 パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳
アルゴリズムデザインコンテスト2015 最優秀賞 (DAシンポジウム2015)
2015.8 情報処理学会 SLDM研究会 iSugar+GlueMiniSat
迫 龍哉, 川原 征大, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE, 鍋島 英知
最優秀賞
2015.8 情報処理学会DAシンポジウム2015 SAT型制約ソルバーを用いたナンバーリンクの求解と解の最適化
迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
第31回大会高橋奨励賞
2014.9 日本ソフトウェア科学会 Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
SOH TAKEHIDE
アルゴリズムデザインコンテスト2014 最優秀賞 (DAシンポジウム2014・SWEST16)
2014.8 情報処理学会 SLDM研究会 Sugar+GlueMiniSat
TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI, 鍋島 英知
アルゴリズムデザインコンテスト2014 最優秀賞
2014.8 情報処理学会DAシンポジウム2014 SAT型制約ソルバーを用いたナンバーリンクの解法
田村直之, 宋剛秀, 番原睦則, 鍋島英知
学長賞
2010.4 総合研究大学院大学 SATとASPを用いた生物学におけるパスウェイの解析
SOH TAKEHIDE
２００９年度全国大会優秀賞
2009.9 人工知能学会 Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
SOH TAKEHIDE
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 Vol. 17 page： 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) page： 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) page： 26 - 15 2024
Hamiltonian Cycle Reconfiguration with Answer Set Programming Reviewed International coauthorship International journal
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 Vol. 14281 page： to appear - 16p. 2023.9
SAT-Based Method for Finding Attractors in Asynchronous Multi-Valued Networks Reviewed
Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
Proceedings of the 16th International Joint Conference on Biomedical Engineering Systems and Technologies page： 163 - 174 2023.3
SAF: SAT-Based Attractor Finder in Asynchronous Automata Networks Reviewed
Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
2023
ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems. Reviewed
Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
CPAIOR page： 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) page： 294 - 302 2023
ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems. Reviewed
Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
CoRR Vol. abs/2207.13959 2022.12
Core Challenge 2022: Solver and Graph Descriptions.
Takehide Soh, Yoshio Okamoto, Takehiro Ito
CoRR Vol. abs/2208.02495 2022.9
チャネリング制約を用いた alldifferent 制約の SAT 符号化 Open Access
小菅脩司, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022.3
解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価 Open Access
桑原和也, 宋剛秀, 田村直之, 番原睦則
情報処理学会第84回全国大会講演論文集 2022.3
有界モデル検査による独立集合遷移問題の解法に関する考察 Open Access
戸田 貴久, 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一
情報処理学会 研究報告アルゴリズム（AL） Vol. 2022-AL-186 ( 5 ) page： 1 - 7 2022.1
Towards CEGAR-based Parallel SAT Solving Reviewed
Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue
Pragmatics of SAT 2021 2021.7
Studies on a Parallelization Method of SAT-based CSP Solvers using CEGAR and the Share of Counterexamples Open Access
Vol. 112 page： 6 - 11 2020.3
Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming Open Access
IINO Naoki, TAMURA Naoyuki, SOH Takehide, BANBARA Mutsunori, INOUE Katsumi
Proceedings of the Annual Conference of JSAI Vol. 2020 ( 0 ) page： 2N5OS17b05 - 2N5OS17b05 2020
alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用 Open Access
大野周亮, 番原睦則, SOH TAKEHIDE, TAMURA NAOYUKI
人工知能学会研究会資料 Vol. SIG-FPAI-B803 page： 6 - 11 2019.3
A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition Open Access
SOH Takehide, BERRE Daniel Le, BANBARA Mutsunori, TAMURA Naoyuki
Proceedings of the Annual Conference of JSAI Vol. 2019 ( 0 ) page： 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) page： 1 - 2 2019
teaspoon : solving the curriculum-based course timetabling problems with answer set programming. Reviewed
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
Annals OR Vol. 275 ( 1 ) page： 3 - 37 2019
Proposal of SAT-based Method to Detect Deadlock of Petri Nets Open Access
寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
情報処理学会論文誌 Vol. 59 ( 9 ) page： 1749 - 1760 2018.9
A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints Reviewed Open Access
南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
コンピュータソフトウェア Vol. 35 ( 3 ) page： 65 - 78 2018.8
Recent Advances in SAT Solvers and their Utilization Technologies. Reviewed Open Access
SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki, NABESHIMA Hidetomo
Computer Software Vol. 35 ( 4 ) page： 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) page： 1 - 2 2018
A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウェア科学会第34回大会講演論文集 Vol. 34 page： 393 - 404 2017.9
Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings Reviewed
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS Vol. 26 ( 1 ) 2017.2
Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー Open Access
SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
第58回プログラミング・シンポジウム予稿集 page： 71 - 74 2017.1
ブール基数制約を経由した擬似ブール制約のSAT符号化法 Open Access
南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
人工知能学会研究会資料 page： 18 - 23 2017.1
SATソルバーの使い方 —問題をSATに符号化する方法— Open Access
TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI
第58回プログラミング・シンポジウム予稿集 page： 165 - 172 2017.1
catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming. Reviewed
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) page： 265 - 278 2017
A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints Open Access
MINAMI Yushi, SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki
JSAI Technical Report, SIG-FPAI Vol. 103 page： 4 - 4 2017
Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation. Reviewed
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Daniel Le Berre
Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017) Vol. 10416 page： 596 - 614 2017
SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案 Open Access
寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウェア科学会第33回大会講演論文集 Vol. 2017 ( 0 ) page： 1M1OS02a2 - 1M1OS02a2 2017
SAT-based Constraint Programming Systems and Related Technologies Reviewed Open Access
SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki
Computer Software Vol. 34 ( 1 ) page： 1_67 - 1_80 2017
制約充足問題のASP符号化に関する一考察 Open Access
坡山 直樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI
2017年度人工知能学会全国大会(第31回)論文集 Vol. 2017 ( 0 ) page： 1M1OS02a4 - 1M1OS02a4 2017
解集合プログラミングによるカリキュラムベース・コース時間割編成 Invited
BANBARA MUTSUNORI, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, SOH TAKEHIDE, TAMURA NAOYUKI, フィリップ ワンコ
第29回RAMPシンポジウム論文集 page： 73 - 88 2017
An incremental SAT solving library and its applications Reviewed Open Access
Tatsuya Sako, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima, Katsumi Inoue
Computer Software Vol. 33 ( 4 ) page： 16 - 29 2016.11
Implementing efficient all solutions SAT solvers Reviewed
Takahisa Toda, Takehide Soh
ACM Journal of Experimental Algorithmics Vol. 21 ( 1 ) page： 1 - 44 2016.10
インクリメンタルSAT解法ライブラリとその応用 Reviewed Open Access
迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知, 井上 克巳
コンピュータソフトウェア Vol. 33 ( 4 ) page： 16 - 29 2016.7
Solving Optimal Software Component Configuration Problem in Cloud Open Access
TAMURA NAOYUKI, 井上 克巳, 鍋島 英知, BANBARA MUTSUNORI, SOH TAKEHIDE
人工知能基本問題研究会(第100回) Vol. 100 page： 19 - 24 2016.3
分子ネットワーク上の状態推定とその可視化による知識発見支援 Open Access
平沼 祐人, 山本 泰生, 守屋 央朗, SOH TAKEHIDE, 岩沼 宏治
第45回バイオ情報学研究発表会 Vol. 11 page： 1 - 6 2016.3
解集合プログラミングを用いた制約組合せテストケース生成 Reviewed
兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, 沖本 天太
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) Vol. カテゴリC1 2016.3
SATソルバーを用いた制約プログラミングシステムとその応用 Open Access
SOH TAKEHIDE
第57回プログラミング・シンポジウム page： 1 - 10 2016.1
SATソルバーを用いた部分グラフ探索のための制約モデル Open Access
川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
2016年度人工知能学会全国大会(第30回)論文集 Vol. 2016 ( 0 ) page： 1D4OS02a4 - 1D4OS02a4 2016
Teaspoon: Solving the curriculum-based course timetabling problems with answer set programming Reviewed
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 page： 13 - 32 2016
SAT型制約ソルバーによるナンバーリンクの解法とその評価 Open Access
迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
2016年度人工知能学会全国大会(第30回)論文集 Vol. 2016 ( 0 ) page： 1D4OS02a3 - 1D4OS02a3 2016
iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー Open Access
迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知, 井上 克巳
日本ソフトウェア科学会第32回大会 page： 1 - 12 2015.9
Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について Open Access
SOH TAKEHIDE, 馬場 知哉
日本ソフトウェア科学会第32回大会 page： 1 - 8 2015.9
SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価 Open Access
川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウェア科学会第32回大会 Vol. 32 page： 1 - 9 2015.9
順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化 Open Access
SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウェア科学会第32回大会 page： 1 - 11 2015.9
制約充足問題のハイブリッド符号化に向けて Open Access
SOH TAKEHIDE, 佐古田 淳史, BANBARA MUTSUNORI, TAMURA NAOYUKI
第第97回人工知能基本問題研究会．人工知能学会研究会資料 page： 65 - 73 2015.3
A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings Reviewed
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015) Vol. 2016-January page： 421 - 428 2015
aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming. Reviewed
Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
CoRR Vol. abs/1312.6113 page： 112 - 126 2015
Implementing Efficient All Solutions SAT Solvers. Reviewed
Takahisa Toda, Takehide Soh
CoRR Vol. abs/1510.00523 2015
組合せテストケース生成問題に対する制約解集合プログラミングの適用 Open Access
兼行 大将, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳
2015年度人工知能学会全国大会 Vol. 2015 ( 0 ) page： 2H5OS03b5 - 2H5OS03b5 2015
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール Open Access
SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウェア科学会第31回大会講演論文集 page： 1 - 15 2014.9
制約解集合プログラミングシステムの設計方式に関する考察 Open Access
SOH TAKEHIDE, 則武 治樹, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
日本ソフトウェア科学会第31回大会講演論文集 page： 1 - 15 2014.9
Solving Numberlink by a SAT-based Constraint Solver Open Access
TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI, 鍋島 英知
DAシンポジウム2014論文集 Vol. 2014 ( 2014 ) page： 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) page： 1 - 12 2014.7
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法 Open Access
佐古田 淳史, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
第28回人工知能学会全国大会論文集 page： 1 - 4 2014.5
Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem Reviewed
Takehide Soh, Daniel Le Berre, Stephanie Roussel, Mutsunori Banbara, Naoyuki Tamura
LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2014 Vol. 8761 page： 684 - 693 2014
SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用 Open Access
SOH TAKEHIDE, Daniel Le Berre, Stéphanie Roussel, BANBARA MUTSUNORI, TAMURA NAOYUKI
第28回人工知能学会全国大会論文集 Vol. 2014 ( 0 ) page： 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 page： 684 - 693 2014
PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding Reviewed
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 Reviewed
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
THEORY AND PRACTICE OF LOGIC PROGRAMMING Vol. 13 ( 4/5 ) page： 783 - 798 2013.7
SAT符号化を用いたパッキング配列の構成 Reviewed
則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集 2013.3
Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems. Reviewed
Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings Vol. 7962 page： 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 Vol. 4(3-4):154-165 2012.12
Encoding Curriculum based Course Timetabling Problems into Pseudo-Boolean Optimization Problems
鈴江 美奈, 田村 直之, 番原 睦則, 宋 剛秀, 鳩野 逸生
日本ソフトウェア科学会第29回大会講演論文集 Vol. 29 page： 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 page： 11 - 19 2012.3
Analyzing pathways using ASP-based approaches Reviewed
Oliver Ray, Takehide Soh, Katsumi Inoue
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 6479 page： 167 - 183 2012
Enumerating minimal active metabolic pathways by model generation Reviewed
Takehide Soh, Katsumi Inoue
Transactions of the Japanese Society for Artificial Intelligence Vol. 27 ( 3 ) page： 204 - 212 2012
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem Reviewed
Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
Fundamenta Informaticae Vol. 102(3-4): 467-487 2010.11
A SAT-based Method for Analyzing Metabolic Pathways Reviewed
Takehide Soh, Katsumi Inoue
Poster presentation at: Systems Biochemistry 2010 2010
Finding Minimal Reaction Sets in Large Metabolic Pathways Reviewed
Takehide Soh, Katsumi Inoue
Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010) page： 54 - 54 2010
(2H3-3)SAT問題への変換を用いたフィードバックを含むパスウェイの解析 Open Access
SOH TAKEHIDE, 井上克巳
人工知能学会全国大会 2009.6
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem Reviewed
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 Reviewed
Katsumi Inoue, Takehide Soh, Seiji Ueda, Yoshito Sasaura, Mutsunori Banbara, Naoyuki Tamura
DISCRETE APPLIED MATHEMATICS Vol. 154 ( 16 ) page： 2291 - 2306 2006.11
Lemma Reusing for SAT based Planning and Scheduling Reviewed 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) page： 103 - 112 2006
Experimental results for solving job-shop scheduling problems with multiple SAT solvers Reviewed
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) Vol. pp.25-38 2005.10
生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般)
SOH TAKEHIDE, 井上克巳
電子情報通信学会技術研究報告. AI, 人工知能と知識処理 Vol. 104 ( 133 ) page： 19 - 24 2004.6
Large Neighborhood Prioritized Search for Combinatorial Optimization with Answer Set Programming International coauthorship International journal
Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
CoRR Vol. abs/2403.07885 page： 11p. 2024.5
ハミルトン閉路問題に対するCut-arc集合制約を用いたSAT型CEGAR解法
大橋瞭雅, 宋剛秀, 鍋島英知, 番原睦則, 井上克巳, 田村直之
日本ソフトウェア科学会大会講演論文集(Web) Vol. 41st 2024
独立集合遷移問題に対する有界組合せ遷移の改良に関する一考察
桑原祥文, 宋剛秀, 盧暁南, 鍋島英知, 番原睦則, 井上克巳, 田村直之
日本ソフトウェア科学会大会講演論文集(Web) Vol. 41st 2024
ZDDを用いた組合せ遷移ソルバー
伊藤健洋, 川原純, 中畑裕, 宋剛秀, 鈴木顕, 照山順一, 戸田貴久
日本オペレーションズ・リサーチ学会秋季研究発表会アブストラクト集 Vol. 2022 2022
CDCL型SATソルバーの内部動作可視化ツール
堀岡真未, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021.9
ライフゲームを逆向きに動かす
足立啓一, 宋剛秀, 田村直之
日本ソフトウェア科学会第38回大会ポスター発表 2021.9
SATソルバーを用いた一層平面配置配線問題の解法に関する考察
三嶋哲平, 宋剛秀, 田村直之
日本ソフトウェア科学会第37回大会ポスター発表 2020.9
Vol. 57 ( 8 ) page： 710 - 715 2016.7
制約充足問題のハイブリッド符号化に向けて
SO TAKEHIDE, SAKODA ATSUSHI, BAMBARA MUTSUNORI, TAMURA NAOYUKI
人工知能学会人工知能基本問題研究会資料 Vol. 97th page： 65 - 73 2015.3
Scala上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
宋剛秀, 馬場知哉
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 32nd page： ROMBUNNO.SOFUTOWEA1 2015
SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
川原征大, 宋剛秀, 番原睦則, 田村直之
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 32nd page： ROMBUNNO.PPL3-1 2015
iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 32nd page： ROMBUNNO.PPL6-1 2015
組合せテストケース生成問題に対する制約解集合プログラミングの適用
KANEYUKI HIROMASA, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI
人工知能学会全国大会論文集(CD-ROM) Vol. 2015 ( 0 ) page： 2H5OS03b5 - 2H5OS03b5 2015
順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
宋剛秀, 番原睦則, 田村直之
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 32nd page： ROMBUNNO.PPL6-3 2015
Prototyping Tool for SAT-based Constraint Programming Systems in Scala
Vol. 31 page： 217 - 231 2014.9
Studies on a Design of Constraint Answer Set Programming Systems
Vol. 31 page： 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 Sci Vol. 8761 page： 684 - 693 2014
制約解集合プログラミングシステムの設計方式に関する考察
SO TAKEHIDE, NORITAKE HARUKI, BAMBARA MUTSUNORI, TAMURA NAOYUKI, INOUE KATSUMI
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 31st page： ROMBUNNO.PPL2-3 2014
Constraint Modeling and SAT Encoding of the Packing Array Problem
NORITAKE HARUKI, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI
コンピュータソフトウェア Vol. 31 ( 1 ) page： 116 - 130 2014
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 31st page： ROMBUNNO.SOFUTO1-1 2014
SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用
SO TAKEHIDE, LE BERRE DANIEL, ROUSSEL STEPHANIE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
人工知能学会全国大会論文集(CD-ROM) Vol. 2014 ( 0 ) page： 1D5OS11b6i - 1D5OS11b6i 2014
Solving Post-Enrollment Course Timetabling using Cardinality Constraint and SAT Solvers
佐古田 淳史, 宋 剛秀, 番原 睦則
人工知能学会全国大会論文集 Vol. 28 page： 1 - 4 2014
登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
SAKODA ATSUSHI, SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
人工知能学会全国大会論文集(CD-ROM) Vol. 28th page： ROMBUNNO.1D5-OS-11B-7 2014
Scarab : A Prototyping Tool for SAT-based Constraint Programming Systems in Scala
Vol. 30 page： 237 - 245 2013.9
Constraint Modeling and SAT Encoding of the Packing Array Problem
Vol. 30 page： 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 Program Vol. 13 ( 4/5 ) page： 783 - 798 2013.7
BANBARA Mutsunori, SOH Takehide, TAMURA Naoyuki, INOUE Katsumi, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
人工知能学会誌 Vol. 28 ( 2 ) page： 343 - 348 2013.3
BANBARA Mutsunori, SOH Takehide, TAMURA Naoyuki, INOUE Katsumi, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
Journal of Japanese Society for Artificial Intelligence Vol. 28 ( 2 ) page： 343 - 348 2013.3
Report of 2012 FLOPS International Symposium
TAMURA Naoyuki, BANBARA Mutsunori, HIRAYAMA Katsutoshi, SOH Takehide
Computer Software Vol. 30 ( 1 ) page： 16 - 19 2013.1
正方形詰込み問題の制約モデルとSAT符号化を用いた解法
SAKODA ATSUSHI, SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
人工知能学会全国大会論文集(CD-ROM) Vol. 2013 ( 0 ) page： 2E5OS09b1 - 2E5OS09b1 2013
パッキング配列問題の制約モデリングとSAT符号化
NORITAKE HARUKI, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 30th page： 79 - 92 2013
Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI, LE BERRE DANIEL, ROUSSEL STEPHANIE
日本ソフトウエア科学会大会講演論文集(CD-ROM) Vol. 30th page： 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) Vol. 2011 ( 5 ) page： 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)
宋 剛秀
Journal of Japanese Society for Artificial Intelligence Vol. 27 ( 1 ) page： 84 - 84 2012.1
Principles of Modern SAT Solvers(<Special Issue>Recent Advances in SAT Techniques)
Nabeshima Hidetomo, Soh Takehide
Journal of Japanese Society for Artificial Intelligence Vol. 25 ( 1 ) page： 68 - 76 2010.1
Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation Reviewed
Takehide Soh, Katsumi Inoue
The Sixth Conference on Prestigious Applications of Intelligent Systems (PAIS 2010) Vol. 215 page： 277 - 282 2010
Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
宋 剛秀, 井上 克巳
人工知能学会全国大会論文集 Vol. 24 page： 1 - 4 2010
高速SATソルバーの原理 Reviewed
鍋島英知, SOH TAKEHIDE
人工知能学会論文誌(解説論文) Vol. 25 ( 1 ) page： 68 - 76 2010
Analyzing Pathways through a Translation into SAT Problems
宋 剛秀, 井上 克巳
論文集 Vol. 23 page： 1 - 4 2009
A SAT-based Method for Solving the Two-dimensional Strip Packing Problem Reviewed
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 page： 97 - 102 2007
ショップ・スケジューリング問題のSAT変換による解法
田村 直之, 多賀 明子, 番原 睦則, 宋 剛秀, 鍋島 英知, 井上 克巳
スケジューリング・シンポジウム2007講演論文集 page： 97 - 102 2007
Effective SAT Planning and SAT Scheduling by Lemma Reusing
NABESHIMA Hidetomo, SOH Takehide, INOUE Katsumi, IWANUMA Koji
電子情報通信学会技術研究報告 Vol. 106 ( 38(AI2006 1-11) ) page： 19 - 24 2006.5
Effective SAT Planning and SAT Scheduling by Lemma Reusing
NABESHIMA Hidetomo, SOH Takehide, INOUE Katsumi, IWANUMA Koji
IEICE technical report Vol. 106 ( 38 ) page： 19 - 24 2006.5
効率的なSATプランニングとSATスケジューリングのための補題利用 (in English)
鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
信学技報, AI2006-4 page： 19 - 24 2006
Experimental Results for Solving Job-shop Scheduling Problems with Multiple SAT Solvers Reviewed
Takehide Soh, Katsumi Inoue, Mutsunori Banbara, Naoyuki Tamura
In the Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing page： 25 - 38 2005.10
A-7-4 Parallel Implementation of the Block Lanczos Algorithm on the Dual-CPU Workstation
Soh Takehide, Kuwakado Hidenori, Morii Masakatu, Tanaka Hatsukazu
Proceedings of the Society Conference of IEICE Vol. 2005 page： 177 - 177 2005.9
Solving Job-shop Scheduling Problems with Multiple SAT Solvers
SOH Takehide, INOUE Katumi
IEICE technical report. Artificial intelligence and knowledge-based processing Vol. 104 ( 133 ) page： 19 - 24 2004.6
The characteristics of Japanese Vowel using frequency analysis
Nishida Shigeki, Soh Takehide, Mashima Ryou
Research reports of Nara Technical College ( 38 ) page： 29 - 34 2002
解集合プログラミングを用いた多層ナンバーリンクの解法
坡山 直樹, 川原 征大, 迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017.3 日本ソフトウェア科学会 プログラミング論研究会
解集合ソルバーを用いた様相命題論理の充足可能性判定
Naoki Iino, Naoyuki Tamura, Takehide Soh, Banbara Mutsunori, Katsumi Inoue
The 22th Workshop on Programming and Programming Languages (PPL 2020) 2020
正規制約のSAT符号化とその性能評価
生田 哲也, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE
日本ソフトウェア科学会第35回大会 2018.8
正規制約に対するSAT符号化手法の提案と評価
Tetsuya Ikuta, Naoyuki Tamura, Takehide Soh, Mutsunori Banbara
The 22th Workshop on Programming and Programming Languages (PPL 2020) 2020
正方形詰込み問題の制約モデルとSAT符号化を用いた解法
佐古田 淳史, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
2013年度人工知能学会全国大会 2013.6 人工知能学会
パッキング配列問題の制約モデリングとSAT符号化
則武 治樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳
日本ソフトウェア科学会第30回大会 2013.9 日本ソフトウェア科学会
インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー
迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 2016.3 日本ソフトウェア科学会プログラミング論研究会
Towards Incremental SAT-based CSP Solving: Experimental Results for the Hamiltonian Cycle Problem International conference
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 International conference
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 International conference
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のトレースツール
吉玉 元和, 寸田 智也, 南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017.3 日本ソフトウェア科学会 プログラミング論研究会
Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015) 2015.3 日本ソフトウェア科学会プログラミング論研究会
Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール
宋 剛秀, 田村 直之, 番原 睦則
第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 2013.3 日本ソフトウェア科学会
Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について
SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, Daniel Le Berre, Stéphanie Roussel
日本ソフトウェア科学会第30回大会 2013.9 日本ソフトウェア科学会
SAT型制約ソルバーを用いた多層ナンバーリンクの解法
寸田 智也, 南 雄之, 吉玉 元和, SOH TAKEHIDE
DAシンポジウム2016 2016.9 情報処理学会 システムとLSIの設計技術研究会（SLDM）
SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
寸田 智也, 南 雄之, 宋 剛秀, 田村 直之
DAシンポジウム2017 2017.8 情報処理学会システムとLSIの設計技術研究会
SATソルバーを用いた様相命題論理S4の充足可能性判定
飯野 有軌, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE
日本ソフトウェア科学会第35回大会 2018.8
SATソルバーの最新動向と利用技術
SOH TAKEHIDE, TAMURA NAOYUKI
第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017) 2017.3 日本ソフトウェア科学会 プログラミング論研究会
SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー) Invited
SOH TAKEHIDE
人工知能学会 第9回AIツール入門講座 2015.12 人工知能学会
PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding International conference
Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
The 4th International Workshop on Pragmatics of SAT 2013.7 PoS
CSPSAT Projects and their SAT Related Tools International conference
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 日本ソフトウェア科学会プログラミング論研究会
Speeding-up SAT-based Constraint Optimization Solvers
Grant number：23K11047 2023.4 - 2027.3
Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)
Research and Development of a New SAT Solving Technologies for Constraint Satisfaction Problems
Grant number：22K11973 2022.4 - 2025.3
Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)
Research and Development on SAT-based Integration of Systematic and Stochastic Search
Grant number：21K11828 2021.4 - 2024.3
Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)
Engineering Approach for Expanding Combinatorial Reconfiguration: Toward a General-Purpose Solver Using Power Distribution Systems as a Steppingstone
Grant number：20H05794 2020.10 - 2023.3
Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research Grant-in-Aid for Transformative Research Areas (B)
Acceleration of SAT-based CSP Solvers using MDD
Grant number：20K11748 2020.4 - 2023.3
Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (C)
先進的な知識表現および推論技術を基盤とした多目的最適化ソルバーの研究開発
2018.4 - 2021.3
学術研究助成基金助成金／基盤研究(C)
番原 睦則
Grant type：Competitive
SATを基盤とした新しい制約プログラミングシステムの研究開発
2016.4 - 2019.3
科学研究費補助金／基盤研究(B)
田村 直之
Grant type：Competitive
ハイブリッド符号化を用いた高性能なSAT型制約プログラミングシステム
2016.4 - 2019.3
学術研究助成基金助成金／若手研究(B)
宋 剛秀
Authorship：Principal investigator Grant type：Competitive
SAT符号化を用いた制約解集合プログラミングに関する研究開発
2015.4 - 2018.3
学術研究助成基金助成金／基盤研究(C)
番原 睦則
Grant type：Competitive
代謝パスウェイ解析のための制約プログラミングシステムの研究開発
2013 - 2015
文部科学省 科学研究費補助金(若手研究(B))
宋 剛秀
Authorship：Principal investigator Grant type：Competitive
Grant amount：\2340000 （ Direct Cost: \1800000 、 Indirect Cost：\540000 ）
近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライ
命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現
2012 - 2014
文部科学省 科学研究費補助金(基盤研究(B))
田村 直之
Grant type：Competitive
当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進めた．「A. フレキシブル制約に関する研究開発」については，フレキシブル制約のSAT符号化で重要になる擬似ブール制約の符号化方法の研究，PBSugarシステムの開発，および論文発表を行った．「B. 動的な制約変更に関する研究開発」については，動的な制約変更が可能なScarabシステムの開発および論文発表を行った．「C. ドメイン拡張に関する研究開発」については，記号推論が可能な解集合プログラミングシステム上で整数上の制約記述を可能にするプロトタイプシステムを開発し，性能評価を行った．「D. 応用研究開発」については，各種問題の評価を進めた．特に，時間割問題について優れた結果を得，論文発表を行った．また，「論理と推論の理論，実装，応用に関する合同セミナー」のERATO
SAT変換を用いた制約充足問題の解法とシステム生物学への応用
Grant number：10J02321 2010 - 2011
日本学術振興会 科学研究費助成事業 特別研究員奨励費
宋 剛秀
最終年度の報告として、これまでの研究成果について以下にまとめる。
本研究では化学反応法則を満たしつつ入力代謝物集合から出力代謝物集合を生成可能なパスウェイを活性パスウェイ呼び、特にその包含関係において極小なものを極小活性パスウェイと呼ぶ。研究ではまず極小活性パスウェイを列挙する問題を極小活性パスウェイ同定問題として定義を行った。代謝パスウェイの解析を行う際には既存のデータから問題を構築する必要がある。そこで更新頻度において優れていることから、生物学的知識のデータベースEcoCyc(http://ecocyc.org/)から問題を構成して評価を行った。このデータから構成した問題をSAT技術によって解くために本研究では次の枠組みを用いた:(1)まず問題を命題論理式に符号化する、(2)SATソルバを漸増的に適用するインクリメンタルSAT解法を用いて符号化された命題論理式から極小モデルを計算する、(3)得られた極小モデルを逆符号化することで問題の解である極小活性パスウェイを得る。
提案した問題および解法の評価のためにEcoCycのデータから極小活性パスウェイ同定問題を構成し、SAT技術を用いて解を求めた。結果として9個の極小活性パスウェイを同定し、その中の2個が生物学における既存の知識と一致したパスウェイ(参照パスウェイ)であることを確認している。また専門家との議論で提案された制約を命題論理式に追加することでより精緻なパスウェイを計算することに成功した。この成果は国内雑誌論文として発表を行った。また代謝パスウェイに対する解集合プログラミングを用いた解析研究についても国際会議の会議録で発表を行った。
さらにより具体的な生物学の問題に適用するために、大腸菌における単一遺伝子ノックアウトの影響予測を極小活性パスウェイの同定によって行う手法の研究を国立遺伝学研究所の研究チームと共同して進めた。大腸菌の解糖系に対して計算機実験を行った結果,提案手法の予測が生物実験の結果とよく一致することを確認した。この成果は国際会議において発表を行った。
Advanced Course on Programming Languages
（Kobe University）
言語工学（-15）
（Kobe University）
言語工学
（Kobe University）
情報基礎特論
（Kobe University）
情報基礎
（Kobe University）
プログラミング言語論及び演習（-15）
（Kobe University）
プログラミング言語特論
（Kobe University）
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）
