@Helsinki

SOH, Takehide
宋 剛秀

English Page | Japanese Page
Tamura Lab | CSPSAT | Scarab

1 プロフィールページ

2 学術論文誌 (査読あり)

  1. ブール基数制約を経由した擬似ブール制約のSAT符号化手法
  2. SAT技術を用いたペトリネットのデッドロック検出手法の提案 情報処理学会 2018年度特選論文
  3. 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 of Operations Research, in print, 2018.
    • (DOI) https://doi.org/10.1007/s10479-018-2757-7
  4. Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
  5. Implementing Efficient All Solutions SAT Solvers.
  6. インクリメンタルSAT解法ライブラリとその応用.
  7. パッキング配列問題の制約モデリングとSAT符号化. 第20回研究論文賞(2015年度)
  8. Answer Set Programming as a Modeling Language for Course Timetabling
    • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue and Torsten Schaub
    • Theory and Practice of Logic Programming (TPLP), 13(4-5):783-798, Cambridge Journals, 2013.
    • (DOI) https://doi.org/10.1017/S1471068413000495
  9. モデル生成を用いた代謝ネットワークにおける極小活性パスウェイの列挙
  10. A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
  11. A Competitive and Cooperative Approach to Propositional Satisfiability

3 国際会議のプロシーディングス (査読あり)

  1. 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.
    • (DOI) https://doi.org/10.1007/978-3-319-66158-2_38
  2. 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
    • Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2017), LNAI, Vol.10377, pp.265--278, Springer
    • (DOI) https://doi.org/10.1007/978-3-319-61660-5_24
  3. 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
    • Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling (PATAT 2016), pp.13-32, 2016.
    • (DOI) https://doi.org/10.1007/s10479-018-2757-7
  4. A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
  5. 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, and Matthias Weise.
    • In: Francesco Calimeri, Giovambattista Ianni, and Miroslaw Truszczynski (eds.),
    • Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015),
    • Lecture Notes in Artificial Intelligence, Vol.9345, pp.112-126, Springer, 2015.
    • (DOI) https://doi.org/10.1007/978-3-319-23264-5_10
  6. Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem.
  7. PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding.
  8. Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (Tool Paper)
  9. Analyzing Pathways using ASP-based Approaches
  10. Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation
  11. Lemma Reusing for SAT based Planning and Scheduling

4 国際ワークショップのプロシーディングス (査読あり)

  1. Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming
  2. Finding Minimal Reaction Sets in Large Metabolic Pathways
  3. 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, No.16 (15 pages), CEUR Workshop Proceedings (CEUR-WS.org), Vol.451, 2008.
    • (URL) http://ceur-ws.org/Vol-451/
    • (CEUR-WS) http://ceur-ws.org/Vol-451/paper16soh.pdf
  4. Experimental Results for Solving Job-shop Scheduling Problems with Multiple SAT Solvers
    • Takehide Soh, Katsumi Inoue, Mutsunori Banbara, and Naoyuki Tamura
    • In the Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing (held in conjunction with CP 2005), pages 25-38, Sitges Spain, October 1st 2005.

5 解説論文

  1. SATソルバーの最新動向と利用技術
  2. SAT型制約プログラミングシステムと周辺技術.
  3. SATとパズル 〜パズルからプログラム検証まで〜
  4. 高速SATソルバーの原理

6 システム記述

  1. sCOP: SAT-based Constraint Programming System.

7 その他上記に含まれない論文

  1. 解集合プログラミングによるカリキュラムベース・コース時間割編成.
    • 番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
    • 第29回RAMPシンポジウム論文集, pp.73--88, 日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017.
  2. ブール基数制約を経由した擬似ブール制約のSAT符号化法
    • 南雄之, 宋剛秀, 番原睦則, 田村直之.
    • 人工知能基本問題研究会(第103回), 人工知能学会研究会資料 SIG-FPAI-B506-04, pp.18-23, 人工知能学会, 2017.
  3. SAT技術を用いたペトリネットのデッドロック検出手法の提案
    • 寸田智也, 宋剛秀, 番原睦則, 田村直之
    • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-2, 2017.
  4. 制約充足問題のASP符号化に関する一考察
    • 坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-4, 2017.
  5. SATソルバーの使い方 〜問題をSATに符号化する方法〜
    • 田村直之, 宋剛秀, 番原睦則.
    • 第58回プログラミング・シンポジウム予稿集, pp.165--172, 情報処理学会, 2017.
  6. Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー
    • 宋剛秀, 番原睦則, 田村直之.
    • 第58回プログラミング・シンポジウム予稿集, pp.71--74, 情報処理学会, 2017.
  7. SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案.
    • 寸田智也, 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第33回大会講演論文集, PPL9-2, 日本ソフトウェア科学会, 2016.
  8. SAT型制約ソルバーによるナンバーリンクの解法とその評価. 全国大会優秀賞受賞
    • 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
    • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-3, 人工知能学会, 2016.
  9. SATソルバーを用いた部分グラフ探索のための制約モデル.
    • 川原征大, 宋剛秀, 番原睦則, 田村直之.
    • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-4, 人工知能学会, 2016.
  10. クラウド上のソフトウェア要素最適配置問題の解法.
    • 田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀.
    • 人工知能基本問題研究会(第100回), 人工知能学会研究会資料 SIG-FPAI-B503, pp.19-24, 人工知能学会, 2016.
  11. 分子ネットワーク上の状態推定とその可視化による知識発見支援.
    • 平沼祐人, 山本泰生, 守屋央朗, 宋剛秀, 岩沼宏治.
    • 第45回バイオ情報学研究発表会, 研究報告バイオ情報学 (BIO), 2016-BIO-45, Vol. 11, pp. 1--6, 2016.
  12. 解集合プログラミングを用いた制約組合せテストケース生成.
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太.
    • 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 論文集, カテゴリC1, 2016.
  13. SATソルバーを用いた制約プログラミングシステムとその応用.
    • 宋剛秀.
    • 第57回プログラミング・シンポジウム, 第57回プログラミング・シンポジウム予稿集, 10ページ, 2016.
  14. Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について.
    • 宋剛秀, 馬場知哉.
    • 日本ソフトウェア科学会第32回大会講演論文集, ソフトウェア-1, 日本ソフトウェア科学会, 2015.
  15. SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価. 学生奨励賞受賞
    • 川原征大, 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL3-1, 日本ソフトウェア科学会, 2015.
  16. iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー.
    • 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-1, 日本ソフトウェア科学会, 2015.
  17. 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化.
    • 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-3, 日本ソフトウェア科学会, 2015.
  18. 組合せテストケース生成問題に対する制約解集合プログラミングの適用. 全国大会優秀賞受賞
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
    • 2015年度人工知能学会全国大会(第29回)論文集, 2H5-OS-03b-5, 人工知能学会, 2015.
  19. 制約充足問題のハイブリッド符号化にむけて.
    • 宋剛秀, 番原睦則, 田村直之.
    • 第97回人工知能基本問題研究会(SIG-FPAI), 人工知能学会研究会資料, SIG-FPAI-B404-12, pp. 65-73, 2015.
  20. Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール. 高橋奨励賞受賞
    • 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第31回大会講演論文集, ソフト1-1, 日本ソフトウェア科学会, 2014.
  21. 制約解集合プログラミングシステムの設計方式に関する考察.
    • 宋剛秀, 則武治樹, 番原睦則, 田村直之, 井上克巳.
    • 日本ソフトウェア科学会第31回大会講演論文集, PPL2-3, 日本ソフトウェア科学会, 2014.
  22. SAT型制約ソルバーを用いたナンバーリンクの解法. SLDM優秀論文賞受賞
    • 田村直之, 宋剛秀, 番原睦則, 鍋島英知.
    • DAシンポジウム2014論文集, DA2014-7B-2, pp.215-220, 情報処理学会システムとLSIの設計技術研究会, 2014.
  23. 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法.
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
    • 2014年度人工知能学会全国大会(第28回)論文集, 1D5-OS-11b-7, 人工知能学会, 2014.
  24. SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用
    • 宋剛秀, Daniel Le Berre, Stéphanie Roussel, 番原睦則,田村直之
    • 2014年度人工知能学会全国大会(第28回)論文集, 1D5-OS-11b-6in, 人工知能学会, 2014.
  25. パッキング配列問題の制約モデリングとSAT符号化
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
    • 日本ソフトウェア科学会第30回大会講演論文集, PPL1-1, 日本ソフトウェア科学会, 2013.
  26. Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について.
    • 宋剛秀, 番原睦則, 田村直之, Daniel Le Berre, Stéphanie Roussel.
    • 日本ソフトウェア科学会第30回大会講演論文集, PPL2-5, 日本ソフトウェア科学会, 2013.
  27. 正方形詰込み問題の制約モデルとSAT符号化を用いた解法
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
    • 2013年度人工知能学会全国大会(第27回)論文集, 2E5-OS-09b-1, 人工知能学会, 2013.
  28. Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration
    • Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada, and Toshihiko Shiroishi
    • International Journal On Advances in Life Sciences, 4(3-4):154-165, 2012.
  29. Predicting Gene Knockout Effects by Minimal Pathway Enumeration
    • Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada and Toshihiko Shiroishi
    • The 4th International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies (BIOTECHNO 2012), pp.11-19, 2012.
  30. Predicting Gene Knockout Effects on E. coli by Minimal Active Pathway Enumeration
    • Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada and Toshihiko Shiroishi
    • IPSJ SIG Technical Report, Vol.2012-ICS-165, No.7, pages 1-6, 2012.
  31. モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定 全国大会優秀賞受賞
    • 宋剛秀, 井上克巳
    • 人工知能学会第24回全国大会 (JSAI 2010), 人工知能学会, 2010.
  32. SAT問題への変換を用いたフィードバックを含むパスウェイの解析
    • 宋剛秀, 井上克巳
    • 人工知能学会第23回全国大会 (JSAI 2009), 人工知能学会, 2009.
  33. ショップ・スケジューリング問題のSAT変換による解法
    • 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知,
    • スケジューリング・シンポジウム2007, pages 97-102, スケジューリング学会, 2007.
  34. 効率的なSAT プランニングとSAT スケジューリングのための補題再利用
    • 鍋島英知, 宋剛秀, 井上克巳, 岩沼宏治
    • 電子情報通信学会技術研究報告, 106(38): 19-24, 信学技報, 2006.
  35. 行列分割を用いたBlock Lanczos 法の改良
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
    • 暗号と情報セキュリティシンポジウム予稿集, pages 40, 信学会情報セキュリティ研究専門委員会, 2006.
  36. Dual-CPU 上におけるBlock Lanczos 法の並列実装
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
    • 信学会ソサエティ大会, A-7-4, 電子情報通信学会, 2005.
  37. 複数のSATソルバを用いたジョブショップスケジューリング問題の解法
    • 宋剛秀, 井上克巳
    • 信学技報, 104(133): 19-24, 電子情報通信学会技術研究報告, 2004.

8 その他の記事・著作物

  1. OS-2「SAT 技術の理論, 実装, 応用」
    • 波多野大輔, 戸田貴久, 宋剛秀
    • 人工知能学会誌, 31(6):879, 2016
  2. OS-3「SAT 技術の理論, 実装, 応用」
    • 戸田貴久, 波多野大輔, 宋剛秀
    • 人工知能学会誌, 30(6):773, 2015
  3. OS-11「SAT 技術の理論, 実装, 応用」
    • 宋剛秀, 鍋島英知, 越村三幸
    • 人工知能学会誌, 29(6):641, 2014
  4. OS-09「SAT 技術の理論, 実装, 応用」
    • 越村三幸, 鍋島英知, 宋剛秀
    • 人工知能学会誌, 28(6):942, 2013
  5. 国際シンポジウムFLOPS 2012開催報告
    • 田村直之,番原睦則,平山勝敏,宋剛秀
    • コンピュータソフトウェア 30(1):16-19, 2013
  6. 私のブックマーク:SAT ソルバー
    • 番原睦則,宋剛秀,田村直之,井上克巳
    • 人工知能学会誌,28(2):343-348,2013年3月.

9 招待講演

  1. SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー).
    • 宋剛秀.
    • 第9回AIツール入門講座, 国立情報学研究所, 19階会議室1901,1902,1903, 2015年12月14日

10 口頭発表・ポスター発表 (予稿が無いもの)

  1. 正規制約のSAT符号化とその性能評価.
    • 生田哲也, 田村直之, 番原睦則, 宋剛秀
    • 日本ソフトウェア科学会第35回大会, デモ・ポスター発表, 2018
  2. SATソルバーを用いた様相命題論理S4の充足可能性判定.
    • 飯野有軌, 田村直之, 番原睦則, 宋剛秀
    • 日本ソフトウェア科学会第35回大会, デモ・ポスター発表, 2018
  3. 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, and Philipp Wanko
    • The 28th International Conference on Automated Planning and Scheduling, (ICAPS 2018), Delft, The Netherlands, June 27, 2018
  4. SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
    • 寸田智也, 南雄之, 宋剛秀, 田村直之
    • DAシンポジウム2017, ADC-2, 情報処理学会システムとLSIの設計技術研究会, 2017
  5. SATソルバーの最新動向と利用技術. PPL2017発表賞(一般の部)受賞
    • 宋剛秀, 田村直之.
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), サーベイ・チュートリアル発表, 2017.
  6. SugarTracer: SAT型制約ソルバーSugarのトレースツール.
    • 吉玉元和, 寸田智也, 南雄之, 宋剛秀, 番原睦則, 田村 直之.
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), ポスター発表, 2017.
  7. 解集合プログラミングを用いた多層ナンバーリンクの解法.
    • 坡山直樹, 川原征大, 迫龍哉, 宋剛秀, 番原睦則, 田村直之
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), ポスター発表, 2017.
  8. SAT型制約ソルバーを用いた多層ナンバーリンクの解法.
    • 寸田智也, 南雄之, 吉玉元和, 宋剛秀.
    • DAシンポジウム2016, 情報処理学会 システムとLSIの設計技術研究会(SLDM), 2016
  9. インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー.
    • 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
    • プログラミング言語ワークショップ (PPL 2016), ポスター発表, 2016.
  10. SAT型制約ソルバーによるナンバーリンクの求解と解の最適化.
    • 迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知.
    • DAシンポジウム2015, ADC-2, 情報処理学会システムとLSIの設計技術研究会, 2015
  11. Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
    • 宋剛秀, 番原睦則, 田村直之
    • 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015), 日本ソフトウェア科学会, 2015
  12. Answer Set Programming as a Modeling Language for Course Timetabling
    • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
    • 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014), 日本ソフトウェア科学会, 2014
  13. 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
    • The 5th International Workshop on Pragmatics of SAT (PoS 2014), Vienna, 2014
  14. PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding
    • Naoyuki Tamura, Mutsunori Banbara and Takehide Soh
    • In the Proceedings of Pragmatics of SAT 2013 (PoS-13), 14 pages, July 2013.
  15. System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems
    • Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stéphanie Roussel
    • In the Proceedings of Pragmatics of SAT 2013 (PoS-13), 14 pages, July 2013.
  16. 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
  17. Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール.
    • 宋剛秀, 田村直之, 番原睦則
    • 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013), 日本ソフトウェア科学会, 2013
  18. Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation
    • Takehide Soh and Katsumi Inoue
    • JFLI Workshop in Paris, Université Pierre et Marie Curie, Paris, 2010.
  19. A SAT-based Method for Analyzing Metabolic Pathways
    • Takehide Soh and Katsumi Inoue
    • Poster presentation at: Systems Biochemistry 2010, University of York, 2010.
  20. An Implementation of Model-based Abduction and its Application to Systems Biology
    • Takehide Soh and Katsumi Inoue
    • The 3rd Franco-Japanese Symposium on Knowledge Discovery in Systems Biology (FJ'09), Bastia, France, 2009.
  21. A SAT-based Approach for Analyzing Biochemical Pathways
    • Takehide Soh and Katsumi Inoue
    • The 2nd Franco-Japanese Symposium on Knowledge Discovery in Systems Biology (FJ'08), Takayama, Japan, 2008.

Author: Takehide Soh

Created: 2018-12-16 日 19:24

Validate