SOH, Takehide
宋 剛秀

1 プロフィールページ

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

1. ブール基数制約を経由した擬似ブール制約のSAT符号化手法
   
   • 南雄之, 宋剛秀, 番原睦則, 田村直之.
     
   • コンピュータソフトウェア, 35(3): 65-78, 2018.
     
   • (DOI) https://doi.org/10.11309/jssst.35.3_65
     
2. SAT技術を用いたペトリネットのデッドロック検出手法の提案 情報処理学会 2018年度特選論文
   
   • 寸田智也, 宋剛秀, 番原睦則, 田村直之, 井上 克巳.
     
   • 情報処理学会論文誌, 59(9): 1749--1760, 2018.
     
   • (URL) http://id.nii.ac.jp/1001/00191384/
     
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
   
   • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • International Journal on Artificial Intelligence Tools, 26(1):1-29 , World Scientific Publishing, 2017.
     
   • (DOI) https://doi.org/10.1142/S0218213017600053
     
5. Implementing Efficient All Solutions SAT Solvers.
   
   • Takahisa Toda, Takehide Soh
     
   • Journal of Experimental Algorithmics, 21(1): Article 1.12 (44 pages), ACM, 2016.
     
   • (DOI) https://doi.org/10.1145/2975585
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2975585hh
     
6. インクリメンタルSAT解法ライブラリとその応用.
   
   • 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳.
     
   • コンピュータソフトウェア, 33(4):16-29, 2016.
     
   • (DOI) https://doi.org/10.11309/jssst.33.4_16
     
7. パッキング配列問題の制約モデリングとSAT符号化. 第20回研究論文賞（2015年度）
   
   • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
     
   • コンピュータソフトウェア, 31(1): 116-130, 2014.
     
   • (DOI) https://doi.org/10.11309/jssst.31.1_116
     
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. モデル生成を用いた代謝ネットワークにおける極小活性パスウェイの列挙
   
   • 宋剛秀, 井上克巳
     
   • 人工知能学会論文誌, 27(3):204-212, 2012.
     
   • (DOI) https://doi.org/10.1527/tjsai.27.204
     
10. 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, IOS Press, 2010.
      
    • (DOI) https://doi.org/10.3233/FI-2010-314
      
    • (ACM DL) https://dl.acm.org/citation.cfm?id=1890516
      
11. A Competitive and Cooperative Approach to Propositional Satisfiability
    
    • Katsumi Inoue, Takehide Soh, Seiji Ueda, Yoshito Sasaura, Mutsunori Banbara and Naoyuki Tamura
      
    • Discrete Applied Mathematics, 154(16):2291-2306, Elsevier, 2006.
      
    • (DOI) https://doi.org/10.1016/j.dam.2006.04.015
      
    • (ACM DL) https://dl.acm.org/citation.cfm?id=1225862
      

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
   
   • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
     
   • Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), pp.421--428, IEEE Computer Society, 2015.
     
   • (DOI) https://doi.org/10.1109/ICTAI.2015.70
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2922011
     
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.
   
   • Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara and Naoyuki Tamura.
     
   • In: Eduardo Fermé and Joäo Leite (eds.), Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014),
     
   • Lecture Notes in Artificial Intelligence, Vol.8761, pp.684-693, Springer, 2014.
     
   • (DOI) https://doi.org/10.1007/978-3-319-11558-0_52
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2735008
     
7. PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding.
   
   • Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh.
     
   • Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013), pp. 1020-1027, IEEE Computer Society, 2013. DOI 10.1109/ICTAI.2013.153
     
   • (DOI) https://doi.org/10.1109/ICTAI.2013.153
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2572806
     
8. Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (Tool Paper)
   
   • Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
     
   • In the Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), LNCS 7962, pp. 429-436, 2013.
     
   • (DOI) https://doi.org/10.1007/978-3-642-39071-5_34
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2525760
     
9. Analyzing Pathways using ASP-based Approaches
   
   • Oliver Ray, Takehide Soh, and Katsumi Inoue
     
   • Proceedings of the 4th International Conference on Algebraic and Numeric Biology (ANB'10), LNCS, Vol. 6479, pp.167-183, Springer, 2012.
     
   • (DOI) https://doi.org/10.3233/AIC-2010-0465
     
   • (ACM DL) https://dl.acm.org/citation.cfm?id=2187435
     
10. Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation
    
    • Takehide Soh and Katsumi Inoue
      
    • In the Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010), pp.277-282, IOS Press, 2010.
      
    • (DOI) https://doi.org/10.3233/978-1-60750-606-5-277
      
    • (ACM DL) https://dl.acm.org/citation.cfm?id=1861023
      
11. Lemma Reusing for SAT based Planning and Scheduling
    
    • Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, and Koji Iwanuma
      
    • In the proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006), pages 103-112, AAAI Press, 2006.
      
    • (DOI) http://www.aaai.org/Library/ICAPS/2006/icaps06-011.php
      
    • (ACM DL) https://dl.acm.org/citation.cfm?id=3037118
      

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

1. Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming
   
   • Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Torsten Schaub, Takehide Soh, Naoyuki Tamura and Matthias Weise
     
   • In the Proceedings of Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP), Istanbul, August 2013.
     
   • (URL) http://www.kr.tuwien.ac.at/events/aspocp2013/prog.html
     
   • (arXiv) https://arxiv.org/abs/1312.6113
     
2. Finding Minimal Reaction Sets in Large Metabolic Pathways
   
   • Takehide Soh and Katsumi Inoue
     
   • In the Proceedings of the Workshop on Constraint Based Methods for Bioinformatics (WCB 2010), pp.54-68, Edinburgh, 2010.
     
   • (URL) http://wcb10.dimi.uniud.it/
     
   • (DOI) https://doi.org/10.29007/xp2k
     
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.
     
     • A description of this workshop can be found in the front matter of CP 2005 proceeding.
       • https://link.springer.com/content/pdf/bfm:978-3-540-32050-0/1.pdf
     • (PDF)

5 解説論文

1. SATソルバーの最新動向と利用技術
   
   • 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
     
   • コンピュータソフトウェア, 35(4):72--92, 2018.
     
   • (DOI) https://doi.org/10.11309/jssst.35.4_72
     
2. SAT型制約プログラミングシステムと周辺技術.
   
   • 宋剛秀, 番原睦則, 田村直之.
     
   • コンピュータソフトウェア, 34(1):67-80, 2017.
     
   • (DOI) https://doi.org/10.11309/jssst.34.1_67
     
3. SATとパズル 〜パズルからプログラム検証まで〜
   
   • 田村直之, 宋剛秀, 番原睦則.
     
   • 情報処理, 57(8): 710-715, 2016.
     
   • (URL) http://id.nii.ac.jp/1001/00169409/
     
4. 高速SATソルバーの原理
   
   • 鍋島英知, 宋剛秀
     
   • 解説論文, 人工知能学会誌, 25(1):68-76, 2010.
     
   • (URL) http://id.nii.ac.jp/1004/00007418/
     

6 システム記述

1. sCOP: SAT-based Constraint Programming System.
   
   • Takehide Soh,Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
     
   • Solver Descriptions of XCSP3 Competition 2018 (XCSP18).
     
   • (URL of XCSP3 Competitions) http://xcsp.org/competition
     
   • (URL of Solver Description) http://www.cril.univ-artois.fr/XCSP18/files/scop.pdf
     

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

1. 解集合プログラミングによるカリキュラムベース・コース時間割編成.
   
   • 番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
     
   • 第29回RAMPシンポジウム論文集, pp.73--88, 日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017.
     
2. ブール基数制約を経由した擬似ブール制約のSAT符号化法
   
   • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
   • 南雄之, 宋剛秀, 番原睦則, 田村直之.
     
   • 人工知能基本問題研究会(第103回), 人工知能学会研究会資料 SIG-FPAI-B506-04, pp.18-23, 人工知能学会, 2017.
     
   • (URL) http://id.nii.ac.jp/1004/00008597/
     
3. SAT技術を用いたペトリネットのデッドロック検出手法の提案
   
   • Proposal of SAT-based Method to Detect Deadlock of Petri nets
   • 寸田智也, 宋剛秀, 番原睦則, 田村直之
     
   • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-2, 2017.
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2017.0_1M1OS02a2
     
4. 制約充足問題のASP符号化に関する一考察
   
   • A Study of ASP Encoding of Constraint Satisfaction Problems
   • 坡山直樹, 番原睦則, 宋剛秀, 田村直之
     
   • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-4, 2017.
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2017.0_1M1OS02a4
     
5. SATソルバーの使い方 〜問題をSATに符号化する方法〜
   
   • How to use SAT solvers—How to encode problems to SAT—
   • 田村直之, 宋剛秀, 番原睦則.
     
   • 第58回プログラミング・シンポジウム予稿集, pp.165--172, 情報処理学会, 2017.
     
   • (URL) http://www.ipsj.or.jp/prosym/58/58program.html
     
6. Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー
   
   • Diet-Sugar: SAT-based Constraint Solver Implementing Hybrid SAT Encoding
   • 宋剛秀, 番原睦則, 田村直之.
     
   • 第58回プログラミング・シンポジウム予稿集, pp.71--74, 情報処理学会, 2017.
     
   • (URL) http://www.ipsj.or.jp/prosym/58/58program.html
     
7. SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案
   
   • Proposal of a SAT-based Method to Detect Deadlocks of Ordinary Petri Nets
   • 寸田智也, 宋剛秀, 番原睦則, 田村直之.
     
   • 日本ソフトウェア科学会第33回大会講演論文集, PPL9-2, 日本ソフトウェア科学会, 2016.
     
   • (URL) http://jssst.or.jp/files/user/taikai/2016/PPL/ppl9-2.pdf
     
8. SAT型制約ソルバーによるナンバーリンクの解法とその評価 全国大会優秀賞受賞
   
   • Solving Numberlink by a SAT-based Constraint Solver and its Evaluation
   • 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
     
   • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-3, 人工知能学会, 2016.
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2016.0_1D4OS02a3
     
9. SATソルバーを用いた部分グラフ探索のための制約モデル
   
   • Constraint Models for SAT-based Subgraph Search
   • 川原征大, 宋剛秀, 番原睦則, 田村直之.
     
   • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-4, 人工知能学会, 2016.
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2016.0_1D4OS02a4
     
10. クラウド上のソフトウェア要素最適配置問題の解法
    
    • Solving Optimal Software Component Configuration Problem in Cloud
    • 田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀.
      
    • 人工知能基本問題研究会(第100回), 人工知能学会研究会資料 SIG-FPAI-B503, pp.19-24, 人工知能学会, 2016.
      
    • (URL) http://id.nii.ac.jp/1004/00000889/
      
11. 分子ネットワーク上の状態推定とその可視化による知識発見支援
    
    • Estimating and Visualizing State Transitions of Transcription Factors from Perturbation Experiments
    • 平沼祐人, 山本泰生, 守屋央朗, 宋剛秀, 岩沼宏治.
      
    • 第45回バイオ情報学研究発表会, 研究報告バイオ情報学 (BIO), 2016-BIO-45, Vol. 11, pp. 1--6, 2016.
      
    • (URL) http://id.nii.ac.jp/1001/00158055/
      
12. 解集合プログラミングを用いた制約組合せテストケース生成
    
    • Test Case Generation of Constrained Combinatorial Testing with Answer Set Programming
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太.
      
    • 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 論文集, カテゴリC1, 2016.
      
    • (URL) http://logic.cs.tsukuba.ac.jp/ppl2016/program.html
      
13. SATソルバーを用いた制約プログラミングシステムとその応用
    
    • SAT-based Constraint Programming Systems and its Applications
    • 宋剛秀.
      
    • 第57回プログラミング・シンポジウム, 第57回プログラミング・シンポジウム予稿集, 10ページ, 2016.
      
    • (URL) http://www.ipsj.or.jp/prosym/57/57program.html
      
14. Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
    
    • A Domain-Specific Language in Scala for the Analysis of Metabolic Pathways
    • 宋剛秀, 馬場知哉.
      
    • 日本ソフトウェア科学会第32回大会講演論文集, ソフトウェア-1, 日本ソフトウェア科学会, 2015.
      
    • (URL) https://ci.nii.ac.jp/naid/40020656977
      
15. SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価 学生奨励賞受賞
    
    • Implementation and Evaluation of an Efficient Subgraph Search Tool using SAT Solvers
    • 川原征大, 宋剛秀, 番原睦則, 田村直之.
      
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL3-1, 日本ソフトウェア科学会, 2015.
      
    • (URL) https://ci.nii.ac.jp/naid/40020657178
      
    • (URL) http://jssst.or.jp/files/user/taikai/2015/PPL/ppl3-1.pdf
      
16. iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
    
    • iSugar : A SAT-based Constraint Solver Utilizing In- cremental SAT Method
    • 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳.
      
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-1, 日本ソフトウェア科学会, 2015.
      
    • (URL) http://jssst.or.jp/files/user/taikai/2015/PPL/ppl6-1.pdf
      
17. 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
    
    • A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
    • 宋剛秀, 番原睦則, 田村直之.
      
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-3, 日本ソフトウェア科学会, 2015.
      
    • (URL) http://jssst.or.jp/files/user/taikai/2015/PPL/ppl6-3.pdf
      
    • (URL) https://ci.nii.ac.jp/naid/40020657481
      
18. 組合せテストケース生成問題に対する制約解集合プログラミングの適用. 全国大会優秀賞受賞
    
    • Applying Constraint Answer Set Programming to Combinatorial Test Case Generation Problems
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
      
    • 2015年度人工知能学会全国大会(第29回)論文集, 2H5-OS-03b-5, 人工知能学会, 2015.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2015.0_2H5OS03b5
      
19. 制約充足問題のハイブリッド符号化にむけて
    
    • Towards a Hybrid Encoding of Constraint Satisfaction Problems
    • 宋剛秀, 番原睦則, 田村直之.
      
    • 第97回人工知能基本問題研究会(SIG-FPAI), 人工知能学会研究会資料, SIG-FPAI-B404-12, pp. 65-73, 2015.
      
    • (URL) http://id.nii.ac.jp/1004/00000590/
      
20. Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール 高橋奨励賞受賞
    
    • Prototyping Tool for SAT-based Constraint Programming Systems in Scala
    • 宋剛秀, 番原睦則, 田村直之.
      
    • 日本ソフトウェア科学会第31回大会講演論文集, ソフト1-1, 日本ソフトウェア科学会, 2014.
      
    • (URL) http://jssst.or.jp/files/user/taikai/2014/soft/soft1-1.pdf
      
21. 制約解集合プログラミングシステムの設計方式に関する考察
    
    • Studies on a Design of Constraint Answer Set Programming Systems
    • 宋剛秀, 則武治樹, 番原睦則, 田村直之, 井上克巳.
      
    • 日本ソフトウェア科学会第31回大会講演論文集, PPL2-3, 日本ソフトウェア科学会, 2014.
      
    • (URL) https://ci.nii.ac.jp/naid/40020581916
      
    • (URL) http://jssst.or.jp/files/user/taikai/2014/PPL/PPL2-3.pdf
      
22. SAT型制約ソルバーを用いたナンバーリンクの解法 SLDM優秀論文賞受賞
    
    • Solving Numberlink by a SAT-based Constraint Solver
    • 田村直之, 宋剛秀, 番原睦則, 鍋島英知.
      
    • DAシンポジウム2014論文集, DA2014-7B-2, pp.215-220, 情報処理学会システムとLSIの設計技術研究会, 2014.
      
    • (URL) https://ci.nii.ac.jp/naid/170000084795
      
    • (URL) http://id.nii.ac.jp/1001/00102757/
      
23. 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法.
    
    • Solving Post-Enrollment Course Timetabling using Cardinality Constraint and SAT Solvers
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
      
    • 2014年度人工知能学会全国大会(第28回)論文集, 1D5-OS-11b-7, 人工知能学会, 2014.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2014.0_1D5OS11b7
      
24. SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用
    
    • SAT-based CP System Scarab and its Application to Hamiltonian Cycle Problem
    • 宋剛秀, Daniel Le Berre, Stéphanie Roussel, 番原睦則，田村直之
      
    • 2014年度人工知能学会全国大会(第28回)論文集, 1D5-OS-11b-6in, 人工知能学会, 2014.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2014.0_1D5OS11b6i
      
25. パッキング配列問題の制約モデリングとSAT符号化
    
    • Constraint Modeling and SAT Encoding of the Packing Array Problem
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
      
    • 日本ソフトウェア科学会第30回大会講演論文集, PPL1-1, 日本ソフトウェア科学会, 2013.
      
    • (URL) https://jssst2013.wordpress.com/program-911/
      
26. Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について.
    
    • Scarab: A Prototyping Tool for SAT-based Constraint Programming Systems in Scala
    • 宋剛秀, 番原睦則, 田村直之, Daniel Le Berre, Stéphanie Roussel.
      
    • 日本ソフトウェア科学会第30回大会講演論文集, PPL2-5, 日本ソフトウェア科学会, 2013.
      
    • (URL) http://jssst.or.jp/files/user/taikai/2013/ppl2/ppl2-5.pdf
      
27. 正方形詰込み問題の制約モデルとSAT符号化を用いた解法
    
    • Constraint Models of the Square Packing Problem and their SAT Encodings
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
      
    • 2013年度人工知能学会全国大会(第27回)論文集, 2E5-OS-09b-1, 人工知能学会, 2013.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2013.0_2E5OS09b1
      
28. SAT符号化を用いたパッキング配列の構成
    
    • Constructing Packing Arrays by SAT Encoding
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
      
    • 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集, カテゴリC1, 2013.
      
    • (URL) http://www.pllab.riec.tohoku.ac.jp/ppl2013/timetable-without-abstract.html
      
29. 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.
      
    • (DOI) https://www.thinkmind.org/index.php?view=article&articleid=lifsci_v4_n34_2012_8
      
30. 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.
      
    • (DOI) https://www.thinkmind.org/index.php?view=article&articleid=biotechno_2012_1_30_50068
      
31. 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.
      
    • (DOI) http://id.nii.ac.jp/1001/00079763/
      
32. モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
    
    • Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
    • 宋剛秀, 井上克巳
      
    • 人工知能学会第24回全国大会 (JSAI 2010), 人工知能学会, 2010.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2010.0_1E13
      
33. SAT問題への変換を用いたフィードバックを含むパスウェイの解析 全国大会優秀賞受賞
    
    • Analyzing Pathways through a Translation into SAT Problems
    • 宋剛秀, 井上克巳
      
    • 人工知能学会第23回全国大会 (JSAI 2009), 人工知能学会, 2009.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2009.0_2H33
      
34. ショップ・スケジューリング問題のSAT変換による解法
    
    • Solving Shop Scheduling Problems by SAT encoding
    • 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知,
      
    • スケジューリング・シンポジウム2007, pages 97-102, スケジューリング学会, 2007.
      
35. 効率的なSATプランニングとSAT スケジューリングのための補題再利用
    
    • Effective SAT Planning and SAT Scheduling by Lemma Reusing
    • 鍋島英知, 宋剛秀, 井上克巳, 岩沼宏治
      
    • 電子情報通信学会技術研究報告, 106(38): 19-24, 信学技報, 2006.
      
    • (URL) https://ci.nii.ac.jp/naid/110004744913
      
36. 行列分割を用いたBlock Lanczos 法の改良
    
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
      
    • 暗号と情報セキュリティシンポジウム予稿集, pages 40, 信学会情報セキュリティ研究専門委員会, 2006.
      
    • (URL) http://scis.jp/2006/program/
      
37. Dual-CPU 上におけるBlock Lanczos 法の並列実装
    
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
      
    • 信学会ソサエティ大会, A-7-4, 電子情報通信学会, 2005.
      
    • (URL) https://www.ieice.org/jpn/event/societytaikai.html
      
38. 複数のSATソルバを用いたジョブショップスケジューリング問題の解法
    
    • Solving Job-shop Scheduling Problems with Multiple SAT Solvers
    • 宋剛秀, 井上克巳
      
    • 信学技報, 104(133): 19-24, 電子情報通信学会技術研究報告, 2004.
      
    • (URL) https://ci.nii.ac.jp/naid/110003176997
      

8 その他の記事・著作物

1. OS-2「SAT 技術の理論, 実装, 応用」
   
   • 波多野大輔, 戸田貴久, 宋剛秀
     
   • 人工知能学会誌, 31(6):879, 2016
     
   • (URL) http://id.nii.ac.jp/1004/00008927/
     
2. OS-3「SAT 技術の理論, 実装, 応用」
   
   • 戸田貴久, 波多野大輔, 宋剛秀
     
   • 人工知能学会誌, 30(6):773, 2015
     
   • (URL) http://id.nii.ac.jp/1004/00001947/
     
3. OS-11「SAT 技術の理論, 実装, 応用」
   
   • 宋剛秀, 鍋島英知, 越村三幸
     
   • 人工知能学会誌, 29(6):641, 2014
     
   • (URL) http://id.nii.ac.jp/1004/00001666/
     
4. OS-09「SAT 技術の理論, 実装, 応用」
   
   • 越村三幸, 鍋島英知, 宋剛秀
     
   • 人工知能学会誌, 28(6):942, 2013
     
   • (URL) http://id.nii.ac.jp/1004/00008415/
     
5. 国際シンポジウムFLOPS 2012開催報告
   
   • 国際シンポジウムFLOPS 2012開催報告
   • 田村直之，番原睦則，平山勝敏，宋剛秀
     
   • コンピュータソフトウェア 30(1):16-19, 2013
     
   • (DOI) https://doi.org/10.11309/jssst.30.1_16
     
6. 私のブックマーク：SAT ソルバー
   
   • 番原睦則，宋剛秀，田村直之，井上克巳
     
   • 人工知能学会誌，28(2):343-348，2013年3月．
     
   • (URL) https://www.ai-gakkai.or.jp/my-bookmark_vol28-no2/
     
   • (URL) http://id.nii.ac.jp/1004/00008251/
     

9 招待講演

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

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.
      

11 博士論文

1. Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems
   
   • Takehide Soh
     
   • School of Multidisciplinary Sciences, The Graduate University for Advanced Studies, Japan, 125 pages
     
   • (URL) http://id.nii.ac.jp/1013/00002566/