@Helsinki

SOH, Takehide
宋 剛秀

English Page | Japanese Page
Tamura Lab | CSPSAT | Scarab

1 Profile Pages

2 Journal Papers (with peer review)

  1. A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
  2. Proposal of SAT-Based Method to Detect Deadlock of Petri Nets
  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. An Incremental SAT Solving Library and its Applications
  7. Constraint Modeling and SAT Encoding of the Packing Array Problem
  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. Enumerating Minimal Active Metabolic Pathways by Model Generation
  10. A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
  11. A Competitive and Cooperative Approach to Propositional Satisfiability

3 Conference Proceedings (with peer review)

  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 International Workshop Proceedings (with peer review)

  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 of Workshop Proceeding) http://ceur-ws.org/Vol-451/
    • (URL of Paper) 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 Survey/Tutorial Papers

  1. Recent Advances in SAT Solvers and their Utilization Technologies
  2. SAT-based Constraint Programming Systems and Related Technologies
  3. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver
  4. Principles of Modern SAT Solvers

6 System Description

  1. sCOP: SAT-based Constraint Programming System.

7 Other Papers (without peer review)

  1. 解集合プログラミングによるカリキュラムベース・コース時間割編成.
    • Mutsunori Banbara, Katsumi Inoue, ベンジャミン カウフマン, トルステン シャウブ, Takehide Soh, Naoyuki Tamura, フィリップ ワンコ
    • 第29回RAMPシンポジウム論文集, pp.73--88, 日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017.
  2. A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
  3. Proposal of SAT-based Method to Detect Deadlock of Petri nets
  4. A Study of ASP Encoding of Constraint Satisfaction Problems
  5. How to use SAT solvers---How to encode problems to SAT---
  6. Diet-Sugar: SAT-based Constraint Solver Implementing Hybrid SAT Encoding
  7. Proposal of a SAT-based Method to Detect Deadlocks of Ordinary Petri Nets
  8. Solving Numberlink by a SAT-based Constraint Solver and its Evaluation
  9. Constraint Models for SAT-based Subgraph Search
  10. Solving Optimal Software Component Configuration Problem in Cloud
  11. Estimating and Visualizing State Transitions of Transcription Factors from Perturbation Experiments
    • 平沼祐人, 山本泰生, 守屋央朗, Takehide Soh, 岩沼宏治.
    • 第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
    • Hiromasa Kaneyuki, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, 沖本天太.
    • 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016) 論文集, カテゴリC1, 2016.
    • (URL) http://logic.cs.tsukuba.ac.jp/ppl2016/program.html
  13. SAT-based Constraint Programming Systems and its Applications
  14. A Domain-Specific Language in Scala for the Analysis of Metabolic Pathways
    • Takehide Soh, Tomoya Baba.
    • 日本ソフトウェア科学会第32回大会講演論文集, ソフトウェア-1, 日本ソフトウェア科学会, 2015.
    • (URL) https://ci.nii.ac.jp/naid/40020656977
  15. Implementation and Evaluation of an Efficient Subgraph Search Tool using SAT Solvers .
  16. iSugar : A SAT-based Constraint Solver Utilizing Incremental SAT Method .
    • Tatsuya Sako, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima, and Katsumi Inoue.
    • The 32st Conference of Japan Society for Software Science and Technology (JSSST 2015), PPL6-1, Japan Society for Software Science and Technology, 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 .
  18. Applying Constraint Answer Set Programming to Combinatorial Test Case Generation Problems .
    • Hiromasa Kaneyuki, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura and Katsumi Inoue.
    • The 29th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2015), 2H5-OS-03b-5, The Japanese Society for Artificial Intelligence, 2015. JSAI Annual Conference Award.
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2015.0_2H5OS03b5
  19. Prototyping Tool for SAT-based Constraint Programming Systems in Scala .
    • Takehide Soh, Mutsunori Banbara and Naoyuki Tamura. Prototyping Tool for SAT-based.
    • The 31st Conference of Japan Society for Software Science and Technology (JSSST 2014), SOFT1-1, Japan Society for Software Science and Technology, 2014.
    • (URL) http://jssst.or.jp/files/user/taikai/2014/soft/soft1-1.pdf
  20. Studies on a Design of Constraint Answer Set Programming Systems .
  21. Solving Numberlink by a SAT-based Constraint Solver .
  22. Solving Post-Enrollment Course Timetabling using Cardinality Constraint and SAT Solvers .
    • Atsushi Sakoda, Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura.
    • The 28th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2014), 1D5-OS-11b-7, The Japanese Society for Artificial Intelligence, 2014.
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2014.0_1D5OS11b7
  23. SAT-based CP System Scarab and its Application to Hamiltonian Cycle Problem .
    • Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, and Naoyuki Tamura.
    • The 28th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2014), 1D5-OS-11b-6in, The Japanese Society for Artificial Intelligence, 2014.
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2014.0_1D5OS11b6i
  24. Constraint Modeling and SAT Encoding of the Packing Array Problem .
    • Haruki Noritake, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, and Katsumi Inoue.
    • The 30th Conference of Japan Society for Software Science and Technology (JSSST 2013), PPL1-1, Japan Society for Software Science and Technology, 2013.
    • (URL) https://jssst2013.wordpress.com/program-911/
  25. Scarab: A Prototyping Tool for SAT-based Constraint Programming Systems in Scala .
    • Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stéphanie Roussel.
    • The 30th Conference of Japan Society for Software Science and Technology (JSSST 2013), PPL2-5, Japan Society for Software Science and Technology, 2013.
    • (URL) http://jssst.or.jp/files/user/taikai/2013/ppl2/ppl2-5.pdf
  26. Constraint Models of the Square Packing Problem and their SAT Encodings .
    • Atsushi Sakoda, Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura.
    • The 27th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2013), 2E5-OS-09b-1, The Japanese Society for Artificial Intelligence, 2013.
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2013.0_2E5OS09b1
  27. Constructing Packing Arrays by SAT Encoding.
  28. Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration
  29. Predicting Gene Knockout Effects by Minimal Pathway Enumeration
  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.
    • (DOI) http://id.nii.ac.jp/1001/00079763/
  31. Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
  32. Analyzing Pathways through a Translation into SAT Problems
  33. Solving Shop Scheduling Problems by SAT Encoding
    • Naoyuki Tamura, Akiko Taga, Mutsunori Banbara, Takehide Soh, Hidetomo Nabeshima, and Katsumi Inoue.
    • Proceedings of the Scheduling Symposium 2007, pp.97-102, The Sceduling Society of Japan, 2007.
  34. Effective SAT Planning and SAT Scheduling by Lemma Reusing
    • Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, and Koji Iwanuma
    • Technical Report of IEICE, 106(38): 19-24, The Institute of Electronics, Information and Communication Engineers, 2006.
    • (URL) https://ci.nii.ac.jp/naid/110004744913
  35. Solving Job Shop Scheduling Problems With Multiple SAT Solvers
    • Takehide Soh and Katsumi Inoue
    • Technical Report of IEICE, 104(133): 19-24, The Institute of Electronics, Information and Communication Engineers, 2004.
    • (URL) https://ci.nii.ac.jp/naid/110003176997

8 Other Report etc.

  1. OS-2 ``Theory, Implementation, and Applications of SAT Technology''
    • Daisuke Hatano, Takahisa Toda, Takehide Soh
    • Journal of Japanese Society for Artificial Intelligence, 31(6):879, 2016
  2. OS-3 ``Theory, Implementation, and Applications of SAT Technology''
    • Takahisa Toda, Daisuke Hatano, Takehide Soh
    • Journal of Japanese Society for Artificial Intelligence, 30(6):773, 2015
  3. OS-11 ``Theory, Implementation, and Applications of SAT Technology''
    • Takehide Soh, Hidetomo Nabeshima, Miyuki Koshimura
    • Journal of Japanese Society for Artificial Intelligence, 29(6):641, 2014
  4. OS-09 ``Theory, Implementation, and Applications of SAT Technology''
    • Miyuki Koshimura, Hidetomo Nabeshima, Takehide Soh
    • Journal of Japanese Society for Artificial Intelligence, 28(6):942, 2013
  5. Report of 2012 FLOPS International Symposium
  6. My Bookmark: SAT Solver

9 Oral and Poster Presentations

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

10 Dissertation

  1. Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems

Author: Takehide Soh

Created: 2018-12-29 土 17:11

Validate