田村 直之 Tamura Naoyuki

Articles:  1-20 of 120

  • Studies on a Parallelization Method of SAT-based CSP Solvers using CEGAR and the Share of Counterexamples  [in Japanese]

    宋 剛秀 , 鍋島 英知 , 番原 睦則 , 田村 直之 , 井上 克巳

    人工知能基本問題研究会 112, 6-11, 2020-03-08

  • Satisfiability Testing of Propositional Modal Logic K with Answer Set Programming  [in Japanese]

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

    <p>様相命題論理の体系Kについて,与えられた論理式の充足可能性を判定する新しい手法を提案する.提案する手法はタブロー法に基づいており,解集合プログラミングを用いて実装されている.タブロー法に基づいた既存手法では,可能世界を最初にすべて生成してから充足可能性判定を行う方法か,可能世界を幅優先的に順次拡大しながら充足可能性判定を繰り返し行う方法が取られている.提案するシステムでは,これら …

    Proceedings of the Annual Conference of JSAI JSAI2020(0), 2N5OS17b05-2N5OS17b05, 2020

    J-STAGE 

  • Proposal of encoding alldifferent constraints to Boolean cardinality constraints and its evaluation on queen graph coloring problems  [in Japanese]

    大野 周亮 , 番原 睦則 , 宋 剛秀 , 田村 直之

    人工知能基本問題研究会 109, 6-11, 2019-03-13

  • A SAT-based CSP Solver sCOP and its Results on 2018 XCSP3 Competition  [in Japanese]

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

    <p>制約充足問題 (CSP) は, 与えられた制約を全て充足する値割当てを求める問 題である. CSP には, 人工知能およびオペレーションズ・リサーチにおける幅 広い応用がある. XCSP3 は, CSP を記述できる主要な制約言語の1つであり, 105種類2万3千問を超える問題例が XCSP3 のデータベースから利用可能である. また2018年には, XCSP3ソルバーの国際競技 …

    Proceedings of the Annual Conference of JSAI JSAI2019(0), 1E2OS3a03-1E2OS3a03, 2019

    J-STAGE 

  • Optimal Configuration based on Constraint Programming for Wireless Mesh Networks with Multi-Interface in IEEE802.11 Infrastructure Mode  [in Japanese]

    高橋 智輝 , 前野 誉 , 高木 由美 , 鎌田 十三郎 , 太田 能 , 田村 直之

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 118(316), 17-22, 2018-11-22

  • Proposal of SAT-based Method to Detect Deadlock of Petri Nets  [in Japanese]

    寸田 智也 , 宋 剛秀 , 番原 睦則 , 田村 直之 , 井上 克巳

    本論文では,トークン数が整数値である一般のペトリネットを対象とし,そのデッドロック検出についてSAT技術を用いた手法を提案する.提案手法では,非負整数値であるトークン数を表現するために順序符号化を採用することで,既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した.また,既存SAT型手法で採用されていたモデル(連続発火モデルと呼ぶ)よりも短いステップ長でデッドロッ …

    情報処理学会論文誌 59(9), 1749-1760, 2018-09-15

    IPSJ  IR 

  • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints  [in Japanese]

    南 雄之 , 宋 剛秀 , 番原 睦則 , 田村 直之

    本論文では,擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として,ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する.提案手法は,次の3つの特徴を持つ. 1つ目は,SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である. 2つ目は,同じ解を持つ同値なPB制約であ …

    コンピュータソフトウェア = Computer software 35(3), 65-78, 2018-08

    IR 

  • LSI Routing Problem - Routing Problem Solver Contest at DA Symposium -:3. Problem Solving with SAT Technologies  [in Japanese]

    松永 裕介 , 田村 直之

    本稿ではSATソルバーを用いて配線問題を解く手法について解説を行う.まず,配線問題をグラフ上の経路探索問題と見なし,どの枝が経路として用いられているかを表す命題変数を導入することで,配線問題を命題論理式に変換する.変換された命題論理式がSATソルバーによって充足可能と判定された場合には,充足可能な割り当て結果から1となっている変数に対応する枝を得ることにより最終的な配線結果を得ることができる.SA …

    情報処理 59(3), 232-238, 2018-02-15

    IPSJ 

  • Recent Advances in SAT Solvers and their Utilization Technologies.  [in Japanese]

    SOH Takehide , BANBARA Mutsunori , TAMURA Naoyuki , NABESHIMA Hidetomo

    <p>命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最 …

    Computer Software 35(4), 72-92, 2018

    IR  J-STAGE 

  • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints  [in Japanese]

    MINAMI Yushi , SOH Takehide , BANBARA Mutsunori , TAMURA Naoyuki

    本論文では,擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として,ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する.提案手法は,次の3つの特徴を持つ. 1つ目は,SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である. 2つ目は,同じ解を持つ同値なPB制約であ …

    Computer Software 35(3), 3_65-3_78, 2018

    J-STAGE 

  • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints  [in Japanese]

    南 雄之 , 宋 剛秀 , 番原 睦則 , 田村 直之

    日本ソフトウェア科学会大会論文集 34, 393-404, 2017-09-18

  • A SAT Encoding of Pseudo-Boolean Constraints via Boolean Cardinality Constraints  [in Japanese]

    南 雄之 , 宋 剛秀 , 番原 睦則 , 田村 直之

    人工知能基本問題研究会 103, 18-23, 2017-03-13

  • SAT-based Constraint Programming Systems and Related Technologies  [in Japanese]

    宋 剛秀 , 番原 睦則 , 田村 直之

    コンピュータソフトウェア = Computer software 34(1), 67-80, 2017-02

  • Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings

    Soh Takehide , Banbara Mutsunori , Tamura Naoyuki

    This paper proposes a new hybrid encoding of finite linear CSP to SAT which integrates order and log encodings. The former maintains bound consistency by unit propagation and works well for constraint …

    International Journal on Artificial Intelligence Tools 26(1), 1760005, 2017-02

    IR 

  • 制約充足問題のASP符号化に関する一考察  [in Japanese]

    坡山 直樹 , 番原 睦則 , 宋 剛秀 , 田村 直之

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

    Proceedings of the Annual Conference of JSAI JSAI2017(0), 1M1OS02a4-1M1OS02a4, 2017

    J-STAGE 

  • SAT技術を用いたペトリネットのデッドロック検出手法の提案  [in Japanese]

    寸田 智也 , 宋 剛秀 , 番原 睦則 , 田村 直之

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

    Proceedings of the Annual Conference of JSAI JSAI2017(0), 1M1OS02a2-1M1OS02a2, 2017

    J-STAGE 

  • SAT-based Constraint Programming Systems and Related Technologies  [in Japanese]

    SOH Takehide , BANBARA Mutsunori , TAMURA Naoyuki

    近年SATソルバーの求解性能が飛躍的に向上しており,様々な分野で応用が進んでいる.しかし,SATソルバーは連言標準形の命題論理式を入力としており,実用的な応用が多くある算術制約を含むような問題を直接記述して解くことには向いていない.このため,より表現力のある入力形式に対応できるようにSATソルバーを利用・拡張したシステムが研究されている.本解説では,そのような利用・拡張の1つとしてSATソルバーの …

    Computer Software 34(1), 1_67-1_80, 2017

    J-STAGE 

  • Proposal of a SAT-based Method to Detect Deadlocks of Ordinary Petri Nets  [in Japanese]

    寸田 智也 , 宋 剛秀 , 番原 睦則 , 田村 直之

    日本ソフトウェア科学会大会論文集 33, 513-521, 2016-09-07

  • SAT Evolution and Applications:2. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver -  [in Japanese]

    田村 直之 , 宋 剛秀 , 番原 睦則

    数独やナンバーリンクなどのパズルを題材として取り上げ,SATソルバーを用いてこれらのパズルを解く方法について説明する.SATソルバーは,与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである.近年になって大幅な性能向上が実現され,最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている.このことを背景とし,さまざまな問題をCNF式に変換(符号化) しSA …

    情報処理 57(8), 710-715, 2016-07-15

    IPSJ 

  • Solving Optimal Software Component Configuration Problem in Cloud  [in Japanese]

    田村 直之 , 井上 克巳 , 鍋島 英知 , 番原 睦則 , 宋 剛秀

    人工知能基本問題研究会 100, 19-24, 2016-03-27

Page Top