Skip to content

Publication List

Conference Proceedings (Reviewed)

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

  1. Hamiltonian Cycle Reconfiguration with Answer Set Programming
    • Takahiro Hirate, Mutsunori Banbara, Katsumi Inoue, Xiao-Nan Lu, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    • Proceedings of the 18th European Conference (JELIA 2023), LNAI 14281, pp.262-277, 2023.
    • DOI
  2. 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), LNCS 14137, pp. 175-183, 2023.
    • DOI
  3. ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems
    • Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
    • Proceedings of the International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2023), LNCS 13884, pp. 167-183, 2023.
    • DOI
  4. 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 (BIOSTEC 2023) - 14th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS 2023), pp. 163-174, 2023.
    • DOI
  5. 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), LNCS 10416, pp. 596-614, 2017.
    • DOI
  6. 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
  7. 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
  8. 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, ACM DL
  9. 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
  10. 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, ACM DL
  11. 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, ACM DL
  12. 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, ACM DL
  13. 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, ACM DL
  14. 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, ACM DL
  15. 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, ACM DL

Workshop Proceedings (Reviewed)

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

  1. Towards CEGAR-based Parallel SAT Solving
    • Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue
    • Pragmatics of SAT 2021 2021年7月
  2. 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, arXiv
  3. 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, DOI
  4. 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, CEUR-WS
  5. 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. URL

Journal (Reviewed)

学術論文誌 (査読あり)

  1. ブール基数制約を経由した擬似ブール制約のSAT符号化手法
    • 南雄之, 宋剛秀, 番原睦則, 田村直之.
    • コンピュータソフトウェア, 35(3): 65-78, 2018.
    • DOI
  2. SAT技術を用いたペトリネットのデッドロック検出手法の提案 情報処理学会 2018年度特選論文
    • 寸田智也, 宋剛秀, 番原睦則, 田村直之, 井上 克巳.
    • 情報処理学会論文誌, 59(9): 1749--1760, 2018.
    • PERM LINK
  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
  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
  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, ACM DL
  6. インクリメンタルSAT解法ライブラリとその応用.
    • 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳.
    • コンピュータソフトウェア, 33(4):16-29, 2016.
    • DOI
  7. パッキング配列問題の制約モデリングとSAT符号化. 第20回研究論文賞（2015年度）
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
    • コンピュータソフトウェア, 31(1): 116-130, 2014.
    • DOI
  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
  9. モデル生成を用いた代謝ネットワークにおける極小活性パスウェイの列挙
    • 宋剛秀, 井上克巳
    • 人工知能学会論文誌, 27(3):204-212, 2012.
    • DOI
  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, ACM DL
  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, ACM DL

Survey/Overview Articles

解説論文

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

System Descriptions

システム記述

  1. Solver Description of Fun-sCOP

    • Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura
    • Solver Descriptions of XCSP3 Competition 2019 (XCSP19)
    • (URL of XCSP3 Competitions) http://xcsp.org/competition

  2. 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

Other papers

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

  1. ZDDを用いた疑似ブール制約のSAT符号化
    • 大橋 瞭雅, 宋 剛秀
    • 人工知能基本問題研究会 126 6-11 2020年3月8日
  2. 最大独立集合問題のSAT技術を用いた解法に関する研究
    • 大森 嶺, 宋 剛秀, 田村 直之
    • 2023年度人工知能学会全国大会(第37回)論文集, 2I4-OS-9a-03, 2023
    • DOI
  3. 解集合プログラミングを用いたハミルトン閉路遷移問題の解法.
    • 平手貴大, 番原睦則, 井上克巳, 盧暁南, 鍋島英知, 宋剛秀, 田村直之
    • 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, カテゴリC1, 2023年3月6日
  4. Core Challenge 2022: Solver and Graph Descriptions.
    • Takehide Soh, Yoshio Okamoto, Takehiro Ito
    • CoRR abs/2208.02495 2022年9月
  5. 解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価
    • 桑原和也, 宋剛秀, 田村直之, 番原睦則
    • 情報処理学会第84回全国大会講演論文集 2022年3月
  6. チャネリング制約を用いた alldifferent 制約の SAT 符号化
    • 小菅脩司, 宋剛秀, 田村直之, 番原睦則
    • 情報処理学会第84回全国大会講演論文集 2022年3月
  7. ZDDを用いた組合せ遷移ソルバーについての考察
    • 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一, 戸田 貴久
    • 冬のLAシンポジウム, 2022年2月
  8. 有界モデル検査による独立集合遷移問題の解法に関する考察
    • 戸田 貴久, 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一
    • 情報処理学会 研究報告アルゴリズム（AL） 2022-AL-186(5) 1-7 2022年1月
  9. CEGARと反例の共有を用いたSAT型CSPソルバーの並列化方法の考察
    • 宋 剛秀, 鍋島 英知, 番原 睦則, 田村 直之, 井上 克巳
    • 人工知能基本問題研究会 112 6-11 2020年3月8日
  10. 解集合プログラミングによる様相命題論理Kの充足可能性判定
    • 飯野 有軌, 田村 直之, 宋 剛秀, 番原 睦則, 井上 克巳
    • 人工知能学会全国大会論文集 2020 2N5OS17b05-2N5OS17b05 2020年
  11. alldifferent制約のブール基数制約への符号化手法の提案とクイーングラフ彩色問題への応用
    • 大野周亮, 番原睦則, 宋剛秀, 田村 直之
    • 人工知能学会研究会資料 SIG-FPAI-B803 6-11 2019年3月
    • DOI
  12. A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
    • 宋 剛秀, Le Berre Daniel, 番原 睦則, 田村 直之
    • 人工知能学会全国大会論文集 2019 1E2OS3a03-1E2OS3a03 2019年
  13. 解集合プログラミングによるカリキュラムベース・コース時間割編成.
    • 番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
    • 第29回RAMPシンポジウム論文集, pp.73--88, 日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017.
  14. ブール基数制約を経由した擬似ブール制約のSAT符号化法
    • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
    • 南雄之, 宋剛秀, 番原睦則, 田村直之.
    • 人工知能基本問題研究会(第103回), 人工知能学会研究会資料 SIG-FPAI-B506-04, pp.18-23, 人工知能学会, 2017.
    • URL
  15. SAT技術を用いたペトリネットのデッドロック検出手法の提案
    • Proposal of SAT-based Method to Detect Deadlock of Petri nets
    • 寸田智也, 宋剛秀, 番原睦則, 田村直之
    • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-2, 2017.
    • DOI
  16. 制約充足問題のASP符号化に関する一考察
    • A Study of ASP Encoding of Constraint Satisfaction Problems
    • 坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • 2017年度人工知能学会全国大会(第31回)論文集, 1M1-OS-02a-4, 2017.
    • DOI
  17. SATソルバーの使い方 〜問題をSATに符号化する方法〜
    • How to use SAT solvers—How to encode problems to SAT—
    • 田村直之, 宋剛秀, 番原睦則.
    • 第58回プログラミング・シンポジウム予稿集, pp.165--172, 情報処理学会, 2017.
    • URL
  18. Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー
    • Diet-Sugar: SAT-based Constraint Solver Implementing Hybrid SAT Encoding
    • 宋剛秀, 番原睦則, 田村直之.
    • 第58回プログラミング・シンポジウム予稿集, pp.71--74, 情報処理学会, 2017.
    • URL
  19. SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案
    • Proposal of a SAT-based Method to Detect Deadlocks of Ordinary Petri Nets
    • 寸田智也, 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第33回大会講演論文集, PPL9-2, 日本ソフトウェア科学会, 2016.
    • URL
  20. SAT型制約ソルバーによるナンバーリンクの解法とその評価 全国大会優秀賞受賞
    • Solving Numberlink by a SAT-based Constraint Solver and its Evaluation
    • 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
    • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-3, 人工知能学会, 2016.
    • DOI
  21. SATソルバーを用いた部分グラフ探索のための制約モデル
    • Constraint Models for SAT-based Subgraph Search
    • 川原征大, 宋剛秀, 番原睦則, 田村直之.
    • 2016年度人工知能学会全国大会(第30回)論文集, 1D4-OS-02a-4, 人工知能学会, 2016.
    • DOI
  22. クラウド上のソフトウェア要素最適配置問題の解法
    • Solving Optimal Software Component Configuration Problem in Cloud
    • 田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀.
    • 人工知能基本問題研究会(第100回), 人工知能学会研究会資料 SIG-FPAI-B503, pp.19-24, 人工知能学会, 2016.
    • CiNii
  23. 分子ネットワーク上の状態推定とその可視化による知識発見支援
    • Estimating and Visualizing State Transitions of Transcription Factors from Perturbation Experiments
    • 平沼祐人, 山本泰生, 守屋央朗, 宋剛秀, 岩沼宏治.
    • 第45回バイオ情報学研究発表会, 研究報告バイオ情報学 (BIO), 2016-BIO-45, Vol. 11, pp. 1--6, 2016.
    • CiNii
  24. 解集合プログラミングを用いた制約組合せテストケース生成
    • Test Case Generation of Constrained Combinatorial Testing with Answer Set Programming
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太.
    • 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 論文集, カテゴリC1, 2016.
    • URL
  25. SATソルバーを用いた制約プログラミングシステムとその応用
    • SAT-based Constraint Programming Systems and its Applications
    • 宋剛秀.
    • 第57回プログラミング・シンポジウム, 第57回プログラミング・シンポジウム予稿集, 10ページ, 2016.
    • URL
  26. Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
    • A Domain-Specific Language in Scala for the Analysis of Metabolic Pathways
    • 宋剛秀, 馬場知哉.
    • 日本ソフトウェア科学会第32回大会講演論文集, ソフトウェア-1, 日本ソフトウェア科学会, 2015.
    • CiNii
  27. SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価 学生奨励賞受賞
    • Implementation and Evaluation of an Efficient Subgraph Search Tool using SAT Solvers
    • 川原征大, 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL3-1, 日本ソフトウェア科学会, 2015.
    • CiNii, URL
  28. iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
    • iSugar : A SAT-based Constraint Solver Utilizing In- cremental SAT Method
    • 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-1, 日本ソフトウェア科学会, 2015.
    • URL
  29. 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
    • A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
    • 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第32回大会講演論文集, PPL6-3, 日本ソフトウェア科学会, 2015.
    • URL, CiNii
  30. 組合せテストケース生成問題に対する制約解集合プログラミングの適用. 全国大会優秀賞受賞
    • Applying Constraint Answer Set Programming to Combinatorial Test Case Generation Problems
    • 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
    • 2015年度人工知能学会全国大会(第29回)論文集, 2H5-OS-03b-5, 人工知能学会, 2015.
    • DOI
  31. 制約充足問題のハイブリッド符号化にむけて
    • Towards a Hybrid Encoding of Constraint Satisfaction Problems
    • 宋剛秀, 番原睦則, 田村直之.
    • 第97回人工知能基本問題研究会(SIG-FPAI), 人工知能学会研究会資料, SIG-FPAI-B404-12, pp. 65-73, 2015.
    • CiNii
  32. Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール 高橋奨励賞受賞
    • Prototyping Tool for SAT-based Constraint Programming Systems in Scala
    • 宋剛秀, 番原睦則, 田村直之.
    • 日本ソフトウェア科学会第31回大会講演論文集, ソフト1-1, 日本ソフトウェア科学会, 2014.
    • URL
  33. 制約解集合プログラミングシステムの設計方式に関する考察
    • Studies on a Design of Constraint Answer Set Programming Systems
    • 宋剛秀, 則武治樹, 番原睦則, 田村直之, 井上克巳.
    • 日本ソフトウェア科学会第31回大会講演論文集, PPL2-3, 日本ソフトウェア科学会, 2014.
    • CiNii, URL
  34. SAT型制約ソルバーを用いたナンバーリンクの解法 SLDM優秀論文賞受賞
    • Solving Numberlink by a SAT-based Constraint Solver
    • 田村直之, 宋剛秀, 番原睦則, 鍋島英知.
    • DAシンポジウム2014論文集, DA2014-7B-2, pp.215-220, 情報処理学会システムとLSIの設計技術研究会, 2014.
    • CiNii, URL
  35. 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法.
    • Solving Post-Enrollment Course Timetabling using Cardinality Constraint and SAT Solvers
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
    • 2014年度人工知能学会全国大会(第28回)論文集, 1D5-OS-11b-7, 人工知能学会, 2014.
    • DOI
  36. 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
  37. パッキング配列問題の制約モデリングとSAT符号化
    • Constraint Modeling and SAT Encoding of the Packing Array Problem
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
    • 日本ソフトウェア科学会第30回大会講演論文集, PPL1-1, 日本ソフトウェア科学会, 2013.
    • URL
  38. 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
  39. 正方形詰込み問題の制約モデルとSAT符号化を用いた解法
    • Constraint Models of the Square Packing Problem and their SAT Encodings
    • 佐古田淳史, 宋剛秀, 番原睦則, 田村直之.
    • 2013年度人工知能学会全国大会(第27回)論文集, 2E5-OS-09b-1, 人工知能学会, 2013.
    • DOI
  40. SAT符号化を用いたパッキング配列の構成
    • Constructing Packing Arrays by SAT Encoding
    • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳.
    • 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集, カテゴリC1, 2013.
    • URL
  41. 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
  42. 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
  43. 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.
    • CiNii
  44. モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
    • Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
    • 宋剛秀, 井上克巳
    • 人工知能学会第24回全国大会 (JSAI 2010), 人工知能学会, 2010.
    • DOI
  45. SAT問題への変換を用いたフィードバックを含むパスウェイの解析 全国大会優秀賞受賞
    • Analyzing Pathways through a Translation into SAT Problems
    • 宋剛秀, 井上克巳
    • 人工知能学会第23回全国大会 (JSAI 2009), 人工知能学会, 2009.
    • DOI
  46. ショップ・スケジューリング問題のSAT変換による解法
    • Solving Shop Scheduling Problems by SAT encoding
    • 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知,
    • スケジューリング・シンポジウム2007, pages 97-102, スケジューリング学会, 2007.
  47. 効率的なSATプランニングとSAT スケジューリングのための補題再利用
    • Effective SAT Planning and SAT Scheduling by Lemma Reusing
    • 鍋島英知, 宋剛秀, 井上克巳, 岩沼宏治
    • 電子情報通信学会技術研究報告, 106(38): 19-24, 信学技報, 2006.
    • CiNii
  48. 行列分割を用いたBlock Lanczos 法の改良
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
    • 暗号と情報セキュリティシンポジウム予稿集, pages 40, 信学会情報セキュリティ研究専門委員会, 2006.
    • URL
  49. Dual-CPU 上におけるBlock Lanczos 法の並列実装
    • 宋剛秀, 桑門秀典, 森井昌克, 田中初一
    • 信学会ソサエティ大会, A-7-4, 電子情報通信学会, 2005.
    • URL
  50. 複数のSATソルバを用いたジョブショップスケジューリング問題の解法
    • Solving Job-shop Scheduling Problems with Multiple SAT Solvers
    • 宋剛秀, 井上克巳
    • 信学技報, 104(133): 19-24, 電子情報通信学会技術研究報告, 2004.
    • CiNii

Misc

その他の記事・著作物

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

Oral/Poster Presentations

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

  1. CDCL型SATソルバーの内部動作可視化ツール
    • 堀岡真未, 宋剛秀, 田村直之
    • 日本ソフトウェア科学会第38回大会ポスター発表 2021年9月
  2. ライフゲームを逆向きに動かす
    • 足立啓一, 宋剛秀, 田村直之
    • 日本ソフトウェア科学会第38回大会ポスター発表 2021年9月
  3. SATソルバーを用いた一層平面配置配線問題の解法に関する考察
    • 三嶋哲平, 宋剛秀, 田村直之
    • 日本ソフトウェア科学会第37回大会ポスター発表 2020年9月
  4. 正規制約のSAT符号化とその性能評価.
    • 生田哲也, 田村直之, 番原睦則, 宋剛秀
    • 日本ソフトウェア科学会第35回大会, デモ・ポスター発表, 2018
  5. SATソルバーを用いた様相命題論理S4の充足可能性判定.
    • 飯野有軌, 田村直之, 番原睦則, 宋剛秀
    • 日本ソフトウェア科学会第35回大会, デモ・ポスター発表, 2018
  6. 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
  7. SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
    • 寸田智也, 南雄之, 宋剛秀, 田村直之
    • DAシンポジウム2017, ADC-2, 情報処理学会システムとLSIの設計技術研究会, 2017
  8. SATソルバーの最新動向と利用技術. PPL2017発表賞（一般の部）受賞
    • 宋剛秀, 田村直之.
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), サーベイ・チュートリアル発表, 2017.
  9. SugarTracer: SAT型制約ソルバーSugarのトレースツール.
    • 吉玉元和, 寸田智也, 南雄之, 宋剛秀, 番原睦則, 田村 直之.
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), ポスター発表, 2017.
  10. 解集合プログラミングを用いた多層ナンバーリンクの解法.
    • 坡山直樹, 川原征大, 迫龍哉, 宋剛秀, 番原睦則, 田村直之
    • 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), ポスター発表, 2017.
  11. SAT型制約ソルバーを用いた多層ナンバーリンクの解法.
    • 寸田智也, 南雄之, 吉玉元和, 宋剛秀.
    • DAシンポジウム2016, 情報処理学会 システムとLSIの設計技術研究会（SLDM）, 2016
  12. インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー.
    • 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知.
    • プログラミング言語ワークショップ (PPL 2016), ポスター発表, 2016.
  13. SAT型制約ソルバーによるナンバーリンクの求解と解の最適化.
    • 迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知.
    • DAシンポジウム2015, ADC-2, 情報処理学会システムとLSIの設計技術研究会, 2015
  14. Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
    • 宋剛秀, 番原睦則, 田村直之
    • 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015), 日本ソフトウェア科学会, 2015
  15. Answer Set Programming as a Modeling Language for Course Timetabling
    • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
    • 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014), 日本ソフトウェア科学会, 2014
  16. 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
  17. 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.
  18. 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.
  19. 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
  20. Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール.
    • 宋剛秀, 田村直之, 番原睦則
    • 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013), 日本ソフトウェア科学会, 2013
  21. 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.
  22. A SAT-based Method for Analyzing Metabolic Pathways
    • Takehide Soh and Katsumi Inoue
    • Poster presentation at: Systems Biochemistry 2010, University of York, 2010.
  23. 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.
  24. 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.

Thesis

博士論文

  • 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/