SEARCH
検索詳細
宋 剛秀DX・情報統括本部准教授
プロフィール
神戸大学 情報基盤センター 准教授．博士（情報学)．
SAT問題を含む制約充足問題の研究およびシステム生物学への応用に従事．
ResearchMap の情報は最新でないことがあります．
最新の情報・詳細は以下のURLをご覧ください．
http://tsoh.org/jp/
研究者基本情報
■ 学位■ 研究ニュース
■ 研究キーワード
■ 研究分野
研究活動情報
■ 受賞- 2022年08月 XCSP3 Competition Organization, 2022 XCSP3 Competition 逐次CSPソルバー部門準優勝, Fun-sCOP
- 2019年10月02日 XCSP3 Competition Organization, 2019 XCSP3 Competition 逐次CSPソルバー部門準優勝, Fun-sCOPフランス共和国国際学会・会議・シンポジウム等の賞
- 2019年08月29日 日本ソフトウェア科学会, 第７回解説論文賞 (2018年度), SAT型制約プログラミングシステムと周辺技術国内学会・会議・シンポジウム等の賞
- 2019年 人工知能学会, 2019年度全国大会優秀賞, A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition国内学会・会議・シンポジウム等の賞
- 2018年09月 情報処理学会, 情報処理学会 2018 年度特選論文, SAT技術を用いたペトリネットのデッドロック検出手法の提案国内学会・会議・シンポジウム等の賞
- 2018年08月 XCSP3 Competition Organization, 2018 XCSP3 Competition 2部門優勝 (逐次CSPソルバー部門, 並列CSPソルバー部門), sCOPフランス共和国国際学会・会議・シンポジウム等の賞
- 2017年03月 日本ソフトウェア科学会 プログラミング論研究会, PPL2017発表賞（一般の部）, SATソルバーの最新動向と利用技術学会誌・学術雑誌による顕彰
- 2017年03月 人工知能学会, 2016年度全国大会優秀賞, SAT型制約ソルバーによるナンバーリンクの解法とその評価国内学会・会議・シンポジウム等の賞
- 2016年03月 日本ソフトウェア科学会, 第20回研究論文賞, パッキング配列問題の制約モデリングとSAT符号化学会誌・学術雑誌による顕彰
- 2015年08月 情報処理学会DAシンポジウム2015, 最優秀賞, SAT型制約ソルバーを用いたナンバーリンクの求解と解の最適化
- 2015年08月 情報処理学会 SLDM研究会, アルゴリズムデザインコンテスト2015 最優秀賞 (DAシンポジウム2015), iSugar+GlueMiniSat国内学会・会議・シンポジウム等の賞
- 2014年09月 日本ソフトウェア科学会, 第31回大会高橋奨励賞, Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール国内学会・会議・シンポジウム等の賞
- 2014年08月 情報処理学会 SLDM研究会, アルゴリズムデザインコンテスト2014 最優秀賞 (DAシンポジウム2014・SWEST16), Sugar+GlueMiniSat国内学会・会議・シンポジウム等の賞
- 2014年08月 情報処理学会DAシンポジウム2014, アルゴリズムデザインコンテスト2014 最優秀賞, SAT型制約ソルバーを用いたナンバーリンクの解法
- 2010年04月 総合研究大学院大学, 学長賞, SATとASPを用いた生物学におけるパスウェイの解析日本国その他の賞
- 2009年09月 人工知能学会, ２００９年度全国大会優秀賞, モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定日本国国内学会・会議・シンポジウム等の賞
- 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), 2024年06月, Proceedings of the International Symposium on Combinatorial Search, 17, 285 - 286研究論文（学術雑誌）
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024年, 22nd International Symposium on Experimental Algorithms(SEA), 26 - 15研究論文（国際会議プロシーディングス）
- Springer, 2023年09月, 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., 英語, 国際誌, 国際共著している[査読有り]研究論文（国際会議プロシーディングス）
- SCITEPRESS - Science and Technology Publications, 2023年03月, Proceedings of the 16th International Joint Conference on Biomedical Engineering Systems and Technologies, 163 - 174[査読有り]研究論文（国際会議プロシーディングス）
- IEEE, 2023年, 35th IEEE International Conference on Tools with Artificial Intelligence(ICTAI), 294 - 302研究論文（国際会議プロシーディングス）
- 2023年, CPAIOR, 167 - 183[査読有り]研究論文（国際会議プロシーディングス）
- 2022年12月, CoRR, abs/2207.13959[査読有り]研究論文（学術雑誌）
- 2022年09月, CoRR, abs/2208.02495研究論文（学術雑誌）
- 2022年03月, 情報処理学会第84回全国大会講演論文集, 日本語解集合プログラミングを用いた優先度付き巨大近傍探索の実装と評価研究論文（大学，研究機関等紀要）
- 2022年03月, 情報処理学会第84回全国大会講演論文集, 日本語チャネリング制約を用いた alldifferent 制約の SAT 符号化研究論文（研究会，シンポジウム資料等）
- 2022年01月, 情報処理学会 研究報告アルゴリズム（AL）, 2022-AL-186(5) (5), 1 - 7, 日本語有界モデル検査による独立集合遷移問題の解法に関する考察研究論文（研究会，シンポジウム資料等）
- 2021年07月, Pragmatics of SAT 2021, 英語Towards CEGAR-based Parallel SAT Solving[査読有り]研究論文（その他学術会議資料等）
- 人工知能学会, 2020年03月, 人工知能基本問題研究会, 112, 6 - 11, 日本語CEGARと反例の共有を用いたSAT型CSPソルバーの並列化方法の考察 (特集 「命題論理の充足可能性問題SATの最新動向」および一般)
- 一般社団法人 人工知能学会, 2020年, 人工知能学会全国大会論文集, 2020(0) (0), 2N5OS17b05 - 2N5OS17b05, 日本語
様相命題論理の体系Kについて，与えられた論理式の充足可能性を判定する新しい手法を提案する．提案する手法はタブロー法に基づいており，解集合プログラミングを用いて実装されている．タブロー法に基づいた既存手法では，可能世界を最初にすべて生成してから充足可能性判定を行う方法か，可能世界を幅優先的に順次拡大しながら充足可能性判定を繰り返し行う方法が取られている．提案するシステムでは，これらの方法に加え，ヒューリスティック関数を用いて可能世界を順次拡大する手法を導入している．ヒューリスティック関数を用いることで，充足不能になりそうな可能世界から先に探索することが可能になり，判定手続きの高速化につながることが期待できる．本手法を標準的なベンチマーク問題を用いて評価したところ，論理式の長さをヒューリスティック関数に用いた場合に，既存手法よりも良い結果が得られる場合があることがわかった．また，既存手法ではSATソルバーが利用されているが，本手法では解集合プログラミングを利用することで，非常に簡潔に証明系を記述できている点にも特徴がある．
研究論文（研究会，シンポジウム資料等） - 人工知能学会, 2019年03月, 人工知能学会研究会資料, SIG-FPAI-B803, 6 - 11, 日本語研究論文（その他学術会議資料等）
- 2019年, Solver Descriptions of XCSP3 Competition 2019 (XCSP19), 1 - 2, 英語Solver Description of Fun-sCOP研究論文（その他学術会議資料等）
- Springer, 2019年, Annals OR, 275(1) (1), 3 - 37, 英語[査読有り]研究論文（学術雑誌）
- 一般社団法人 人工知能学会, 2019年, 人工知能学会全国大会論文集, 2019(0) (0), 1E2OS3a03 - 1E2OS3a03, 日本語
制約充足問題 (CSP) は, 与えられた制約を全て充足する値割当てを求める問 題である. CSP には, 人工知能およびオペレーションズ・リサーチにおける幅 広い応用がある. XCSP3 は, CSP を記述できる主要な制約言語の1つであり， 105種類2万3千問を超える問題例が XCSP3 のデータベースから利用可能である． また2018年には, XCSP3ソルバーの国際競技会が開催されており, 18 のソルバー が参加した. 本論文では, 現在開発中の CSP ソルバー sCOP とその2018年XCSP3競技会の結 果について述べる. sCOP はSAT型ソルバーであり, CSP をSAT問題へと符号化 し, SATソルバーを用いて解を求める. 現在, sCOP では順序符号化と対数符号 化を利用することができ, 最新の SAT ソルバーをバックエンドに利用可能で ある. 2018年XCSP3競技会において, sCOP はCSP・スタンダード・逐次部門と CSP・スタンダード・並列部門の2部門に参加登録し, その両部門で優勝した．
研究論文（その他学術会議資料等） - SAT技術を用いたペトリネットのデッドロック検出手法の提案本論文では，トークン数が整数値である一般のペトリネットを対象とし，そのデッドロック検出についてSAT技術を用いた手法を提案する．提案手法では，非負整数値であるトークン数を表現するために順序符号化を採用することで，既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した．また，既存SAT型手法で採用されていたモデル（連続発火モデルと呼ぶ）よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し，性能向上を実現した．評価実験では，Model Checking Contest 2017のベンチマーク問題を用いて，連続発火モデルと多重発火モデルを比較した．ほぼすべての問題で多重発火モデルのほうが優れていたが，特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった．また，Model Checking Contest 2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った．提案手法は，デッドロックを検出できた問題数ではLoLA，Tapaalより少なかったが，LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し，提案手法の有効性が確認できた．情報処理学会, 2018年09月, 情報処理学会論文誌, 59(9) (9), 1749 - 1760, 日本語
- 本論文では，擬似ブール (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.日本ソフトウェア科学会, 2018年08月, コンピュータソフトウェア = Computer software, 35(3) (3), 65 - 78, 日本語[査読有り]研究論文（学術雑誌）
- 2018年, Solver Descriptions of XCSP3 Competition 2018 (XCSP18), 1 - 2, 英語sCOP: SAT-based Constraint Programming System研究論文（その他学術会議資料等）
- 日本ソフトウェア科学会, 2018年, コンピュータ ソフトウェア, 35(4) (4), 72 - 92, 日本語
命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは，2000年以降その性能面において飛躍的に進化した．それに伴い，解きたい問題をSAT符号化によりSAT問題へと変換し，SATソルバーを用いて解くSAT型システムが，プランニング，ソフトウェア・ハードウェア検証，スケジューリング問題など様々な分野で成功を収めるようになった．本稿では，まずSATソルバーの最新動向として，性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う．次に SAT ソルバーの利用技術の視点から，SAT ソルバーの機能面の進化と符号化技術を組み合わせることで，複雑な問題を解くことが可能になることの説明を行う．そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する．
[査読有り] - 日本ソフトウェア科学会, 2017年09月, 日本ソフトウェア科学会大会論文集, 34, 393 - 404, 日本語ブール基数制約を経由した擬似ブール制約のSAT符号化手法研究論文（研究会，シンポジウム資料等）
- 2017年02月, INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS, 26(1) (1), 英語[査読有り]研究論文（学術雑誌）
- World Scientific Publishing, 2017年02月, International Journal on Artificial Intelligence Tools, 26(1) (1), 1 - 29, 英語[査読有り]研究論文（学術雑誌）
- 一般社団法人 人工知能学会, 2017年, 人工知能学会研究会資料 人工知能基本問題研究会, 103, 4 - 4, 日本語
- 一般社団法人 人工知能学会, 2017年, 人工知能学会全国大会論文集, 2017(0) (0), 1M1OS02a2 - 1M1OS02a2, 日本語
本稿ではSAT技術を用いたペトリネットのデッドロック検出手法について述べる．まず，トークン数や多重度が整数値のペトリネットの制約モデルを提案し，次に，検証するステップ長が短くなるように制約モデルを改良する．また，マーキングインバリアントを用いて，トークン数の上限を求める方法について述べる．最後に計算機実験で提案手法の有効性を評価する．
研究論文（研究会，シンポジウム資料等） - 一般社団法人 人工知能学会, 2017年, 人工知能学会全国大会論文集, 2017(0) (0), 1M1OS02a4 - 1M1OS02a4, 日本語
解集合プログラミング(ASP)言語は一階論理に基づく表現力の高いモデリング言語である．ASPソルバーは安定モデル意味論に基づいた解集合を求める．近年，SAT 技術を応用した高速 ASP ソルバーが実現され，人工知能分野への実用的応用が急速に拡大している．本研究では，高速な ASP 型制約ソルバーの実現に向けて，制約充足問題から ASP への符号化の設計・実装・評価を行う．
研究論文（研究会，シンポジウム資料等） - 日本オペレーションズ・リサーチ学会 常設研究部会数理計画, 2017年, 第29回RAMPシンポジウム論文集, 73 - 88, 日本語解集合プログラミングによるカリキュラムベース・コース時間割編成[招待有り]研究論文（研究会，シンポジウム資料等）
- Springer, 2017年, Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017), 10416, 596 - 614, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 一般社団法人 人工知能学会, 2017年, 人工知能学会全国大会論文集, 2017(0) (0), 1M1OS02a2 - 1M1OS02a2, 日本語
本稿ではSAT技術を用いたペトリネットのデッドロック検出手法について述べる．まず，トークン数や多重度が整数値のペトリネットの制約モデルを提案し，次に，検証するステップ長が短くなるように制約モデルを改良する．また，マーキングインバリアントを用いて，トークン数の上限を求める方法について述べる．最後に計算機実験で提案手法の有効性を評価する．
研究論文（研究会，シンポジウム資料等） - 人工知能学会, 2017年01月, 人工知能学会研究会資料, 18 - 23, 日本語ブール基数制約を経由した擬似ブール制約のSAT符号化法研究論文（研究会，シンポジウム資料等）
- 情報処理学会, 2017年01月, 第58回プログラミング・シンポジウム予稿集, 165 - 172, 日本語SATソルバーの使い方 —問題をSATに符号化する方法—研究論文（研究会，シンポジウム資料等）
- 情報処理学会, 2017年01月, 第58回プログラミング・シンポジウム予稿集, 71 - 74, 日本語Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー研究論文（研究会，シンポジウム資料等）
- Springer, 2017年, The 14th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR-17), 265 - 278, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 近年SATソルバーの求解性能が飛躍的に向上しており，様々な分野で応用が進んでいる．しかし，SATソルバーは連言標準形の命題論理式を入力としており，実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない．このため，より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている．本解説では，そのような利用・拡張の1つとしてSATソルバーの求解性能と制約プログラミングシステムの表現力を融合させたSAT型制約プログラミングシステム(SAT型CPシステム)について説明し，その周辺技術についても概説する．日本ソフトウェア科学会, 2017年, コンピュータ ソフトウェア, 34(1) (1), 1_67 - 1_80, 日本語[査読有り]
- 2016年11月, Computer Software, 33(4) (4), 16 - 29An incremental SAT solving library and its applications[査読有り]研究論文（学術雑誌）
- Association for Computing Machinery, 2016年10月, ACM Journal of Experimental Algorithmics, 21(1) (1), 1 - 44, 英語[査読有り]研究論文（学術雑誌）
- 人工知能学会, 2016年03月, 人工知能基本問題研究会, 100, 19 - 24, 日本語クラウド上のソフトウェア要素最適配置問題の解法 (特集 「命題論理の充足可能性問題SATと応用技術」および一般)
- 2016年03月, 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016), カテゴリC1, 日本語解集合プログラミングを用いた制約組合せテストケース生成[査読有り]研究論文（研究会，シンポジウム資料等）
- 情報処理学会, 2016年03月, 第45回バイオ情報学研究発表会, 11, 1 - 6, 日本語分子ネットワーク上の状態推定とその可視化による知識発見支援研究論文（研究会，シンポジウム資料等）
- 情報処理学会, 2016年01月, 第57回プログラミング・シンポジウム, 1 - 10, 日本語SATソルバーを用いた制約プログラミングシステムとその応用研究論文（研究会，シンポジウム資料等）
- 一般社団法人 人工知能学会, 2016年, 人工知能学会全国大会論文集, 2016(0) (0), 1D4OS02a3 - 1D4OS02a3, 日本語研究論文（研究会，シンポジウム資料等）
- 一般社団法人 人工知能学会, 2016年, 人工知能学会全国大会論文集, 2016(0) (0), 1D4OS02a4 - 1D4OS02a4, 日本語研究論文（研究会，シンポジウム資料等）
- 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, 英語Teaspoon: Solving the curriculum-based course timetabling problems with answer set programming[査読有り]研究論文（国際会議プロシーディングス）
- 日本ソフトウェア科学会, 2015年09月, 日本ソフトウェア科学会第32回大会, 1 - 11, 日本語順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化研究論文（研究会，シンポジウム資料等）
- 日本ソフトウェア科学会, 2015年09月, 日本ソフトウェア科学会第32回大会, 1 - 8, 日本語Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について研究論文（研究会，シンポジウム資料等）
- 日本ソフトウェア科学会, 2015年09月, 日本ソフトウェア科学会第32回大会, 32, 1 - 9, 日本語SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価研究論文（研究会，シンポジウム資料等）
- 日本ソフトウェア科学会, 2015年09月, 日本ソフトウェア科学会第32回大会, 1 - 12, 日本語iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー研究論文（研究会，シンポジウム資料等）
- 人工知能学会, 2015年03月, 第第97回人工知能基本問題研究会．人工知能学会研究会資料, 65 - 73, 日本語制約充足問題のハイブリッド符号化に向けて研究論文（研究会，シンポジウム資料等）
- Springer, 2015年, CoRR, abs/1312.6113, 112 - 126[査読有り]研究論文（国際会議プロシーディングス）
- Springer, 2015年, Proceedings of the Sixth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2013), 112 - 126, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 2015年, CoRR, abs/1510.00523[査読有り]
- Springer, 2015年, Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, Lexington, KY, USA, September 27-30, 2015. Proceedings, 9345, 112 - 126[査読有り]研究論文（国際会議プロシーディングス）
- 2015年, 2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015), 2016-January, 421 - 428, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 一般社団法人 人工知能学会, 2015年, 人工知能学会全国大会論文集, 2015(0) (0), 2H5OS03b5 - 2H5OS03b5, 日本語
制約解集合プログラミング(CASP;Constraint Answer Set Programming)は，解集合プログラミングと制約プログラミングを融合した新しいプログラミングパラダイムである．近年，SAT技術を応用した高速なCASPソルバが開発され，注目を集めている．本研究では，組合せテストケース生成問題に対して，制約充足問題としての定式化およびCASP符号化を提案し，その有効性を検証する．
研究論文（研究会，シンポジウム資料等） - Springer, 2015年, Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015), 112 - 126, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 2015年, 2015 IEEE 27TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2015), 421 - 428, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 日本ソフトウェア科学会, 2014年09月, 日本ソフトウェア科学会第31回大会講演論文集, 1 - 15, 日本語制約解集合プログラミングシステムの設計方式に関する考察研究論文（研究会，シンポジウム資料等）
- 日本ソフトウェア科学会, 2014年09月, 日本ソフトウェア科学会第31回大会講演論文集, 1 - 15, 日本語Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール研究論文（研究会，シンポジウム資料等）
- 情報処理学会システムとLSIの設計技術研究会, 2014年08月, DAシンポジウム2014論文集, 2014(2014) (2014), 215 - 220, 日本語SAT型制約ソルバーを用いたナンバーリンクの解法
- 2014年07月, Proceedings of the 5th International Workshop on Pragmatics of SAT (PoS 2014), 1 - 12, 英語Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem研究論文（国際会議プロシーディングス）
- 人工知能学会, 2014年05月, 第28回人工知能学会全国大会論文集, 1 - 4, 日本語登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法研究論文（研究会，シンポジウム資料等）
- 2014年, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, 684 - 693[査読有り]研究論文（学術雑誌）
- 一般社団法人 人工知能学会, 2014年, 人工知能学会全国大会論文集, 2014(0) (0), 1D5OS11b6i - 1D5OS11b6i, 日本語
近年のSAT技術の進歩に伴い，SAT型制約プログラミングシステムが成功をおさ めいる．しかし従来のシステムではSATソルバーとの通信手段がCNFファイルや 基本的なAPIに限定されており，SATソルバーとの密接な連携が困難であった． 本研究ではSATソルバーと密に結合された制約プログラミングシステムScarabの提案を行う．またハミルトン閉路問題への応用を示し，その有効性の評価を行う．
研究論文（研究会，シンポジウム資料等） - 2014年, LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2014, 8761, 684 - 693, 英語Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem[査読有り]研究論文（国際会議プロシーディングス）
- IEEE, 2013年11月, Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013), 英語[査読有り]研究論文（国際会議プロシーディングス）
- 2013年07月, THEORY AND PRACTICE OF LOGIC PROGRAMMING, 13(4/5) (4/5), 783 - 798, 英語[査読有り]研究論文（学術雑誌）
- Cambridge University Press, 2013年07月, Theory and Practice of Logic Programming, 13(4-5) (4-5), 783 - 798, 英語[査読有り]研究論文（学術雑誌）
- 2013年03月, 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013) 論文集, 日本語SAT符号化を用いたパッキング配列の構成[査読有り]研究論文（学術雑誌）
- 2013年System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems⋆研究論文（学術雑誌）
- Springer, 2013年, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, 7962, 429 - 436[査読有り]研究論文（国際会議プロシーディングス）
- IEEE Computer Society, 2013年, 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, Herndon, VA, USA, November 4-6, 2013, 1020 - 1027[査読有り]研究論文（国際会議プロシーディングス）
- Springer, 2013年, Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), 7962, 429 - 436, 英語[査読有り]研究論文（国際会議プロシーディングス）
- 2012年12月, International Journal On Advances in Life Sciences, 4(3-4):154-165, 英語Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration研究論文（学術雑誌）
- [日本ソフトウェア科学会], 2012年08月, 日本ソフトウェア科学会大会論文集, 29, 495 - 502, 日本語カリキュラムベースのコース時間割問題の擬似ブール最適化問題への符号化研究論文（国際会議プロシーディングス）
- 2012年03月, The 4th International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies, 11 - 19, 英語Predicting Gene Knockout Effects by Minimal Pathway Enumeration研究論文（国際会議プロシーディングス）
- Springer, 2012年, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6479, 167 - 183, 英語[査読有り]研究論文（国際会議プロシーディングス）
- Springer, 2012年, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6479, 167 - 183, 英語[査読有り]研究論文（国際会議プロシーディングス）
- Japanese Society for Artificial Intelligence, 2012年, 人工知能学会論文誌, 27(3) (3), 204 - 212, 日本語[査読有り]研究論文（学術雑誌）
- 2010年11月, Fundamenta Informaticae, 102(3-4): 467-487, 英語[査読有り]研究論文（学術雑誌）
- 2010年, Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010), 54 - 54, 英語Finding Minimal Reaction Sets in Large Metabolic Pathways[査読有り]研究論文（国際会議プロシーディングス）
- 2010年, FUNDAMENTA INFORMATICAE, 102(3-4) (3-4), 467 - 487, 英語[査読有り]研究論文（学術雑誌）
- 2010年, Poster presentation at: Systems Biochemistry 2010, 英語A SAT-based Method for Analyzing Metabolic Pathways[査読有り]研究論文（研究会，シンポジウム資料等）
- 2009年06月, 人工知能学会全国大会, 日本語(2H3-3)SAT問題への変換を用いたフィードバックを含むパスウェイの解析研究論文（研究会，シンポジウム資料等）
- IOS Press, 2009年, Jouranal of Algorithms in Cognition, Informatics and Logic, 102(3,4) (3,4), 467 - 487, 英語[査読有り]研究論文（学術雑誌）
- 2008年12月, In Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 英語A SAT-based Method for Solving the Two-dimensional Strip Packing Problem[査読有り]研究論文（学術雑誌）
- 2006年11月, DISCRETE APPLIED MATHEMATICS, 154(16) (16), 2291 - 2306, 英語[査読有り]研究論文（学術雑誌）
- AAAI Press, 2006年, In the proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006), 103 - 112, 英語Lemma Reusing for SAT based Planning and Scheduling[査読有り]研究論文（国際会議プロシーディングス）
- 2005年10月, Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing (held in conjunction with CP'05), pp.25-38, 英語Experimental results for solving job-shop scheduling problems with multiple SAT solvers[査読有り]研究論文（学術雑誌）
- 社団法人電子情報通信学会, 2004年06月, 電子情報通信学会技術研究報告. AI, 人工知能と知識処理, 104(133) (133), 19 - 24, 日本語複数のSATソルバを用いたジョブショップスケジューリング問題の解法(「自動推論:帰納,演繹,モデル検査研究論文（研究会，シンポジウム資料等）
- 人工知能学会論文誌(解説論文), 25(1) (1), 68 - 76高速SATソルバーの原理[査読有り]
- 2024年05月18日, CoRR, abs/2403.07885, 11p., 英語, 国際誌, 国際共著している速報，短報，研究ノート等（学術雑誌）
- 2024年, 日本ソフトウェア科学会大会講演論文集(Web), 41stハミルトン閉路問題に対するCut-arc集合制約を用いたSAT型CEGAR解法
- 2024年, 日本ソフトウェア科学会大会講演論文集(Web), 41st独立集合遷移問題に対する有界組合せ遷移の改良に関する一考察
- 2022年, 日本オペレーションズ・リサーチ学会秋季研究発表会アブストラクト集, 2022ZDDを用いた組合せ遷移ソルバー
- 2021年09月, 日本ソフトウェア科学会第38回大会ポスター発表, 日本語CDCL型SATソルバーの内部動作可視化ツールその他
- 2021年09月, 日本ソフトウェア科学会第38回大会ポスター発表, 日本語ライフゲームを逆向きに動かすその他
- 2020年09月, 日本ソフトウェア科学会第37回大会ポスター発表, 日本語SATソルバーを用いた一層平面配置配線問題の解法に関する考察その他
- SAT技術の進化と応用 〜パズルからプログラム検証まで〜：2．SATとパズル -問題をいかにSATソルバーで解くか-数独やナンバーリンクなどのパズルを題材として取り上げ，SATソルバーを用いてこれらのパズルを解く方法について説明する．SATソルバーは，与えられた連言標準形の命題論理式（CNF式）を満たす解を探索するプログラムである．近年になって大幅な性能向上が実現され，最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている．このことを背景とし，さまざまな問題をCNF式に変換（符号化） しSAT ソルバーで解を求める手法が注目を集めている．本稿では，パズルを題材とすることで，この手法について分かりやすく解説する．情報処理学会 ; 1960-, 2016年07月15日, 情報処理, 57(8) (8), 710 - 715, 日本語
- 2015年03月18日, 人工知能学会人工知能基本問題研究会資料, 97th, 65 - 73, 日本語制約充足問題のハイブリッド符号化に向けて
- 一般社団法人 人工知能学会, 2015年, 人工知能学会全国大会論文集, 2015(0) (0), 2H5OS03b5 - 2H5OS03b5, 日本語
制約解集合プログラミング(CASP;Constraint Answer Set Programming)は，解集合プログラミングと制約プログラミングを融合した新しいプログラミングパラダイムである．近年，SAT技術を応用した高速なCASPソルバが開発され，注目を集めている．本研究では，組合せテストケース生成問題に対して，制約充足問題としての定式化およびCASP符号化を提案し，その有効性を検証する．
- 2015年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL6-3, 日本語順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化
- 2015年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.SOFUTOWEA1, 日本語Scala上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
- 2015年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL3-1, 日本語SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価
- 2015年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 32nd, ROMBUNNO.PPL6-1, 日本語iSugar:インクリメンタルSAT解法が利用可能なSAT型制約ソルバー
- [日本ソフトウェア科学会], 2014年09月07日, 日本ソフトウェア科学会大会論文集, 31, 140 - 154, 日本語制約解集合プログラミングシステムの設計方式に関する考察
- [日本ソフトウェア科学会], 2014年09月07日, 日本ソフトウェア科学会大会論文集, 31, 217 - 231, 日本語Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
- 人工知能学会, 2014年, 人工知能学会全国大会論文集, 28, 1 - 4, 日本語登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
- 2014年, 人工知能学会全国大会論文集(CD-ROM), 28th, ROMBUNNO.1D5-OS-11B-7, 日本語登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法
- 2014年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 31st, ROMBUNNO.PPL2-3, 日本語制約解集合プログラミングシステムの設計方式に関する考察
- 日本ソフトウェア科学会, 2014年, コンピュータソフトウェア, 31(1) (1), 116 - 130, 日本語
- 2014年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 31st, ROMBUNNO.SOFUTO1-1, 日本語Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール
- 一般社団法人 人工知能学会, 2014年, 人工知能学会全国大会論文集, 2014(0) (0), 1D5OS11b6i - 1D5OS11b6i, 日本語
近年のSAT技術の進歩に伴い，SAT型制約プログラミングシステムが成功をおさ めいる．しかし従来のシステムではSATソルバーとの通信手段がCNFファイルや 基本的なAPIに限定されており，SATソルバーとの密接な連携が困難であった． 本研究ではSATソルバーと密に結合された制約プログラミングシステムScarabの提案を行う．またハミルトン閉路問題への応用を示し，その有効性の評価を行う．
- 2014年, Lect Notes Comput Sci, 8761, 684 - 693, 英語Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
- [日本ソフトウェア科学会], 2013年09月10日, 日本ソフトウェア科学会大会論文集, 30, 79 - 92, 日本語パッキング配列問題の制約モデリングとSAT符号化
- [日本ソフトウェア科学会], 2013年09月10日, 日本ソフトウェア科学会大会論文集, 30, 237 - 245, 日本語Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
- 2013年07月, Theor Pract Log Program, 13(4/5) (4/5), 783 - 798, 英語
- 人工知能学会, 2013年03月01日, 人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence, 28(2) (2), 343 - 348, 日本語「SATソルバー」(私のブックマーク)その他
- 人工知能学会, 2013年03月01日, 人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence, 28(2) (2), 343 - 348, 日本語「SATソルバー」(私のブックマーク)
- 日本ソフトウェア科学会, 2013年01月25日, コンピュータソフトウェア, 30(1) (1), 16 - 19, 日本語
- 一般社団法人 人工知能学会, 2013年, 人工知能学会全国大会論文集, 2013(0) (0), 2E5OS09b1 - 2E5OS09b1, 日本語
近年，命題論理の充足可能性判定問題(SAT)を非常に高速に解くことが可能なSATソルバーが実現され，SAT技術を多分野に応用する研究が急速に拡大している．本研究では，詰込み問題の一つである正方形詰込み問題に対して，制約充足問題としての定式化及びSAT符号化を用いた解法を提案し，その有効性を検証する．
- 2013年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 30th, 79 - 92, 日本語パッキング配列問題の制約モデリングとSAT符号化
- 2013年, 日本ソフトウエア科学会大会講演論文集(CD-ROM), 30th, 237 - 245, 日本語Scala上で実現されたSAT型制約プログラミングシステムのための開発ツールScarabについて
- 2012年02月15日, 情報処理学会研究報告(CD-ROM), 2011(5) (5), ROMBUNNO.ICS-165,NO.7, 英語Predicting Gene Knockout Effects on E. coli by Minimal Active Pathway Enumeration
- 社団法人人工知能学会, 2012年01月01日, 人工知能学会誌, 27(1) (1), 84 - 84, 日本語Studies on Applying Incremental SAT Solving to Optimization and Enumeration Problems(Foundations of AI,
Doctorial Theses on Aritificial Intelligence) - 人工知能学会, 2010年, 人工知能学会論文誌(解説論文), 25(1) (1), 68 - 76, 日本語高速SATソルバーの原理[査読有り]記事・総説・解説・論説等（学術雑誌）
- 人工知能学会, 2010年, 人工知能学会全国大会論文集, 24, 1 - 4, 日本語モデル生成を用いた代謝ネットワークにおける極小部分パスウェイの同定
- 2010年, The Sixth Conference on Prestigious Applications of Intelligent Systems (PAIS 2010), 215, 277 - 282, 英語[査読有り]記事・総説・解説・論説等（学術雑誌）
- 社団法人人工知能学会, 2010年01月01日, 人工知能学会誌, 25(1) (1), 68 - 76, 日本語高速SATソルバーの原理(<特集>最近のSAT技術の発展)
- 人工知能学会, 2009年, 論文集, 23, 1 - 4, 日本語SAT問題への変換を用いたフィードバックを含むパスウェイの解析
- 2008年12月, The 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 英語A SAT-based Method for Solving the Two-dimensional Strip Packing Problem[査読有り]記事・総説・解説・論説等（学術雑誌）
- 2007年, スケジューリング・シンポジウム2007講演論文集, 97 - 102, 日本語ショップ・スケジューリング問題のSAT変換による解法
- 2007年, Proceedings of the Scheduling Symposium 2007, 97 - 102Solving Shop Scheduling Problems by SAT encoding (in Japanese)
- 効率的なSATプランニングとSATスケジューリングのための補題再利用本稿では,SATプランニングとSATスケジューリングを効率よく解くために補題再利用手法を提案し,その効果を実証する.一般的に,SATプランニングやSATスケジューリングなどのSAT符号化手法においては,徐々に大きくなるSAT問題の列を解く必要がある.多くの最新のSATソルバは,冗長な探索空間を狩り取るために補題を学習し利用している.しかし,あるSAT問題から生成された補題は,基本的に他のSAT問題を解くために利用することはできない.本稿では,SATプランニングとSATスケジューリングにおけるある特定のSAT符号化においては補題が再利用可能であることを証明し,補題を再利用することにより効率的に問題を解くことができることを実証する.一般社団法人電子情報通信学会, 2006年05月11日, 電子情報通信学会技術研究報告. AI, 人工知能と知識処理, 106(38) (38), 19 - 24, 英語
- 2006年05月11日, 電子情報通信学会技術研究報告, 106(38(AI2006 1-11)) (38(AI2006 1-11)), 19 - 24, 英語Effective SAT Planning and SAT Scheduling by Lemma Reusing
- 2006年, 信学技報, AI2006-4, 19 - 24効率的なSATプランニングとSATスケジューリングのための補題利用 (in English)
- 2005年10月, In the Proceedings of the 1st International Workshop on Distributed and Speculative Constraint Processing, 25 - 38, 英語Experimental Results for Solving Job-shop Scheduling Problems with Multiple SAT Solvers[査読有り]記事・総説・解説・論説等（学術雑誌）
- 一般社団法人電子情報通信学会, 2005年09月07日, 電子情報通信学会ソサイエティ大会講演論文集, 2005, 177 - 177, 日本語A-7-4 Dual-CPU上におけるBlock Lanczos法の並列実装(A-7.情報セキュリティ,基礎・境界)
- 複数のSATソルバを用いたジョブショップスケジューリング問題の解法本論文では,ジョブショップ・スケジューリング問題(JSSP)に関して,JSSPを充足可能性判定問題(SAT)に変換することによる解法について考察する.JSSPをSATに変換する変換方法として,CrawfordとBakerによる変換を採用し,Javaにより実装した.この変換においてJSSPの期限が,変換後のSAT問題の変数と節数にどのように影響するかについて考察する.この変換の特徴として,期限が最適値に近いほど充足される変数の組み合わせが少なくなり,SAT問題として難しいものになるということが挙げられる.次に計算機実験により,期限を最適値を含む範囲で変化させたSAT問題を複数用意し,複数異種のSATソルバを並列に実行することができるMultisatにより解かせた.これにより,計算速度や有効に働くSATソルバの種類などのMultisatの特性を観察し,問題の難易度との関係を考察する.さらにMultisatと単体ソルバとの性能比較も行う.一般社団法人電子情報通信学会, 2004年06月14日, 電子情報通信学会技術研究報告. AI, 人工知能と知識処理, 104(133) (133), 19 - 24, 日本語
- 奈良工業高等専門学校, 2002年, 奈良工業高等専門学校研究紀要, (38) (38), 29 - 34, 日本語周波数解析を用いた日本語母音の特性に関する研究
- Workshop on Constraint Based Methods for Bioinformatics (co-located with ICLP 2010), 英語Finding Minimal Reaction Sets in Large Metabolic Pathways[査読有り]記事・総説・解説・論説等（学術雑誌）
- Poster presentation at: Systems Biochemistry 2010A SAT-based Method for Analyzing Metabolic Pathways[査読有り]
- 第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020), 2020年, 日本語, 日本ソフトウェア科学会 プログラミング論研究会, 国内会議正規制約に対するSAT符号化手法の提案と評価ポスター発表
- 第22回プログラミングおよびプログラミング言語ワークショップ (PPL 2020), 2020年, 日本語, 日本ソフトウェア科学会 プログラミング論研究会, 国内会議解集合ソルバーを用いた様相命題論理の充足可能性判定ポスター発表
- 日本ソフトウェア科学会第35回大会, 2018年08月, 日本語, 国内会議正規制約のSAT符号化とその性能評価ポスター発表
- 日本ソフトウェア科学会第35回大会, 2018年08月, 日本語, 国内会議SATソルバーを用いた様相命題論理S4の充足可能性判定ポスター発表
- The 28th International Conference on Automated Planning and Scheduling, (ICAPS 2018), 2018年06月, 英語, 国際会議teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming口頭発表（一般）
- DAシンポジウム2017, 2017年08月, 日本語, 情報処理学会システムとLSIの設計技術研究会, 山代温泉ゆのくに天祥, 国内会議SAT型制約ソルバーを用いた3次元ナンバーリンクの解法口頭発表（一般）
- 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), 2017年03月, 日本語, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), 国内会議解集合プログラミングを用いた多層ナンバーリンクの解法ポスター発表
- 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), 2017年03月, 日本語, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), 国内会議SugarTracer: SAT型制約ソルバーSugarのトレースツールポスター発表
- 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), 2017年03月, 日本語, 日本ソフトウェア科学会 プログラミング論研究会, 華やぎの章 慶山 (山梨県・笛吹市), 国内会議SATソルバーの最新動向と利用技術口頭発表（一般）
- DAシンポジウム2016, 2016年09月, 日本語, 情報処理学会 システムとLSIの設計技術研究会（SLDM）, ゆのくに天祥 (石川県・加賀市), 国内会議SAT型制約ソルバーを用いた多層ナンバーリンクの解法ポスター発表
- 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016), 2016年03月, 日本語, 日本ソフトウェア科学会プログラミング論研究会, 岡山県, 国内会議インクリメンタルSAT解法を用いた高速ナンバーリンクソルバーポスター発表
- 人工知能学会 第9回AIツール入門講座, 2015年12月, 日本語, 人工知能学会, 東京都, 国内会議SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー)[招待有り]口頭発表（招待・特別）
- 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015), 2015年03月, 日本語, 日本ソフトウェア科学会プログラミング論研究会, 愛媛県, 国内会議Scarab: 高度なSAT解法を利用可能な制約プログラミングシステムポスター発表
- 第16回プログラミングおよびプログラミング言語ワークショップ, 2014年03月, 英語, 日本ソフトウェア科学会プログラミング論研究会, 阿蘇の司ビラパークホテル, 国内会議Answer Set Programming as a Modeling Language for Course Timetabling口頭発表（一般）
- 日本ソフトウェア科学会第30回大会, 2013年09月, 日本語, 日本ソフトウェア科学会, 東京大学, 国内会議パッキング配列問題の制約モデリングとSAT符号化口頭発表（一般）
- 日本ソフトウェア科学会第30回大会, 2013年09月, 日本語, 日本ソフトウェア科学会, 東京大学, 国内会議Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について口頭発表（一般）
- The 4th International Workshop on Pragmatics of SAT, 2013年07月, 英語, PoS, University of Helsinki, Finland, 国際会議System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems口頭発表（一般）
- The 4th International Workshop on Pragmatics of SAT, 2013年07月, 英語, PoS, University of Helsinki, Finland, 国際会議PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding口頭発表（一般）
- The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Combined tool demo and poster session, 2013年07月, 英語, SAT, University of Helsinki, Finland, 国際会議CSPSAT Projects and their SAT Related Tools口頭発表（一般）
- 2013年度人工知能学会全国大会, 2013年06月, 日本語, 人工知能学会, 富山国際会議場, 国内会議正方形詰込み問題の制約モデルとSAT符号化を用いた解法口頭発表（一般）
- 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013), 2013年03月, 日本語, 日本ソフトウェア科学会, 東山温泉 御宿東鳳, 国内会議Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツールポスター発表
- The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks, 2012年11月, 英語, CRIL, NII, Université d'Artois, Lens, France, 国際会議Towards Incremental SAT-based CSP Solving: Experimental Results for the Hamiltonian Cycle Problem口頭発表（一般）
■ 共同研究・競争的資金等の研究課題
- 日本学術振興会, 科学研究費助成事業, 基盤研究(C), 神戸大学, 2022年04月01日 - 2025年03月31日制約充足問題に対する新しいSAT解法技術の研究開発
- 日本学術振興会, 科学研究費助成事業, 基盤研究(C), 名古屋大学, 2021年04月01日 - 2024年03月31日SAT技術に基づく系統的探索と確率的探索の統合的技法の研究開発近年，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%に大幅に改善することができた．さらに，提案手法の特長的なアプリケーションの開発に向けて，時間割問題に加え，配電網問題，車両装備仕様問題などへの応用研究も行なった． - 日本学術振興会, 科学研究費助成事業, 学術変革領域研究(B), 京都大学, 2020年10月02日 - 2023年03月31日工学アプローチによる組合せ遷移の展開：配電切替を足がかりとして汎用ソルバーへ本研究では組合せ遷移の実装技術の構築とその産業応用に向けて、研究開発の共通基盤となるソフトウェア開発を目標とする。初年度にあたる本年度は、広く知られているグラフの独立集合の遷移問題（独立集合遷移問題）に対して、4種のアプローチを検討した。1つ目は、組合せ遷移の技法を用いたアルゴリズムの設計であり、主に、状態空間の部分探索の手法を検討した。2つ目は、SAT（充足可能性問題）ソルバーを活用するアプローチである。有限整数領域上の制約を命題論理式へと変換する SAT 符号化を行い、SATソルバーの強力な推論性能を用いて独立集合遷移問題を解くソルバーを開発した。3つ目は、ゼロサプレス型二分決定グラフ (ZDD) を活用するアプローチである。当初予定では、ZDD を上記2手法に援用した高速化を想定していたが、本研究において、ZDD が表す独立集合族を直接遷移させるアルゴリズムの開発に成功したため、ZDD を単独で用いて独立集合遷移問題を解くことが可能になった。4つ目の手法は、当初は予定していない新たな構想であるが、モデル検査と呼ばれる、システムの形式的な検査を可能にする技術を用いた手法である。入力グラフと開始、目標独立集合が与えられた際に、開始集合から目標集合に遷移可能ではないことを検証する記述をモデル検査ソルバーに与え、遷移可能な場合は反例として解となる遷移列を出力する。 以上の4つの技法について、アルゴリズム設計と実装を行った。アルゴリズムの比較実験のためには、適切な入力データが必要であるが、組合せ遷移問題に対する広く知られたベンチマークデータは存在しないため、入力データの作成整備を行った。 配電切替への組合せ遷移技術の適用についても研究を行い、配電切替を全域木遷移問題として定式化し、4つの技法の適用を検討して、実装を行っている。
- 日本学術振興会, 科学研究費助成事業 基盤研究(C), 基盤研究(C), 神戸大学, 2020年04月01日 - 2023年03月31日MDDを用いたSAT型CSPソルバーの高速化近年， 命題論理式の充足可能性判定問題 (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), 2018年04月 - 2021年03月競争的資金
- 学術研究助成基金助成金／若手研究(B), 2016年04月 - 2019年03月, 研究代表者競争的資金
- 科学研究費補助金／基盤研究(B), 2016年04月 - 2019年03月競争的資金
- 学術研究助成基金助成金／基盤研究(C), 2015年04月 - 2018年03月競争的資金
- 文部科学省, 科学研究費補助金(若手研究(B)), 2013年 - 2015年, 研究代表者近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライ競争的資金
- 文部科学省, 科学研究費補助金(基盤研究(B)), 2012年 - 2014年当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進めた．「A. フレキシブル制約に関する研究開発」については，フレキシブル制約のSAT符号化で重要になる擬似ブール制約の符号化方法の研究，PBSugarシステムの開発，および論文発表を行った．「B. 動的な制約変更に関する研究開発」については，動的な制約変更が可能なScarabシステムの開発および論文発表を行った．「C. ドメイン拡張に関する研究開発」については，記号推論が可能な解集合プログラミングシステム上で整数上の制約記述を可能にするプロトタイプシステムを開発し，性能評価を行った．「D. 応用研究開発」については，各種問題の評価を進めた．特に，時間割問題について優れた結果を得，論文発表を行った．また，「論理と推論の理論，実装，応用に関する合同セミナー」のERATO競争的資金
- 日本学術振興会, 科学研究費助成事業, 特別研究員奨励費, 2010年 - 2011年SAT変換を用いた制約充足問題の解法とシステム生物学への応用最終年度の報告として、これまでの研究成果について以下にまとめる。 本研究では化学反応法則を満たしつつ入力代謝物集合から出力代謝物集合を生成可能なパスウェイを活性パスウェイ呼び、特にその包含関係において極小なものを極小活性パスウェイと呼ぶ。研究ではまず極小活性パスウェイを列挙する問題を極小活性パスウェイ同定問題として定義を行った。代謝パスウェイの解析を行う際には既存のデータから問題を構築する必要がある。そこで更新頻度において優れていることから、生物学的知識のデータベースEcoCyc(http://ecocyc.org/)から問題を構成して評価を行った。このデータから構成した問題をSAT技術によって解くために本研究では次の枠組みを用いた:(1)まず問題を命題論理式に符号化する、(2)SATソルバを漸増的に適用するインクリメンタルSAT解法を用いて符号化された命題論理式から極小モデルを計算する、(3)得られた極小モデルを逆符号化することで問題の解である極小活性パスウェイを得る。 提案した問題および解法の評価のためにEcoCycのデータから極小活性パスウェイ同定問題を構成し、SAT技術を用いて解を求めた。結果として9個の極小活性パスウェイを同定し、その中の2個が生物学における既存の知識と一致したパスウェイ(参照パスウェイ)であることを確認している。また専門家との議論で提案された制約を命題論理式に追加することでより精緻なパスウェイを計算することに成功した。この成果は国内雑誌論文として発表を行った。また代謝パスウェイに対する解集合プログラミングを用いた解析研究についても国際会議の会議録で発表を行った。 さらにより具体的な生物学の問題に適用するために、大腸菌における単一遺伝子ノックアウトの影響予測を極小活性パスウェイの同定によって行う手法の研究を国立遺伝学研究所の研究チームと共同して進めた。大腸菌の解糖系に対して計算機実験を行った結果,提案手法の予測が生物実験の結果とよく一致することを確認した。この成果は国際会議において発表を行った。
研究シーズ
■ 研究シーズ- SATソルバーを利用した制約プログラミングシステムの研究開発シーズカテゴリ：情報通信研究キーワード：充足可能性判定問題(SAT), 制約充足問題(CSP), 制約プログラミング, SATソルバー研究の背景と目的：命題論理式の充足可能性判定 (Satisfiability Testing; SAT) 問題を解くプログラムはSATソルバーと呼ばれ、2000年以降飛躍的にその性能を向上させてきました。そのようなSATソルバーの性能を利用するために、様々な問題をSAT問題に一度符号化してから解くというSAT型解法が近年注目を集めています。研究内容：論理に基づくプログラミング/ソフトウェアの研究をしています。この研究は実世界に多く現れる組合せ最適化問題にも応用ができます。具体な研究内容はSATソルバーを利用した制約プログラミングシステムの研究開発で、国内外の教育研究機関の研究者と共同で研究を行なっています。2018年には国際競技会の2部門で優勝するなど成果をあげることができました。期待される効果や応用分野：SATソルバーを応用した研究がこれまで多く報告されています。例えば，ジョブショップスケジューリング問題、パッキング問題、クラウド上のソフトウェア要素の最適配置問題、システム生物学における代謝経路解析などです。有限整数領域上の制約で記述できる問題はSATソルバーを用いた解法の適用を考えることができます。