SEARCH

Search Details

SOH Takehide
Information infrastructure and Digital Transformation Initiatives Headquarter
Associate Professor

Researcher basic information

■ Research Keyword
  • 充足可能性判定
  • SAT
  • 制約充足
  • 制約最適化
  • システム生物学
  • 充足可能性判定問題
  • 命題論理
  • ドメイン特化言語
  • 推論技術
  • SAT技術
  • ハミルトン閉路問題
  • 動的制約
  • フランス
  • 国際情報交換
  • 制約プログラミング
■ Research Areas
  • Informatics / Software
  • Informatics / Information theory
  • Informatics / Biological, health, and medical informatics
  • Informatics / Intelligent informatics

Research activity information

■ Award
  • Aug. 2022 XCSP3 Competition Organization, 2022 XCSP3 Competition Sequential CSP Solver track 2nd place, Fun-sCOP
    Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura

  • 02 Oct. 2019 XCSP3 Competition Organization, 2019 XCSP3 Competition Sequential CSP Solver 2nd Place, Fun-sCOP
    Takehide Soh, Daniel Le Berre, Hidetomo Nabesima, Mutsunori Banbara, Naoyuki Tamura
    International society

  • 29 Aug. 2019 Japan Society for Software Science and Technology, 7th Best Review Paper Award (2018), SAT-based Constraint Programming Systems and Related Technologies
    Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    Japan society

  • 2019 The Japanese Society for Artificial Intelligence, JSAI Annual Conference Award 2019, A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition
    Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    Japan society

  • Sep. 2018 情報処理学会, 情報処理学会 2018 年度特選論文, SAT技術を用いたペトリネットのデッドロック検出手法の提案
    寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
    Japan society

  • Aug. 2018 XCSP3 Competition Organization, 2018 XCSP3 Competition 2部門優勝 (逐次CSPソルバー部門, 並列CSPソルバー部門), sCOP
    Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    International society

  • Mar. 2017 日本ソフトウェア科学会 プログラミング論研究会, PPL2017発表賞（一般の部）, SATソルバーの最新動向と利用技術
    SOH TAKEHIDE, TAMURA NAOYUKI
    Official journal

  • Mar. 2017 人工知能学会, 2016年度全国大会優秀賞, SAT型制約ソルバーによるナンバーリンクの解法とその評価
    迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
    Japan society

  • Mar. 2016 日本ソフトウェア科学会, 第20回研究論文賞, パッキング配列問題の制約モデリングとSAT符号化
    則武 治樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳
    Official journal

  • Aug. 2015 情報処理学会DAシンポジウム2015, 最優秀賞, SAT型制約ソルバーを用いたナンバーリンクの求解と解の最適化
    迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知

  • Aug. 2015 情報処理学会 SLDM研究会, アルゴリズムデザインコンテスト2015 最優秀賞 (DAシンポジウム2015), iSugar+GlueMiniSat
    迫 龍哉, 川原 征大, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE, 鍋島 英知
    Japan society

  • Sep. 2014 日本ソフトウェア科学会, 第31回大会高橋奨励賞, Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
    SOH TAKEHIDE
    Japan society

  • Aug. 2014 情報処理学会 SLDM研究会, アルゴリズムデザインコンテスト2014 最優秀賞 (DAシンポジウム2014・SWEST16), Sugar+GlueMiniSat
    TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI, 鍋島 英知
    Japan society

  • Aug. 2014 情報処理学会DAシンポジウム2014, アルゴリズムデザインコンテスト2014 最優秀賞, SAT型制約ソルバーを用いたナンバーリンクの解法
    田村直之, 宋剛秀, 番原睦則, 鍋島英知

  • Apr. 2010 総合研究大学院大学, 学長賞, SATとASPを用いた生物学におけるパスウェイの解析
    SOH TAKEHIDE
    Others

  • Sep. 2009 人工知能学会, ２００９年度全国大会優秀賞, Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
    SOH TAKEHIDE
    Japan society

■ Paper
  • Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
    2025

  • Takehide Soh, Tomoya Tanjo, Yoshio Okamoto, Takehiro Ito
    In this extended abstract, we describe CoRe Challenge 2022/2023, an international competition series aiming to construct the technical foundation of practical research for Combinatorial Reconfiguration. This competition series targets one of the most well-studied reconfiguration problems, called the independent set reconfiguration problem under the token jumping model, which asks a step-by-step transformation between two given independent sets in a graph. Theoretically, the problem is PSPACE-complete, which implies that there exist instances such that even a shortest transformation requires super-polynomial steps with respect to the input size under the assumption of $NP \neq PSPACE$. The competition series consists of four tracks: three tracks take two independent sets of a graph as input, and ask the existence of a transformation, a shortest transformation, a longest transformation between them; and the last track takes only a number of vertices as input, and asks for an instance of the specified number of vertices that needs a longer shortest transformation steps. We describe the background of the competition series and highlight the results of the solver and graph tracks.
    Association for the Advancement of Artificial Intelligence (AAAI), Jun. 2024, Proceedings of the International Symposium on Combinatorial Search, 17, 285 - 286
    Scientific journal

  • Takehide Soh, Takumu Watanabe, Jun Kawahara, Akira Suzuki, Takehiro Ito
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, 22nd International Symposium on Experimental Algorithms(SEA), 26 - 15
    International conference proceedings

  • Takahiro Hirate, Mutsunori Banbara, Katsumi Inoue, Xiao-Nan Lu, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    Springer, Sep. 2023, In: S. Gaggl et al. (eds.), Logics in Artificial Intelligence, Proceedings of the 18th European Conference (JELIA 2023), Lecture Notes in Artificial Intelligence, 14281, to appear - 16p., English, International magazine, Co-authored internationally
    [Refereed]
    International conference proceedings

  • Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    Lead, SCITEPRESS - Science and Technology Publications, Mar. 2023, Proceedings of the 16th International Joint Conference on Biomedical Engineering Systems and Technologies, 163 - 174
    [Refereed]
    International conference proceedings

  • Takahisa Toda, Takehiro Ito, Jun Kawahara, Takehide Soh, Akira Suzuki, Junichi Teruyama
    IEEE, 2023, 35th IEEE International Conference on Tools with Artificial Intelligence(ICTAI), 294 - 302
    International conference proceedings

  • Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    2023
    [Refereed]
    Link to Kobe Univ. Repository (Kernel)

  • Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
    2023, CPAIOR, 167 - 183
    [Refereed]
    International conference proceedings

  • Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama, Takahisa Toda
    Dec. 2022, CoRR, abs/2207.13959
    [Refereed]
    Scientific journal

  • Takehide Soh, Yoshio Okamoto, Takehiro Ito
    Sep. 2022, CoRR, abs/2208.02495
    Scientific journal

  • 解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価
    桑原和也, 宋剛秀, 田村直之, 番原睦則
    Mar. 2022, 情報処理学会第84回全国大会講演論文集, Japanese
    Research institution

  • チャネリング制約を用いた alldifferent 制約の SAT 符号化
    小菅脩司, 宋剛秀, 田村直之, 番原睦則
    Mar. 2022, 情報処理学会第84回全国大会講演論文集, Japanese
    Symposium

  • 有界モデル検査による独立集合遷移問題の解法に関する考察
    戸田 貴久, 伊藤 健洋, 川原 純, 宋 剛秀, 鈴木 顕, 照山 順一
    Jan. 2022, 情報処理学会 研究報告アルゴリズム（AL）, 2022-AL-186(5) (5), 1 - 7, Japanese
    Symposium

  • Towards CEGAR-based Parallel SAT Solving
    Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue
    Lead, Jul. 2021, Pragmatics of SAT 2021, English
    [Refereed]
    Research society

  • Studies on a Parallelization Method of SAT-based CSP Solvers using CEGAR and the Share of Counterexamples
    宋 剛秀, 鍋島 英知, 番原 睦則, 田村 直之, 井上 克巳
    人工知能学会, Mar. 2020, 人工知能基本問題研究会, 112, 6 - 11, Japanese

  • IINO Naoki, TAMURA Naoyuki, SOH Takehide, BANBARA Mutsunori, INOUE Katsumi

    In this paper, we propose a new method for testing satisfiability of the given formula in propositional modal logic K. The proposed way is based on a tableau method and implemented in answer set programming. In previous tableau based solvers, such as Km2SAT and InKreSAT, the satisfiability is tested after creating all possible worlds initially, or it is tested repeatedly by incrementally extending the possible worlds with a breadth-first strategy. The proposal introduces a new way to extend the possible worlds incrementally with a heuristic function in addition to these two previous methods. By using appropriate heuristics, it is expected to search an unsatisfiable possible world first, and will improve the testing performance. We evaluated the proposed method with a standard benchmark set LWB and found the proposal was superior to the existing methods in some benchmark class when the length of the given formula is used as the heuristic function.

    The Japanese Society for Artificial Intelligence, 2020, Proceedings of the Annual Conference of JSAI, 2020(0) (0), 2N5OS17b05 - 2N5OS17b05, Japanese
    Symposium

  • 大野周亮, 番原睦則, SOH TAKEHIDE, TAMURA NAOYUKI
    人工知能学会, Mar. 2019, 人工知能学会研究会資料, SIG-FPAI-B803, 6 - 11, Japanese
    Research society

  • Solver Description of Fun-sCOP
    Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura
    2019, Solver Descriptions of XCSP3 Competition 2019 (XCSP19), 1 - 2, English
    Research society

  • Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    Springer, 2019, Annals OR, 275(1) (1), 3 - 37, English
    [Refereed]
    Scientific journal

  • SOH Takehide, BERRE Daniel Le, BANBARA Mutsunori, TAMURA Naoyuki

    Constraint Satisfaction Problem (CSP) is the combinatorial problem of finding a variable assignment which satisfies all given constraints over finite domains. CSP has a wide range of applications in the research domains of Artificial Intelligence and Operations Research. XCSP3 is one of the major constraint languages that can describe CSPs. More than 23,000 instances over 105 series are available in the XCSP3 database. In 2018, the international XCSP3 competition was held and 18 solvers participated. This paper describes the under development CSP solver sCOP and its results on the 2018 XCSP3 competition. sCOP is a SAT-based solver which encodes CSPs into SAT problems and finds a solution using SAT solvers. Currently, sCOP equips the order and log encodings, and uses off-the-shelves backend SAT solvers. We registered sCOP to two competition tracks CSP-Standard-Sequential and CSP-Standard-Parallel of the 2018 XCSP3 competition and won both tracks.

    The Japanese Society for Artificial Intelligence, 2019, Proceedings of the Annual Conference of JSAI, 2019(0) (0), 1E2OS3a03 - 1E2OS3a03, Japanese
    Research society

  • Proposal of SAT-based Method to Detect Deadlock of Petri Nets
    寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
    In this paper, we propose a SAT-based method to detect deadlock of general Petri nets in which more than one tokens are allowed for each place. In our approach, the transition relation of a Petri net is represented as constraints on integers and they are translated into SAT by order encoding, so that the deadlock of general Petri nets can be detected by a SAT solver, while existing SAT-based methods cannot be applied for them. Furthermore, in order to improve the performance, we introduced multiple firing model, which can detect deadlock with shorter steps than the model used in an existing SAT-based method, called successive firing model. We evaluated the successive firing model and the multiple firing model through a benchmark set of Model Checking Contest 2017. The multiple firing model showed better performance for almost all instances, and was especially effective for the instances in which there are many tokens at the initial marking. Through the comparison with the winner tool LoLA and the second place tool Tapaal of the contest, although the number of detected deadlocks are fewer than LoLA and Tapaal, we confirmed the effectiveness of the proposed method with some instances for which all tools including LoLA and Tapaal failed to detect deadlock.
    情報処理学会, Sep. 2018, 情報処理学会論文誌, 59(9) (9), 1749 - 1760, Japanese
    Link to Kobe Univ. Repository (Kernel)

  • 南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    本論文では，擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として，ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する．提案手法は，次の3つの特徴を持つ． 1つ目は，SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である． 2つ目は，同じ解を持つ同値なPB制約であれば係数や右辺の値が異なっても，同一の中間表現およびSAT問題に符号化可能な点である． 3つ目は，項数に対して係数の種類が少ないPB制約に対しては，中間表現が簡潔になり少ない節数でSAT符号化可能な点である．このようなPB制約は，国際PBソルバー競技会のベンチマーク問題にも頻出している．計算機実験では，代表的な既存手法で一般化アーク整合性維持が可能なBDD法，およびそれより弱い整合性検査が可能なSorter法と符号化後の節数と求解性能を比較した．結果として，異なる係数の種類が10%以下であるようなPB制約について，提案手法が節数と求解性能に関して比較した2手法よりも良いことを確認した． / In this paper, we propose a new encoding method for a set of PB (Pseudo-Boolean) constraints into propositional satisfiability (SAT) problems, in which Boolean Cardinality (BC) constraints are used as an intermediate form. The proposed method has the following three features. First, it can maintain general arc consistency by unit propagation of a SAT solver. Second, it can encode equivalent PB constraints with the same solutions—even their coefficients and right hand side value are different—into the same intermediate form and SAT instance. Third, for PB constraints whose number of kinds of coefficients is relatively small compared with the number of terms, the intermediate form becomes simpler and they can be encoded with a small number of clauses. Such PB constraints often appear in international PB solver competition benchmarks. In experiments, we compared the proposed encoding method with existing methods, BDD and Sorter. The former maintains general arc consistency by unit propagation, while the later maintains consistency checking that is weaker than general arc consistency. As the result, for PB constraints in which the number of different coefficients is not more than 10%, we confirmed that the proposed method is better than those two methods in terms of the number of encoded clauses and the efficiency in solver performance.
    日本ソフトウェア科学会, Aug. 2018, コンピュータソフトウェア, 35(3) (3), 65 - 78, Japanese
    [Refereed]
    Scientific journal
    Link to Kobe Univ. Repository (Kernel)

  • sCOP: SAT-based Constraint Programming System
    Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
    2018, Solver Descriptions of XCSP3 Competition 2018 (XCSP18), 1 - 2, English
    Research society

  • SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki, NABESHIMA Hidetomo

    Since 2000, SAT solvers that are programs solving SAT instances has enormously progressed in performance. Due to the performance improvement, SAT-based systems that encode problems into SAT instances and solve them by SAT solvers have succeeded in various research fields such as planning, software/hardware verification, scheduling problems, etc .In this paper, as recent advances in SAT solvers, we first explain the progress of their performance and functions from the viewpoint of the international competition of SAT solvers which is a factor of their progress. Then, from the viewpoint of utilization technologies, we explain that we can solve more complex problems by combining progressive functions of SAT solvers with encoding methods. As an example, we explain a solving method for the multiobjective optimization problems by using SAT solvers.

    Japan Society for Software Science and Technology, 2018, Computer Software, 35(4) (4), 72 - 92, Japanese
    [Refereed]
    Link to Kobe Univ. Repository (Kernel)

  • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints
    南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    日本ソフトウェア科学会, Sep. 2017, 日本ソフトウェア科学会第34回大会講演論文集, 34, 393 - 404, Japanese
    Symposium

  • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    Feb. 2017, INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS, 26(1) (1), English
    [Refereed]
    Scientific journal
    Link to Kobe Univ. Repository (Kernel)

  • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    World Scientific Publishing, Feb. 2017, International Journal on Artificial Intelligence Tools, 26(1) (1), 1 - 29, English
    [Refereed]
    Scientific journal
    Link to Kobe Univ. Repository (Kernel)

  • MINAMI Yushi, SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki
    The Japanese Society for Artificial Intelligence, 2017, JSAI Technical Report, SIG-FPAI, 103, 4 - 4, Japanese

  • 寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI

    本稿ではSAT技術を用いたペトリネットのデッドロック検出手法について述べる．まず，トークン数や多重度が整数値のペトリネットの制約モデルを提案し，次に，検証するステップ長が短くなるように制約モデルを改良する．また，マーキングインバリアントを用いて，トークン数の上限を求める方法について述べる．最後に計算機実験で提案手法の有効性を評価する．

    日本ソフトウェア科学会, 2017, 日本ソフトウェア科学会第33回大会講演論文集, 2017(0) (0), 1M1OS02a2 - 1M1OS02a2, Japanese
    Symposium

  • 坡山 直樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI

    解集合プログラミング(ASP)言語は一階論理に基づく表現力の高いモデリング言語である．ASPソルバーは安定モデル意味論に基づいた解集合を求める．近年，SAT 技術を応用した高速 ASP ソルバーが実現され，人工知能分野への実用的応用が急速に拡大している．本研究では，高速な ASP 型制約ソルバーの実現に向けて，制約充足問題から ASP への符号化の設計・実装・評価を行う．

    人工知能学会, 2017, 2017年度人工知能学会全国大会(第31回)論文集, 2017(0) (0), 1M1OS02a4 - 1M1OS02a4, Japanese
    Symposium

  • 解集合プログラミングによるカリキュラムベース・コース時間割編成
    BANBARA MUTSUNORI, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, SOH TAKEHIDE, TAMURA NAOYUKI, フィリップ ワンコ
    日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017, 第29回RAMPシンポジウム論文集, 73 - 88, Japanese
    [Invited]
    Symposium

  • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Daniel Le Berre
    Springer, 2017, Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017), 10416, 596 - 614, English
    [Refereed]
    International conference proceedings

  • 寸田 智也, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI

    本稿ではSAT技術を用いたペトリネットのデッドロック検出手法について述べる．まず，トークン数や多重度が整数値のペトリネットの制約モデルを提案し，次に，検証するステップ長が短くなるように制約モデルを改良する．また，マーキングインバリアントを用いて，トークン数の上限を求める方法について述べる．最後に計算機実験で提案手法の有効性を評価する．

    人工知能学会, 2017, 2017年度人工知能学会全国大会(第31回)論文集, 2017(0) (0), 1M1OS02a2 - 1M1OS02a2, Japanese
    Symposium

  • ブール基数制約を経由した擬似ブール制約のSAT符号化法
    南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    人工知能学会, Jan. 2017, 人工知能学会研究会資料, 18 - 23, Japanese
    Symposium

  • SATソルバーの使い方 —問題をSATに符号化する方法—
    TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI
    情報処理学会, Jan. 2017, 第58回プログラミング・シンポジウム予稿集, 165 - 172, Japanese
    Symposium

  • Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー
    SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    情報処理学会, Jan. 2017, 第58回プログラミング・シンポジウム予稿集, 71 - 74, Japanese
    Symposium

  • Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    Springer, 2017, The 14th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR-17), 265 - 278, English
    [Refereed]
    International conference proceedings

  • SOH Takehide, BANBARA Mutsunori, TAMURA Naoyuki
    In recent years, the performance of SAT solvers have been enormously improved and its applications are enlarged in various domains. However, SAT solvers are not adequate to directly solve problems such as the one including arithmetic constraints which has many realistic applications since the input of SAT solvers is propositional formulae of conjunction normal form. Therefore, there have been researches for systems extending and/or utilizing SAT solvers so that these can adopt more rich expressions. In this paper, we explain one of such systems—SAT-based constraint programming systems which are the integration of the performance of SAT solvers and the rich expressions of constraint programming systems. We also briefly explain related technologies of SAT-based constraint programming systems.
    Japan Society for Software Science and Technology, 2017, Computer Software, 34(1) (1), 1_67 - 1_80, Japanese
    [Refereed]

  • An incremental SAT solving library and its applications
    Tatsuya Sako, Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Hidetomo Nabeshima, Katsumi Inoue
    Nov. 2016, Computer Software, 33(4) (4), 16 - 29
    [Refereed]
    Scientific journal

  • Takahisa Toda, Takehide Soh
    Association for Computing Machinery, Oct. 2016, ACM Journal of Experimental Algorithmics, 21(1) (1), 1 - 44, English
    [Refereed]
    Scientific journal

  • 迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知, 井上 克巳
    日本ソフトウェア科学会, Jul. 2016, コンピュータソフトウェア, 33(4) (4), 16 - 29, Japanese
    [Refereed]
    Scientific journal

  • Solving Optimal Software Component Configuration Problem in Cloud
    TAMURA NAOYUKI, 井上 克巳, 鍋島 英知, BANBARA MUTSUNORI, SOH TAKEHIDE
    人工知能学会, Mar. 2016, 人工知能基本問題研究会(第100回), 100, 19 - 24, Japanese

  • 解集合プログラミングを用いた制約組合せテストケース生成
    兼行 大将, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳, 沖本 天太
    Mar. 2016, 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016), カテゴリC1, Japanese
    [Refereed]
    Symposium

  • 分子ネットワーク上の状態推定とその可視化による知識発見支援
    平沼 祐人, 山本 泰生, 守屋 央朗, SOH TAKEHIDE, 岩沼 宏治
    情報処理学会, Mar. 2016, 第45回バイオ情報学研究発表会, 11, 1 - 6, Japanese
    Symposium

  • SATソルバーを用いた制約プログラミングシステムとその応用
    SOH TAKEHIDE
    情報処理学会, Jan. 2016, 第57回プログラミング・シンポジウム, 1 - 10, Japanese
    Symposium

  • 迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
    人工知能学会, 2016, 2016年度人工知能学会全国大会(第30回)論文集, 2016(0) (0), 1D4OS02a3 - 1D4OS02a3, Japanese
    Symposium

  • 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    人工知能学会, 2016, 2016年度人工知能学会全国大会(第30回)論文集, 2016(0) (0), 1D4OS02a4 - 1D4OS02a4, Japanese
    Symposium

  • 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
    International Conference on the Practice and Theory of Automated Timetabling, 2016, PATAT 2016 - Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling, 13 - 32, English
    [Refereed]
    International conference proceedings

  • 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
    SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    日本ソフトウェア科学会, Sep. 2015, 日本ソフトウェア科学会第32回大会, 1 - 11, Japanese
    Symposium

  • Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
    SOH TAKEHIDE, 馬場 知哉
    日本ソフトウェア科学会, Sep. 2015, 日本ソフトウェア科学会第32回大会, 1 - 8, Japanese
    Symposium

  • SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
    川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    日本ソフトウェア科学会, Sep. 2015, 日本ソフトウェア科学会第32回大会, 32, 1 - 9, Japanese
    Symposium

  • iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
    迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知, 井上 克巳
    日本ソフトウェア科学会, Sep. 2015, 日本ソフトウェア科学会第32回大会, 1 - 12, Japanese
    Symposium

  • 制約充足問題のハイブリッド符号化に向けて
    SOH TAKEHIDE, 佐古田 淳史, BANBARA MUTSUNORI, TAMURA NAOYUKI
    人工知能学会, Mar. 2015, 第第97回人工知能基本問題研究会．人工知能学会研究会資料, 65 - 73, Japanese
    Symposium

  • Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
    Springer, 2015, CoRR, abs/1312.6113, 112 - 126
    [Refereed]
    International conference proceedings

  • Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
    Springer, 2015, Proceedings of the Sixth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2013), 112 - 126, English
    [Refereed]
    International conference proceedings

  • Takahisa Toda, Takehide Soh
    2015, CoRR, abs/1510.00523
    [Refereed]

  • Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
    Springer, 2015, Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, Lexington, KY, USA, September 27-30, 2015. Proceedings, 9345, 112 - 126
    [Refereed]
    International conference proceedings

  • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    2015, 2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015), 2016-January, 421 - 428, English
    [Refereed]
    International conference proceedings

  • 兼行 大将, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳

    制約解集合プログラミング(CASP;Constraint Answer Set Programming)は，解集合プログラミングと制約プログラミングを融合した新しいプログラミングパラダイムである．近年，SAT技術を応用した高速なCASPソルバが開発され，注目を集めている．本研究では，組合せテストケース生成問題に対して，制約充足問題としての定式化およびCASP符号化を提案し，その有効性を検証する．

    人工知能学会, 2015, 2015年度人工知能学会全国大会, 2015(0) (0), 2H5OS03b5 - 2H5OS03b5, Japanese
    Symposium

  • Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Matthias Weise
    Springer, 2015, Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015), 112 - 126, English
    [Refereed]
    International conference proceedings

  • Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    2015, 2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015), 421 - 428, English
    [Refereed]
    International conference proceedings

  • 制約解集合プログラミングシステムの設計方式に関する考察
    SOH TAKEHIDE, 則武 治樹, BANBARA MUTSUNORI, TAMURA NAOYUKI, 井上 克巳
    日本ソフトウェア科学会, Sep. 2014, 日本ソフトウェア科学会第31回大会講演論文集, 1 - 15, Japanese
    Symposium

  • Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
    SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    日本ソフトウェア科学会, Sep. 2014, 日本ソフトウェア科学会第31回大会講演論文集, 1 - 15, Japanese
    Symposium

  • Solving Numberlink by a SAT-based Constraint Solver
    TAMURA NAOYUKI, SOH TAKEHIDE, BANBARA MUTSUNORI, 鍋島 英知
    情報処理学会システムとLSIの設計技術研究会, Aug. 2014, DAシンポジウム2014論文集, 2014(2014) (2014), 215 - 220, Japanese

  • 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
    Jul. 2014, Proceedings of the 5th International Workshop on Pragmatics of SAT (PoS 2014), 1 - 12, English
    International conference proceedings

  • 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
    佐古田 淳史, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    人工知能学会, May 2014, 第28回人工知能学会全国大会論文集, 1 - 4, Japanese
    Symposium

  • Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura
    2014, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, 684 - 693
    [Refereed]
    Scientific journal

  • SOH TAKEHIDE, Daniel Le Berre, Stéphanie Roussel, BANBARA MUTSUNORI, TAMURA NAOYUKI

    近年のSAT技術の進歩に伴い，SAT型制約プログラミングシステムが成功をおさ めいる．しかし従来のシステムではSATソルバーとの通信手段がCNFファイルや 基本的なAPIに限定されており，SATソルバーとの密接な連携が困難であった． 本研究ではSATソルバーと密に結合された制約プログラミングシステムScarabの提案を行う．またハミルトン閉路問題への応用を示し，その有効性の評価を行う．

    人工知能学会, 2014, 第28回人工知能学会全国大会論文集, 2014(0) (0), 1D5OS11b6i - 1D5OS11b6i, Japanese
    Symposium

  • Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
    Takehide Soh, Daniel Le Berre, Stephanie Roussel, Mutsunori Banbara, Naoyuki Tamura
    2014, LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2014, 8761, 684 - 693, English
    [Refereed]
    International conference proceedings

  • Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
    IEEE, Nov. 2013, Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013), English
    [Refereed]
    International conference proceedings

  • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
    Jul. 2013, THEORY AND PRACTICE OF LOGIC PROGRAMMING, 13(4/5) (4/5), 783 - 798, English
    [Refereed]
    Scientific journal

  • Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
    Cambridge University Press, Jul. 2013, Theory and Practice of Logic Programming, 13(4-5) (4-5), 783 - 798, English
    [Refereed]
    Scientific journal

  • SAT符号化を用いたパッキング配列の構成
    則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
    Mar. 2013, 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集, Japanese
    [Refereed]
    Scientific journal

  • System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems⋆
    Soh, Takehide, Tamura, Naoyuki, Banbara, Mutsunori, Le Berre, Daniel, Roussel, St{\'e}phanie
    2013
    Scientific journal

  • Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
    Springer, 2013, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, 7962, 429 - 436
    [Refereed]
    International conference proceedings

  • Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
    IEEE Computer Society, 2013, 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, Herndon, VA, USA, November 4-6, 2013, 1020 - 1027
    [Refereed]
    International conference proceedings

  • Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
    Springer, 2013, Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), 7962, 429 - 436, English
    [Refereed]
    International conference proceedings

  • Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration
    SOH Takehide, INOUE Katsumi, BABA Tomoya, TAKADA Toyoyuki, SHIROISHI Toshihiko
    Dec. 2012, International Journal On Advances in Life Sciences, 4(3-4):154-165, English
    Scientific journal

  • Encoding Curriculum based Course Timetabling Problems into Pseudo-Boolean Optimization Problems
    鈴江 美奈, 田村 直之, 番原 睦則, 宋 剛秀, 鳩野 逸生
    [日本ソフトウェア科学会], Aug. 2012, 日本ソフトウェア科学会第29回大会講演論文集, 29, 495 - 502, Japanese
    International conference proceedings

  • Predicting Gene Knockout Effects by Minimal Pathway Enumeration
    Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada, Toshihiko Shiroishi
    Mar. 2012, The 4th International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies, 11 - 19, English
    International conference proceedings

  • Oliver Ray, Takehide Soh, Katsumi Inoue
    Springer, 2012, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6479, 167 - 183, English
    [Refereed]
    International conference proceedings

  • Oliver Ray, Takehide Soh, Katsumi Inoue
    Springer, 2012, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6479, 167 - 183, English
    [Refereed]
    International conference proceedings

  • Takehide Soh, Katsumi Inoue
    Japanese Society for Artificial Intelligence, 2012, Transactions of the Japanese Society for Artificial Intelligence, 27(3) (3), 204 - 212, Japanese
    [Refereed]
    Scientific journal

  • Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
    Nov. 2010, Fundamenta Informaticae, 102(3-4): 467-487, English
    [Refereed]
    Scientific journal

  • Finding Minimal Reaction Sets in Large Metabolic Pathways
    Takehide Soh, Katsumi Inoue
    2010, Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010), 54 - 54, English
    [Refereed]
    International conference proceedings

  • Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
    2010, FUNDAMENTA INFORMATICAE, 102(3-4) (3-4), 467 - 487, English
    [Refereed]
    Scientific journal

  • A SAT-based Method for Analyzing Metabolic Pathways
    Takehide Soh, Katsumi Inoue
    2010, Poster presentation at: Systems Biochemistry 2010, English
    [Refereed]
    Symposium

  • (2H3-3)SAT問題への変換を用いたフィードバックを含むパスウェイの解析
    SOH TAKEHIDE, 井上克巳
    Jun. 2009, 人工知能学会全国大会, Japanese
    Symposium

  • Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
    IOS Press, 2009, Jouranal of Algorithms in Cognition, Informatics and Logic, 102(3,4) (3,4), 467 - 487, English
    [Refereed]
    Scientific journal

  • A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
    Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
    Dec. 2008, In Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, English
    [Refereed]
    Scientific journal

  • Katsumi Inoue, Takehide Soh, Seiji Ueda, Yoshito Sasaura, Mutsunori Banbara, Naoyuki Tamura
    Nov. 2006, DISCRETE APPLIED MATHEMATICS, 154(16) (16), 2291 - 2306, English
    [Refereed]
    Scientific journal

  • Lemma Reusing for SAT based Planning and Scheduling
    Hidetomo Nabeshima, Takehide Soh, Katsumi Inoue, Koji Iwanuma
    AAAI Press, 2006, In the proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006), 103 - 112, English
    [Refereed]
    International conference proceedings

  • Experimental results for solving job-shop scheduling problems with multiple SAT solvers
    Takehide Soh, Katsumi Inoue, Mutsunori Banbara, Naoyuki Tamura
    Oct. 2005, Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing (held in conjunction with CP'05), pp.25-38, English
    [Refereed]
    Scientific journal

  • 生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般)
    SOH TAKEHIDE, 井上克巳
    社団法人電子情報通信学会, Jun. 2004, 電子情報通信学会技術研究報告. AI, 人工知能と知識処理, 104(133) (133), 19 - 24, Japanese
    Symposium

  • 高速SATソルバーの原理
    鍋島英知, 宋剛秀
    人工知能学会論文誌(解説論文), 25(1) (1), 68 - 76
    [Refereed]

■ MISC
  • Irumi Sugimori, Katsumi Inoue, Hidetomo Nabeshima, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
    18 May 2024, CoRR, abs/2403.07885, 11p., English, International magazine, Co-authored internationally
    Report scientific journal

  • ハミルトン閉路問題に対するCut-arc集合制約を用いたSAT型CEGAR解法
    大橋瞭雅, 宋剛秀, 鍋島英知, 番原睦則, 井上克巳, 田村直之
    2024, 日本ソフトウェア科学会大会講演論文集(Web), 41st

  • 独立集合遷移問題に対する有界組合せ遷移の改良に関する一考察
    桑原祥文, 宋剛秀, 盧暁南, 鍋島英知, 番原睦則, 井上克巳, 田村直之
    2024, 日本ソフトウェア科学会大会講演論文集(Web), 41st

  • ZDDを用いた組合せ遷移ソルバー
    伊藤健洋, 川原純, 中畑裕, 宋剛秀, 鈴木顕, 照山順一, 戸田貴久
    2022, 日本オペレーションズ・リサーチ学会秋季研究発表会アブストラクト集, 2022

  • CDCL型SATソルバーの内部動作可視化ツール
    堀岡真未, 宋剛秀, 田村直之
    Sep. 2021, 日本ソフトウェア科学会第38回大会ポスター発表, Japanese
    Others

  • ライフゲームを逆向きに動かす
    足立啓一, 宋剛秀, 田村直之
    Sep. 2021, 日本ソフトウェア科学会第38回大会ポスター発表, Japanese
    Others

  • SATソルバーを用いた一層平面配置配線問題の解法に関する考察
    三嶋哲平, 宋剛秀, 田村直之
    Sep. 2020, 日本ソフトウェア科学会第37回大会ポスター発表, Japanese
    Others

  • SAT Evolution and Applications：2. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver -
    田村 直之, 宋 剛秀, 番原 睦則
    数独やナンバーリンクなどのパズルを題材として取り上げ，SATソルバーを用いてこれらのパズルを解く方法について説明する．SATソルバーは，与えられた連言標準形の命題論理式（CNF式）を満たす解を探索するプログラムである．近年になって大幅な性能向上が実現され，最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている．このことを背景とし，さまざまな問題をCNF式に変換（符号化） しSAT ソルバーで解を求める手法が注目を集めている．本稿では，パズルを題材とすることで，この手法について分かりやすく解説する．
    情報処理学会 ; 1960-, 15 Jul. 2016, 情報処理, 57(8) (8), 710 - 715, Japanese

  • 制約充足問題のハイブリッド符号化に向けて
    SO TAKEHIDE, SAKODA ATSUSHI, BAMBARA MUTSUNORI, TAMURA NAOYUKI
    18 Mar. 2015, 人工知能学会人工知能基本問題研究会資料, 97th, 65 - 73, Japanese

  • KANEYUKI HIROMASA, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI

    制約解集合プログラミング(CASP;Constraint Answer Set Programming)は，解集合プログラミングと制約プログラミングを融合した新しいプログラミングパラダイムである．近年，SAT技術を応用した高速なCASPソルバが開発され，注目を集めている．本研究では，組合せテストケース生成問題に対して，制約充足問題としての定式化およびCASP符号化を提案し，その有効性を検証する．

    一般社団法人 人工知能学会, 2015, 人工知能学会全国大会論文集(CD-ROM), 2015(0) (0), 2H5OS03b5 - 2H5OS03b5, Japanese

  • 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
    宋剛秀, 番原睦則, 田村直之
    2015, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL6-3, Japanese

  • Scala上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
    宋剛秀, 馬場知哉
    2015, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.SOFUTOWEA1, Japanese

  • SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
    川原征大, 宋剛秀, 番原睦則, 田村直之
    2015, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL3-1, Japanese

  • iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
    迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    2015, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL6-1, Japanese

  • Studies on a Design of Constraint Answer Set Programming Systems
    宋 剛秀, 則武 治樹, 番原 睦則
    [日本ソフトウェア科学会], 07 Sep. 2014, 日本ソフトウェア科学会大会論文集, 31, 140 - 154, Japanese

  • Prototyping Tool for SAT-based Constraint Programming Systems in Scala
    宋 剛秀, 番原 睦則, 田村 直之
    [日本ソフトウェア科学会], 07 Sep. 2014, 日本ソフトウェア科学会大会論文集, 31, 217 - 231, Japanese

  • Solving Post-Enrollment Course Timetabling using Cardinality Constraint and SAT Solvers
    佐古田 淳史, 宋 剛秀, 番原 睦則
    人工知能学会, 2014, 人工知能学会全国大会論文集, 28, 1 - 4, Japanese

  • 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
    SAKODA ATSUSHI, SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
    2014, 人工知能学会全国大会論文集(CD-ROM), 28th, ROMBUNNO.1D5-OS-11B-7, Japanese

  • 制約解集合プログラミングシステムの設計方式に関する考察
    SO TAKEHIDE, NORITAKE HARUKI, BAMBARA MUTSUNORI, TAMURA NAOYUKI, INOUE KATSUMI
    2014, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 31st, ROMBUNNO.PPL2-3, Japanese

  • NORITAKE HARUKI, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI
    日本ソフトウェア科学会, 2014, コンピュータソフトウェア, 31(1) (1), 116 - 130, Japanese
    Link to Kobe Univ. Repository (Kernel)

  • Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
    SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI
    2014, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 31st, ROMBUNNO.SOFUTO1-1, Japanese

  • SO TAKEHIDE, LE BERRE DANIEL, ROUSSEL STEPHANIE, BAMBARA MUTSUNORI, TAMURA NAOYUKI

    近年のSAT技術の進歩に伴い，SAT型制約プログラミングシステムが成功をおさ めいる．しかし従来のシステムではSATソルバーとの通信手段がCNFファイルや 基本的なAPIに限定されており，SATソルバーとの密接な連携が困難であった． 本研究ではSATソルバーと密に結合された制約プログラミングシステムScarabの提案を行う．またハミルトン閉路問題への応用を示し，その有効性の評価を行う．

    一般社団法人 人工知能学会, 2014, 人工知能学会全国大会論文集(CD-ROM), 2014(0) (0), 1D5OS11b6i - 1D5OS11b6i, Japanese

  • Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
    SOH Takehide, LE BERRE Daniel, ROUSSEL Stephanie, BANBARA Mutsunori, TAMURA Naoyuki
    2014, Lect Notes Comput Sci, 8761, 684 - 693, English

  • Constraint Modeling and SAT Encoding of the Packing Array Problem
    則武 治樹, 番原 睦則, 宋 剛秀
    [日本ソフトウェア科学会], 10 Sep. 2013, 日本ソフトウェア科学会大会論文集, 30, 79 - 92, Japanese

  • Scarab : A Prototyping Tool for SAT-based Constraint Programming Systems in Scala
    宋 剛秀, 番原 睦則, 田村 直之
    [日本ソフトウェア科学会], 10 Sep. 2013, 日本ソフトウェア科学会大会論文集, 30, 237 - 245, Japanese

  • BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI, SCHAUB TORSTEN
    Jul. 2013, Theor Pract Log Program, 13(4/5) (4/5), 783 - 798, English

  • SAT Solvers(My Bookmark)
    BANBARA Mutsunori, SOH Takehide, TAMURA Naoyuki, INOUE Katsumi, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
    人工知能学会, 01 Mar. 2013, 人工知能学会誌, 28(2) (2), 343 - 348, Japanese
    Others

  • SAT Solvers(My Bookmark)
    BANBARA Mutsunori, SOH Takehide, TAMURA Naoyuki, INOUE Katsumi, Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue
    The Japanese Society for Artificial Intelligence, 01 Mar. 2013, Journal of Japanese Society for Artificial Intelligence, 28(2) (2), 343 - 348, Japanese

  • TAMURA Naoyuki, BANBARA Mutsunori, HIRAYAMA Katsutoshi, SOH Takehide
    Japan Society for Software Science and Technology, 25 Jan. 2013, Computer Software, 30(1) (1), 16 - 19, Japanese

  • SAKODA ATSUSHI, SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI

    近年，命題論理の充足可能性判定問題(SAT)を非常に高速に解くことが可能なSATソルバーが実現され，SAT技術を多分野に応用する研究が急速に拡大している．本研究では，詰込み問題の一つである正方形詰込み問題に対して，制約充足問題としての定式化及びSAT符号化を用いた解法を提案し，その有効性を検証する．

    一般社団法人 人工知能学会, 2013, 人工知能学会全国大会論文集(CD-ROM), 2013(0) (0), 2E5OS09b1 - 2E5OS09b1, Japanese

  • パッキング配列問題の制約モデリングとSAT符号化
    NORITAKE HARUKI, BAMBARA MUTSUNORI, SO TAKEHIDE, TAMURA NAOYUKI, INOUE KATSUMI
    2013, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 30th, 79 - 92, Japanese

  • Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
    SO TAKEHIDE, BAMBARA MUTSUNORI, TAMURA NAOYUKI, LE BERRE DANIEL, ROUSSEL STEPHANIE
    2013, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 30th, 237 - 245, Japanese

  • Predicting Gene Knockout Effects on E. coli by Minimal Active Pathway Enumeration
    SOH Takehide, INOUE Katsumi, BABA Tomoya, TAKADA Toyoyuki, SHIROISHI Toshihiko
    15 Feb. 2012, 情報処理学会研究報告(CD-ROM), 2011(5) (5), ROMBUNNO.ICS-165,NO.7, English

  • Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems(Foundations of AI,Doctorial Theses on Aritificial Intelligence)
    宋 剛秀
    The Japanese Society for Artificial Intelligence, 01 Jan. 2012, Journal of Japanese Society for Artificial Intelligence, 27(1) (1), 84 - 84, Japanese

  • 高速SATソルバーの原理
    鍋島英知, SOH TAKEHIDE
    人工知能学会, 2010, 人工知能学会論文誌(解説論文), 25(1) (1), 68 - 76, Japanese
    [Refereed]
    Introduction scientific journal

  • Finding Minimal Sub-pathways in Metabolic Pathways by Model Generation
    宋 剛秀, 井上 克巳
    人工知能学会, 2010, 人工知能学会全国大会論文集, 24, 1 - 4, Japanese

  • Takehide Soh, Katsumi Inoue
    2010, The Sixth Conference on Prestigious Applications of Intelligent Systems (PAIS 2010), 215, 277 - 282, English
    [Refereed]
    Introduction scientific journal

  • Principles of Modern SAT Solvers(Recent Advances in SAT Techniques)
    Nabeshima Hidetomo, Soh Takehide
    The Japanese Society for Artificial Intelligence, 01 Jan. 2010, Journal of Japanese Society for Artificial Intelligence, 25(1) (1), 68 - 76, Japanese

  • Analyzing Pathways through a Translation into SAT Problems
    宋 剛秀, 井上 克巳
    人工知能学会, 2009, 論文集, 23, 1 - 4, Japanese

  • A SAT-based Method for Solving the Two-dimensional Strip Packing Problem
    Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima
    Dec. 2008, The 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, English
    [Refereed]
    Introduction scientific journal

  • ショップ・スケジューリング問題のSAT変換による解法
    田村 直之, 多賀 明子, 番原 睦則, 宋 剛秀, 鍋島 英知, 井上 克巳
    2007, スケジューリング・シンポジウム2007講演論文集, 97 - 102, Japanese

  • Solving Shop Scheduling Problems by SAT encoding (in Japanese)
    Naoyuki Tamura, Akiko Taga, Mutsunori Banbara, Takehide Soh, Hidetomo Nabeshima, Katsumi Inoue
    2007, Proceedings of the Scheduling Symposium 2007, 97 - 102

  • Effective SAT Planning and SAT Scheduling by Lemma Reusing
    NABESHIMA Hidetomo, SOH Takehide, INOUE Katsumi, IWANUMA Koji
    In this paper, we propose a new approach, called lemma-reusing, for accelerating SAT based planning and scheduling. Generally, SAT based approaches generate a sequence of SAT problems which become larger and larger. A SAT solver needs to solve the problems until it encounters a satisfiable SAT problem. Many state-of-the-art SAT solvers learn lemmas called conflict clauses to prune redundant search space, but lemmas deduced from a certain SAT problem can not apply to solve other SAT problems. However, in certain SAT encodings of planning and scheduling, we prove that lemmas generated from a SAT problem are reusable for solving larger SAT problems. We implemented the lemma-reusing planner (LRP) and the lemma-reusing job shop scheduling problem solver (LRS). The experimental results show that LRP and LRS are faster than lemma-no-reusing ones.
    The Institute of Electronics, Information and Communication Engineers, 11 May 2006, IEICE technical report, 106(38) (38), 19 - 24, English

  • Effective SAT Planning and SAT Scheduling by Lemma Reusing
    NABESHIMA Hidetomo, SOH Takehide, INOUE Katsumi, IWANUMA Koji
    11 May 2006, 電子情報通信学会技術研究報告, 106(38(AI2006 1-11)) (38(AI2006 1-11)), 19 - 24, English

  • 効率的なSATプランニングとSATスケジューリングのための補題利用 (in English)
    鍋島 英知, 宋 剛秀, 井上 克巳, 岩沼 宏治
    2006, 信学技報, AI2006-4, 19 - 24

  • Experimental Results for Solving Job-shop Scheduling Problems with Multiple SAT Solvers
    Takehide Soh, Katsumi Inoue, Mutsunori Banbara, Naoyuki Tamura
    Oct. 2005, In the Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing, 25 - 38, English
    [Refereed]
    Introduction scientific journal

  • A-7-4 Parallel Implementation of the Block Lanczos Algorithm on the Dual-CPU Workstation
    Soh Takehide, Kuwakado Hidenori, Morii Masakatu, Tanaka Hatsukazu
    The Institute of Electronics, Information and Communication Engineers, 07 Sep. 2005, Proceedings of the Society Conference of IEICE, 2005, 177 - 177, Japanese

  • Solving Job-shop Scheduling Problems with Multiple SAT Solvers
    SOH Takehide, INOUE Katumi
    Many algorithms have recently been proposed for solving propositional satisfiability(SAT). This paper is concerned with a method to solve a job-shop scheduling problem(JSSP) by SAT solvers. Here, JSSP is translated into SAT using Crawford and Baker's method. We consider how due time affect the number of translated clauses. It turns out that due time heavily affects the difficulty of SAT problems. Next, to solve JSSP efficiently, we perform parallel execution of SAT solvers through Multisat, which competitively solves SAT problems by both systematic and stochastic SAT solvers. We also compare Multisat with single SAT solvers for JSSP.
    The Institute of Electronics, Information and Communication Engineers, 14 Jun. 2004, IEICE technical report. Artificial intelligence and knowledge-based processing, 104(133) (133), 19 - 24, Japanese

  • The characteristics of Japanese Vowel using frequency analysis
    Nishida Shigeki, Soh Takehide, Mashima Ryou
    Nara National College of Technology, 2002, Research reports of Nara Technical College, (38) (38), 29 - 34, Japanese

  • Finding Minimal Reaction Sets in Large Metabolic Pathways
    Takehide Soh, Katsumi Inoue
    Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010), English
    [Refereed]
    Introduction scientific journal

  • A SAT-based Method for Analyzing Metabolic Pathways
    Takehide Soh, Katsumi Inoue
    Poster presentation at: Systems Biochemistry 2010
    [Refereed]

■ Lectures, oral presentations, etc.
  • 正規制約に対するSAT符号化手法の提案と評価
    Tetsuya Ikuta, Naoyuki Tamura, Takehide Soh, Mutsunori Banbara
    The 22th Workshop on Programming and Programming Languages (PPL 2020), 2020, Japanese, 日本ソフトウェア科学会 プログラミング論研究会, Domestic conference
    Poster presentation

  • 解集合ソルバーを用いた様相命題論理の充足可能性判定
    Naoki Iino, Naoyuki Tamura, Takehide Soh, Banbara Mutsunori, Katsumi Inoue
    The 22th Workshop on Programming and Programming Languages (PPL 2020), 2020, Japanese, 日本ソフトウェア科学会 プログラミング論研究会, Domestic conference
    Poster presentation

  • 正規制約のSAT符号化とその性能評価
    生田 哲也, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE
    日本ソフトウェア科学会第35回大会, Aug. 2018, Japanese, Domestic conference
    Poster presentation

  • SATソルバーを用いた様相命題論理S4の充足可能性判定
    飯野 有軌, TAMURA NAOYUKI, BANBARA MUTSUNORI, SOH TAKEHIDE
    日本ソフトウェア科学会第35回大会, Aug. 2018, Japanese, Domestic conference
    Poster presentation

  • 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
    The 28th International Conference on Automated Planning and Scheduling, (ICAPS 2018), Jun. 2018, English, International conference
    Oral presentation

  • SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
    寸田 智也, 南 雄之, 宋 剛秀, 田村 直之
    DAシンポジウム2017, Aug. 2017, Japanese, 情報処理学会システムとLSIの設計技術研究会, 山代温泉ゆのくに天祥, Domestic conference
    Oral presentation

  • 解集合プログラミングを用いた多層ナンバーリンクの解法
    坡山 直樹, 川原 征大, 迫 龍哉, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), Mar. 2017, Japanese, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), Domestic conference
    Poster presentation

  • SugarTracer: SAT型制約ソルバーSugarのトレースツール
    吉玉 元和, 寸田 智也, 南 雄之, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), Mar. 2017, Japanese, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), Domestic conference
    Poster presentation

  • SATソルバーの最新動向と利用技術
    SOH TAKEHIDE, TAMURA NAOYUKI
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), Mar. 2017, Japanese, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), Domestic conference
    Oral presentation

  • SAT型制約ソルバーを用いた多層ナンバーリンクの解法
    寸田 智也, 南 雄之, 吉玉 元和, SOH TAKEHIDE
    DAシンポジウム2016, Sep. 2016, Japanese, 情報処理学会 システムとLSIの設計技術研究会（SLDM）, ゆのくに天祥 (石川県・加賀市), Domestic conference
    Poster presentation

  • インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー
    迫 龍哉, 川原 征大, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, 鍋島 英知
    第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016), Mar. 2016, Japanese, 日本ソフトウェア科学会プログラミング論研究会, 岡山県, Domestic conference
    Poster presentation

  • SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー)
    SOH TAKEHIDE
    人工知能学会 第9回AIツール入門講座, Dec. 2015, Japanese, 人工知能学会, 東京都, Domestic conference
    [Invited]
    Invited oral presentation

  • Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム
    SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015), Mar. 2015, Japanese, 日本ソフトウェア科学会プログラミング論研究会, 愛媛県, Domestic conference
    Poster presentation

  • Answer Set Programming as a Modeling Language for Course Timetabling
    Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
    第16回プログラミングおよびプログラミング言語ワークショップ, Mar. 2014, English, 日本ソフトウェア科学会プログラミング論研究会, 阿蘇の司ビラパークホテル, Domestic conference
    Oral presentation

  • パッキング配列問題の制約モデリングとSAT符号化
    則武 治樹, BANBARA MUTSUNORI, SOH TAKEHIDE, TAMURA NAOYUKI, 井上 克巳
    日本ソフトウェア科学会第30回大会, Sep. 2013, Japanese, 日本ソフトウェア科学会, 東京大学, Domestic conference
    Oral presentation

  • Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について
    SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI, Daniel Le Berre, Stéphanie Roussel
    日本ソフトウェア科学会第30回大会, Sep. 2013, Japanese, 日本ソフトウェア科学会, 東京大学, Domestic conference
    Oral presentation

  • System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems
    Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, Stéphanie Roussel
    The 4th International Workshop on Pragmatics of SAT, Jul. 2013, English, PoS, University of Helsinki, Finland, International conference
    Oral presentation

  • PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding
    Naoyuki Tamura, Mutsunori Banbara, Takehide Soh
    The 4th International Workshop on Pragmatics of SAT, Jul. 2013, English, PoS, University of Helsinki, Finland, International conference
    Oral presentation

  • 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, Jul. 2013, English, SAT, University of Helsinki, Finland, International conference
    Oral presentation

  • 正方形詰込み問題の制約モデルとSAT符号化を用いた解法
    佐古田 淳史, SOH TAKEHIDE, BANBARA MUTSUNORI, TAMURA NAOYUKI
    2013年度人工知能学会全国大会, Jun. 2013, Japanese, 人工知能学会, 富山国際会議場, Domestic conference
    Oral presentation

  • Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール
    宋 剛秀, 田村 直之, 番原 睦則
    第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013), Mar. 2013, Japanese, 日本ソフトウェア科学会, 東山温泉 御宿東鳳, Domestic conference
    Poster presentation

  • Towards Incremental SAT-based CSP Solving: Experimental Results for the Hamiltonian Cycle Problem
    SOH Takehide, FUNAKOSHI Taisuke, TAMURA Naoyuki, BANBARA Mutsunori
    The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks, Nov. 2012, English, CRIL, NII, Université d'Artois, Lens, France, International conference
    Oral presentation

■ Affiliated Academic Society
  • 人工知能学会

  • 電子情報通信学会

  • 情報処理学会

  • 日本ソフトウェア科学会

■ Research Themes
  • Research and Development of a New SAT Solving Technologies for Constraint Satisfaction Problems
    田村 直之, 宋 剛秀, 番原 睦則
    Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Grant-in-Aid for Scientific Research (C), Kobe University, 01 Apr. 2022 - 31 Mar. 2025

  • Research and Development on SAT-based Integration of Systematic and Stochastic Search
    番原 睦則, 田村 直之, 宋 剛秀
    Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Grant-in-Aid for Scientific Research (C), Nagoya University, 01 Apr. 2021 - 31 Mar. 2024
    近年，SAT技術の適用範囲を Beyond NP に拡大しようとする試みが国際的に活発化し，その重要課題として「モデル計数」，「知識コンパイラ」，「高階ソルバー」，「最適化や極小問題等への対応」が挙げれている．本研究では，「最適化や極小問題等への対応」に着目し，SAT技術を用いて系統的探索と確率的局所探索を統合的かつ効率的に扱うアルゴリズム技法およびソルバーの研究開発を行う．
    3年計画の初年度である2021年度は，国際ワークショップ発表1件，国内学会の大会での発表6件，国内研究会での発表4件，学生奨励賞受賞1件の成果を得た．
    組合せ最適化問題に対して系統的探索と確率的局所探索を統合的に適用する探索手法である優先度付き巨大近傍探索 (LNPS: Large Neighborhood Prioritized Search) を改良し，解集合プログラミング (Answer Set Programming; ASP) システム上に実装した．提案手法の有効性を評価するために，カリキュラムベース・コース時間割問題集(全61問)を用いて実験を行った．その結果，提案手法は61問中11問について，既知の最良値を更新することに成功した．また，通常の ASP 解法と比較して，既知の最良値との比を+472%から+53%に大幅に改善することができた．さらに，提案手法の特長的なアプリケーションの開発に向けて，時間割問題に加え，配電網問題，車両装備仕様問題などへの応用研究も行なった．

  • Engineering Approach for Expanding Combinatorial Reconfiguration: Toward a General-Purpose Solver Using Power Distribution Systems as a Steppingstone
    川原 純, 飯岡 大輔, 戸田 貴久, 宋 剛秀, 鈴木 顕, 照山 順一, 中畑 裕
    Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Grant-in-Aid for Transformative Research Areas (B), Kyoto University, 02 Oct. 2020 - 31 Mar. 2023
    本研究では組合せ遷移の実装技術の構築とその産業応用に向けて、研究開発の共通基盤となるソフトウェア開発を目標とする。初年度にあたる本年度は、広く知られているグラフの独立集合の遷移問題（独立集合遷移問題）に対して、4種のアプローチを検討した。1つ目は、組合せ遷移の技法を用いたアルゴリズムの設計であり、主に、状態空間の部分探索の手法を検討した。2つ目は、SAT（充足可能性問題）ソルバーを活用するアプローチである。有限整数領域上の制約を命題論理式へと変換する SAT 符号化を行い、SATソルバーの強力な推論性能を用いて独立集合遷移問題を解くソルバーを開発した。3つ目は、ゼロサプレス型二分決定グラフ (ZDD) を活用するアプローチである。当初予定では、ZDD を上記2手法に援用した高速化を想定していたが、本研究において、ZDD が表す独立集合族を直接遷移させるアルゴリズムの開発に成功したため、ZDD を単独で用いて独立集合遷移問題を解くことが可能になった。4つ目の手法は、当初は予定していない新たな構想であるが、モデル検査と呼ばれる、システムの形式的な検査を可能にする技術を用いた手法である。入力グラフと開始、目標独立集合が与えられた際に、開始集合から目標集合に遷移可能ではないことを検証する記述をモデル検査ソルバーに与え、遷移可能な場合は反例として解となる遷移列を出力する。 以上の4つの技法について、アルゴリズム設計と実装を行った。アルゴリズムの比較実験のためには、適切な入力データが必要であるが、組合せ遷移問題に対する広く知られたベンチマークデータは存在しないため、入力データの作成整備を行った。 配電切替への組合せ遷移技術の適用についても研究を行い、配電切替を全域木遷移問題として定式化し、4つの技法の適用を検討して、実装を行っている。

  • Acceleration of SAT-based CSP Solvers using MDD
    宋 剛秀
    Japan Society for the Promotion of Science, Grants-in-Aid for Scientific Research, Grant-in-Aid for Scientific Research (C), Kobe University, 01 Apr. 2020 - 31 Mar. 2023
    近年， 命題論理式の充足可能性判定問題 (SAT問題) を解くプログラムであるSATソルバーの飛躍的な進歩にともない， 制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している． 本研究の目的は， SAT型CSPソルバーの高速化であり, そのために MDD (Multi-valued Decision Diagram) を用いたCSPの正規化と， MDD が表す制約 (MDD制約) のSAT符号化を研究開発する． 本研究の意義は, SAT型CSPソルバーの新しい一方式を開拓できる点， 既存のCSPソルバーでは求解困難な問題に対して， より高性能な推論基盤を提供できる点である． CSPソルバーはスケジューリング問題, パッキング問題, 時間割問題, クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く， 研究成果の産業分野への応用も期待できる．
    2021年度は研究計画に記載された「(B) MDD 制約の SAT 符号化の研究開発」の研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った． (C) については， CEGAR (Counterexample-guided Abstraction Refinement) の並列化とSATソルバーを用いたハミルトン閉路問題への応用を研究し， 査読付き国際ワークショップで発表を行った．

  • 番原 睦則
    学術研究助成基金助成金／基盤研究(C), Apr. 2018 - Mar. 2021
    Competitive research funding

  • 宋 剛秀
    学術研究助成基金助成金／若手研究(B), Apr. 2016 - Mar. 2019, Principal investigator
    Competitive research funding

  • 田村 直之
    科学研究費補助金／基盤研究(B), Apr. 2016 - Mar. 2019
    Competitive research funding

  • 番原 睦則
    学術研究助成基金助成金／基盤研究(C), Apr. 2015 - Mar. 2018
    Competitive research funding

  • 宋 剛秀
    文部科学省, 科学研究費補助金(若手研究(B)), 2013 - 2015, Principal investigator
    近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライ
    Competitive research funding

  • 田村 直之
    文部科学省, 科学研究費補助金(基盤研究(B)), 2012 - 2014
    当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進めた．「A. フレキシブル制約に関する研究開発」については，フレキシブル制約のSAT符号化で重要になる擬似ブール制約の符号化方法の研究，PBSugarシステムの開発，および論文発表を行った．「B. 動的な制約変更に関する研究開発」については，動的な制約変更が可能なScarabシステムの開発および論文発表を行った．「C. ドメイン拡張に関する研究開発」については，記号推論が可能な解集合プログラミングシステム上で整数上の制約記述を可能にするプロトタイプシステムを開発し，性能評価を行った．「D. 応用研究開発」については，各種問題の評価を進めた．特に，時間割問題について優れた結果を得，論文発表を行った．また，「論理と推論の理論，実装，応用に関する合同セミナー」のERATO
    Competitive research funding

  • SAT変換を用いた制約充足問題の解法とシステム生物学への応用
    宋 剛秀
    日本学術振興会, 科学研究費助成事業, 特別研究員奨励費, 2010 - 2011
    最終年度の報告として、これまでの研究成果について以下にまとめる。 本研究では化学反応法則を満たしつつ入力代謝物集合から出力代謝物集合を生成可能なパスウェイを活性パスウェイ呼び、特にその包含関係において極小なものを極小活性パスウェイと呼ぶ。研究ではまず極小活性パスウェイを列挙する問題を極小活性パスウェイ同定問題として定義を行った。代謝パスウェイの解析を行う際には既存のデータから問題を構築する必要がある。そこで更新頻度において優れていることから、生物学的知識のデータベースEcoCyc(http://ecocyc.org/)から問題を構成して評価を行った。このデータから構成した問題をSAT技術によって解くために本研究では次の枠組みを用いた:(1)まず問題を命題論理式に符号化する、(2)SATソルバを漸増的に適用するインクリメンタルSAT解法を用いて符号化された命題論理式から極小モデルを計算する、(3)得られた極小モデルを逆符号化することで問題の解である極小活性パスウェイを得る。 提案した問題および解法の評価のためにEcoCycのデータから極小活性パスウェイ同定問題を構成し、SAT技術を用いて解を求めた。結果として9個の極小活性パスウェイを同定し、その中の2個が生物学における既存の知識と一致したパスウェイ(参照パスウェイ)であることを確認している。また専門家との議論で提案された制約を命題論理式に追加することでより精緻なパスウェイを計算することに成功した。この成果は国内雑誌論文として発表を行った。また代謝パスウェイに対する解集合プログラミングを用いた解析研究についても国際会議の会議録で発表を行った。 さらにより具体的な生物学の問題に適用するために、大腸菌における単一遺伝子ノックアウトの影響予測を極小活性パスウェイの同定によって行う手法の研究を国立遺伝学研究所の研究チームと共同して進めた。大腸菌の解糖系に対して計算機実験を行った結果,提案手法の予測が生物実験の結果とよく一致することを確認した。この成果は国際会議において発表を行った。

TOP