SOH, Takehide
宋 剛秀

1 Profile Pages

2 Journal Papers (with peer review)

1. A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
   
   • Yushi Minami, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • Computer Software, 35(3): 65-78, 2018.
     
   • (DOI) https://doi.org/10.11309/jssst.35.3_65
     
2. Proposal of SAT-Based Method to Detect Deadlock of Petri Nets
   
   • Tomoya Sunda, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue.
     
   • IPSJ Journal, 59(9), 17-A113.R1, 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. An Incremental SAT Solving Library and its Applications
   
   • Tatsuya Sako, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima, Katsumi Inoue.
     
   • Computer Software, 33(4): 16-29, 2016.
     
   • (DOI) https://doi.org/10.11309/jssst.33.4_16
     
7. Constraint Modeling and SAT Encoding of the Packing Array Problem
   
   • Haruki Noritake, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, and Katsumi Inoue.
     
   • Computer Software, 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. Enumerating Minimal Active Metabolic Pathways by Model Generation
   
   • Takehide Soh and Katsumi Inoue
     
   • Transactions of the Japan Society for Artificial Intelligence, 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 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
   
   • 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 International Workshop Proceedings (with peer review)

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 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.
     
     • 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 Survey/Tutorial Papers

1. Recent Advances in SAT Solvers and their Utilization Technologies
   
   • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima.
     
   • Computer Software, 35(4):72--92, 2018.
     
   • (DOI) https://doi.org/10.11309/jssst.35.4_72
     
2. SAT-based Constraint Programming Systems and Related Technologies
   
   • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • Computer Software, 34(1):67-80, 2017.
     
   • (DOI) https://doi.org/10.11309/jssst.34.1_67
     
3. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver
   
   • Naoyuki Tamura, Takehide Soh, Mutsunori Banbara
     
   • IPSJ Magazine, 57(8): 710-715, 2016.
     
   • (URL) http://id.nii.ac.jp/1001/00169409/
     
4. Principles of Modern SAT Solvers
   
   • Hidetomo Nabeshima and Takehide Soh
     
   • Journal of the Japan Society for Artificial Intelligence, 25(1):68-76, 2010.
     
   • (URL) http://id.nii.ac.jp/1004/00007418/
     

6 System Description

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 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
   
   • Yushi Minami, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • SIG-FPAI-B506
     
   • (URL) http://id.nii.ac.jp/1004/00008597/
     
3. Proposal of SAT-based Method to Detect Deadlock of Petri nets
   
   • Tomoya Sunda, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
     
   • The 31th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2017)
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2017.0_1M1OS02a2
     
4. A Study of ASP Encoding of Constraint Satisfaction Problems
   
   • Naoki Hayama, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura
     
   • The 31th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2017)
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2017.0_1M1OS02a4
     
5. How to use SAT solvers---How to encode problems to SAT---
   
   • Naoyuki Tamura, Takehide Soh, Mutsunori Banbara.
     
   • Proceedings of the 58th Programming Symposium
     
   • (URL) http://www.ipsj.or.jp/prosym/58/58program.html
     
6. Diet-Sugar: SAT-based Constraint Solver Implementing Hybrid SAT Encoding
   
   • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • Proceedings of the 58th Programming Symposium
     
   • (URL) http://www.ipsj.or.jp/prosym/58/58program.html
     
7. Proposal of a SAT-based Method to Detect Deadlocks of Ordinary Petri Nets
   
   • Tomoya Sunda, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • The 33rd Conference of Japan Society for Software Science and Technology (JSSST 2016)
     
   • (URL) http://jssst.or.jp/files/user/taikai/2016/PPL/ppl9-2.pdf
     
8. Solving Numberlink by a SAT-based Constraint Solver and its Evaluation
   
   • Tatsuya Sako, Masahiro Kawahara, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima.
     
   • The 30th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2016)
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2016.0_1D4OS02a3
     
9. Constraint Models for SAT-based Subgraph Search
   
   • Masahiro Kawahara, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura.
     
   • The 30th Annual Conference of the Japanese Society for Artificial Intelligence (JSAI 2016)
     
   • (DOI) https://doi.org/10.11517/pjsai.JSAI2016.0_1D4OS02a4
     
10. Solving Optimal Software Component Configuration Problem in Cloud
    
    • Naoyuki Tamura, Katsumi Inoue, Hidetomo Nabeshima, Mutsunori Banbara, Takehide Soh.
      
    • SIG-FPAI-B503
      
    • (URL) http://id.nii.ac.jp/1004/00000889/
      
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
    
    • Takehide Soh.
      
    • 第57回プログラミング・シンポジウム, 第57回プログラミング・シンポジウム予稿集, 10ページ, 2016.
      
    • (URL) http://www.ipsj.or.jp/prosym/57/57program.html
      
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 .
    
    • Masahiro Kawahara, Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura.
      
    • The 32st Conference of Japan Society for Software Science and Technology (JSSST 2015), PPL3-1, Japan Society for Software Science and Technology, 2015.
      
    • (URL) https://ci.nii.ac.jp/naid/40020657178
      
    • (URL) http://jssst.or.jp/files/user/taikai/2015/PPL/ppl3-1.pdf
      
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 .
    
    • Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura.
      
    • The 32st Conference of Japan Society for Software Science and Technology (JSSST 2015), PPL6-3, Japan Society for Software Science and Technology, 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 .
    
    • 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 .
    
    • Takehide Soh, Haruki Noritake, Mutsunori Banbara, Naoyuki Tamura and Katsumi Inoue.
      
    • The 31st Conference of Japan Society for Software Science and Technology (JSSST 2014), PPL2-3, Japan Society for Software Science and Technology, 2014.
      
    • (URL) https://ci.nii.ac.jp/naid/40020581916
      
    • (URL) http://jssst.or.jp/files/user/taikai/2014/PPL/PPL2-3.pdf
      
21. Solving Numberlink by a SAT-based Constraint Solver .
    
    • Naoyuki Tamura, Takehide Soh, Mutsunori Banbara and Hidetomo Nabeshima.
      
    • DA Symposium 2014, DA2014-7B-2, pp.215-220, IPSJ SIG-SLDM, Information Processing Society of Japan, 2014
      
    • (URL) https://ci.nii.ac.jp/naid/170000084795
      
    • (URL) http://id.nii.ac.jp/1001/00102757/
      
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.
    
    • Haruki Noritake, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, and Katsumi Inoue.
      
    • The 15th JSSST Workshop on Programming and Programming Languages (PPL 2013), C1 category, Japan Society for Software Science and Technology, 2013.
      
    • (URL) http://www.pllab.riec.tohoku.ac.jp/ppl2013/timetable-without-abstract.html
      
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.
      
    • (DOI) https://www.thinkmind.org/index.php?view=article&articleid=lifsci_v4_n34_2012_8
      
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.
      
    • (DOI) https://www.thinkmind.org/index.php?view=article&articleid=biotechno_2012_1_30_50068
      
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
    
    • Takehide Soh and Katsumi Inoue
      
    • The 24th Annual Conference on Japanese Society of Artificial Intelligence (JSAI 2010), Nagasaki, Japan, 2010.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2010.0_1E13
      
32. Analyzing Pathways through a Translation into SAT Problems
    
    • Takehide Soh and Katsumi Inoue
      
    • The 23th Annual Conference on Japanese Society of Artificial Intelligence (JSAI 2009), Takamatsu, Japan, 2009.
      
    • (DOI) https://doi.org/10.11517/pjsai.JSAI2009.0_2H33
      
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
   
   • Naoyuki Tamura, Mutsunori Banbara, Katsutoshi Hirayama, Takehide Soh
     
   • Computer Software, 30(1):16-19, 2013
     
   • (DOI) https://doi.org/10.11309/jssst.30.1_16
     
6. My Bookmark: SAT Solver
   
   • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
     
   • Journal of Japanese Society for Artificial Intelligence, 28(2):343-348, March 2013
     
   • (URL) https://www.ai-gakkai.or.jp/my-bookmark_vol28-no2/
     

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
   
   • Takehide Soh
     
   • School of Multidisciplinary Sciences, The Graduate University for Advanced Studies, Japan, 125 pages
     
   • (URL) http://id.nii.ac.jp/1013/00002566/