著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.33, no.4, pp.4_16-4_29, 2016-10-25 (Released:2017-01-14)

---

近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.

著者

田村 直之 宋 剛秀 番原 睦則

雑誌

情報処理

巻号頁・発行日

vol.57, no.8, pp.710-715, 2016-07-15

---

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

著者

宋 剛秀 番原 睦則 田村 直之

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.34, no.1, pp.1_67-1_80, 2017-01-25 (Released:2017-03-25)

---

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

著者

番原 睦則 姜 京順 田村 直之 Mutsunori Banbara Kyoung-Sun Kang Naoyuki Tamura 奈良工業高等専門学校 釜山外国語大学校(韓国)コンピュータ電子工学部コンピュータ工学科 神戸大学工学部情報知能工学科 Nara National College of Technology Department of Computer Engineering Division of Electronic and Computer Engineering Pusan University of Foreign Studies Department of Computer and Systems Engineering Kobe University

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.18, no.1, pp.39-60, 2001-01-15

参考文献数

29

被引用文献数

4

著者

宋 剛秀 番原 睦則 田村 直之 鍋島 英知

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.4, pp.72-92, 2018-10-25 (Released:2018-12-26)

---

命題論理式の充足可能性判定(SAT)問題を解くプログラムであるSATソルバーは,2000年以降その性能面において飛躍的に進化した.それに伴い,解きたい問題をSAT符号化によりSAT問題へと変換し,SATソルバーを用いて解くSAT型システムが,プランニング,ソフトウェア・ハードウェア検証,スケジューリング問題など様々な分野で成功を収めるようになった.本稿では,まずSATソルバーの最新動向として,性能面と機能面における進化をその要因の1つであるSATソルバーの国際競技会の視点から説明を行う.次に SAT ソルバーの利用技術の視点から,SAT ソルバーの機能面の進化と符号化技術を組み合わせることで,複雑な問題を解くことが可能になることの説明を行う.そのような例として多目的最適化問題のパレート解をSATソルバーを利用して求める方法を説明する.

著者

田村 直之 番原 睦則

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.30, no.2, pp.2_83-2_89, 2013-04-25 (Released:2013-08-25)

著者

井上 克巳 田村 直之 Katsumi Inoue Naoyuki Tamura

出版者

人工知能学会

雑誌

人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence (ISSN:09128085)

巻号頁・発行日

vol.25, no.1, pp.57-67, 2010-01-01

参考文献数

56

被引用文献数

8

著者

松田 秀雄 田村 直之 小畑 正貴 金田 悠紀夫 前川 禎男

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.26, no.2, pp.296-303, 1985-03-15

---

試作マルチマイクロプロセッサシステム上への並列Prolog 処理系"k-Prolog"の実装とその評価について述べる.まずマルチプロセッサ上でProlog 処理系を実現するための並列実行モデルを与えそのモデルをもとにパイプライニング並列とOR 並列という二つの並列処理方式の記述を行う.パイプライニング並列とは後戻り処理のときに必要となる別解を他のプロセッサがあらかじめ求めておくもので解の求められる順番が逐次実行の場合と同じになるという特徴をもっている.OR並列とはゴール節中の述語からの入力節の呼出しを並列に行うものでデータベース検索等の問題に有効な方式だと考えられる.処理系の実装は筆者の所属する研究室で試作されたブロードキャストメモリ結合形並列計算機上に行った.これは16ビットマイクロプロセッサ8086をCPU にしており 共通バスにより結合されている.いくつかの例題プログラムを両並列処理方式で実行した結果 バイプライニング並列ではプロセッサ台数が小さいときに良好なデータが得られており実行プロセス数の急激な増大もなく安定している.OR 並列では全プロセッサ台数を通じて台数に比例した値に近い実行速度の向上が見られるが 実行プロセス数が急激に増大する場合があり大容量のメモリが必要となるという結論が得られている.

著者

番原 睦則 田村 直之 井上 克已

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.24, no.3, pp.3_75-3_86, 2007 (Released:2007-09-30)

---

本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,Prolog CafeはJavaとの連携,拡張性に優れたProlog処理系となっている.Prolog Cafeはマルチスレッドによる並列実行をサポートしており,スレッド間の通信は共有Javaオブジェクトにより実現される.また任意のJavaオブジェクトをPrologの項として取り扱う機能を有しており,Prologからメソッド呼び出し,フィールドへのアクセスも行える.最後にProlog Cafeの応用として,複数SATソルバの並列実行システムMultisatについて述べる.

著者

番原 睦則 田村 直之 井上 克巳

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.24, no.3, pp.75-86, 2007-07-26

被引用文献数

1

---

本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,PrologCafeはJavaとの連携,拡張性に優れたProlog処理系となっている.Prolog Cafeはマルチスレッドによる並列実行をサポートしており,スレッド間の通信は共有Javaオブジェクトにより実現される.また任意のJavaオブジェクトをPrologの項として取り扱う機能を有しており,Prologからメソッド呼び出し,フィールドへのアクセスも行える.最後にProlog Cafeの応用として,複数SATソルバの並列実行システムMultisatについて述べる.

著者

戸谷 友則 太田 耕司 岩室 史英 秋山 正幸 田村 直之

出版者

京都大学

雑誌

特定領域研究

巻号頁・発行日

2007

---

現在の最新宇宙論における重要問題はいくつかあるが、その最大のものは「宇宙のダークサイド(暗黒面)」という言葉で以下の三つにまとめることができる。すなわち、(1)宇宙を加速膨張させる「ダークエネルギー」、(2)宇宙の重力を支配する「ダークマター(暗黒物質)」、そして(3)宇宙の晴れ上がりから最初の天体形成と宇宙再電離をつなぐ「ダークエイジ(暗黒時代)」である。その中でも、ダークエネルギーは現代物理学の根源的な改訂につながる可能性すら秘めた、とくに重大な問題として認識されている。すばる望遠鏡の新観測装置FMOSを用いたバリオン振動探査計画により、このダークエネルギーに迫る事ができると期待されている。本研究の目的は、このバリオン振動探査計画のサーベイデザインを検討し、FMOS完成の際にすみやかに観測提案書を作成する準備を進める事にある。この目的のため、戸谷を中心に分光ターゲット銀河選定の手法や実現性を詳細にしらべた。「すばるディープフィールド」や、「すばるXMM-Newtonディープフィールド」と呼ばれる領域のすばる望遠鏡を中心とする膨大なデータをもとに、バリオン振動探査に使用できる銀河が十分に存在するかどうかを精査した。その結果、バリオン振動探査に十分な数の銀河があり、また、イメージングサーベイデータから測光的赤方偏移計算の手法により効率よく選択できる事も判明した。また、メンバーがハワイに集まってミーティングを開催し、FMOS装置に対する理解を深めるとともに、今後の問題点を洗い出して計画の推進に役立てた。国際的な注目も高く、国際会議で進捗状況を報告した。

著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.3, pp.3_65-3_78, 2018-07-25 (Released:2018-09-25)

---

本論文では,擬似ブール (Pseudo-Boolean; PB)制約の集合を命題論理式の充足可能性判定 (SAT)問題へ符号化する新しい手法として,ブール基数 (Boolean Cardinality; BC)制約を経由する方法を提案する.提案手法は,次の3つの特徴を持つ. 1つ目は,SATソルバーの単位伝播により一般化アーク整合性の維持が可能な点である. 2つ目は,同じ解を持つ同値なPB制約であれば係数や右辺の値が異なっても,同一の中間表現およびSAT問題に符号化可能な点である. 3つ目は,項数に対して係数の種類が少ないPB制約に対しては,中間表現が簡潔になり少ない節数でSAT符号化可能な点である.このようなPB制約は,国際PBソルバー競技会のベンチマーク問題にも頻出している.計算機実験では,代表的な既存手法で一般化アーク整合性維持が可能なBDD法,およびそれより弱い整合性検査が可能なSorter法と符号化後の節数と求解性能を比較した.結果として,異なる係数の種類が10%以下であるようなPB制約について,提案手法が節数と求解性能に関して比較した2手法よりも良いことを確認した.

著者

竹内 頼人 田村 直之 番原 睦則

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会全国大会論文集

巻号頁・発行日

vol.2021, pp.1H4GS1c03, 2021

---

<p>車両装備仕様とは,簡単に言うと,自動車のカタログに記載されているモデル/グレードと装備の組合せのことである.多目的車両装備仕様問題は,与えられたモデル/グレードの個数,装備タイプの集合,装備オプションの集合などから,装備および燃費に関する制約を満たしつつ,予想販売台数の最大化や装備オプション数の最小化など,トレードオフの関係にある複数の目的関数のもとで最適な車両装備仕様を求める問題である.本発表では,CAFE 方式と呼ばれる燃費制約に基づく多目的車両装備仕様問題(多目的 CAFE 問題)に対して,解集合プログラミングを用いてパレート最適解を列挙する方法について述べる.提案手法は,可変性モデルで表現された問題インスタンスを ASP のファクト形式に変換した後,それらファクトと多目的CAFE 問題を解くための ASP 符号化と結合し,高速 ASP システムを用いて解を求める.企業から提供されたベンチマーク問題を用いた実行実験の結果,小規模な問題についてパレート最適解を全列挙することができた.</p>

著者

番原 睦則 田村 直之 Mutsunori Banbara Naoyuki Tamura

雑誌

人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence (ISSN:09128085)

巻号頁・発行日

vol.25, no.1, pp.122-129, 2010-01-01

著者

船越 泰輔 番原 睦則 田村 直之

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会全国大会論文集 第26回全国大会(2012)

巻号頁・発行日

pp.1E3OS42, 2012 (Released:2018-07-30)

---

本論文では,ハミルトン閉路問題を命題論理の充足可能性判定問題 (SAT)に符号化し解く新しい方法を提案する.提案手法の特徴は,閉 路が単一である条件を符号化せず,複数の閉路が求まるたびにその 否定の条件を追加する方法を用いている点にある.このようなイン クリメンタルSAT解法を導入することにより,SAT技術を用いた既存 手法よりも優れた性能を示すことが確認できた.

著者

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

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.59, no.9, pp.1749-1760, 2018-09-15

---

本論文では,トークン数が整数値である一般のペトリネットを対象とし,そのデッドロック検出についてSAT技術を用いた手法を提案する.提案手法では,非負整数値であるトークン数を表現するために順序符号化を採用することで,既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した.また,既存SAT型手法で採用されていたモデル(連続発火モデルと呼ぶ)よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し,性能向上を実現した.評価実験では,Model Checking Contest 2017のベンチマーク問題を用いて,連続発火モデルと多重発火モデルを比較した.ほぼすべての問題で多重発火モデルのほうが優れていたが,特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった.また,Model Checking Contest 2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った.提案手法は,デッドロックを検出できた問題数ではLoLA,Tapaalより少なかったが,LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し,提案手法の有効性が確認できた.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.

著者

松中 春樹 丹生 智也 番原 睦則 田村 直之

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会論文誌 (ISSN:13460714)

巻号頁・発行日

vol.27, no.2, pp.10-15, 2012 (Released:2012-01-13)

参考文献数

15

---

Propositional Satisfiability (SAT) is fundamental in solving many application problems in Artificial Intelligence and Computer Science. Remarkable improvements in the efficiency of SAT solvers have beenmade over the last decade. Such improvements encourage researchers to solve constraint satisfaction problems by encoding them into SAT (i.e. ``SAT encoding''). Balanced Incomplete Block Design (BIBD) is one of the most typical block designs. BIBDs have been applied in several fields such as design experiments, coding theory, and cryptography. In this paper, we consider the problem of generating BIBDs by SAT encoding. We present a new SAT encoding that is an enhancement of order encoding with the idea of binary tree. It is designed to reduce the number of clauses required for cardinality constraints, compared with order encoding. In our experiments, our encoding was able to give a greater number of solutions than order encoding and state-of-the-art constraint solvers Mistral and choco.

著者

松田 秀雄 田村 直之 小畑 正貴 金田 悠紀夫 前川 禎男

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.26, no.2, pp.296-303, 1985-03-15

---

試作マルチマイクロプロセッサシステム上への並列Prolog 処理系"k-Prolog"の実装とその評価について述べる.まずマルチプロセッサ上でProlog 処理系を実現するための並列実行モデルを与えそのモデルをもとにパイプライニング並列とOR 並列という二つの並列処理方式の記述を行う.パイプライニング並列とは後戻り処理のときに必要となる別解を他のプロセッサがあらかじめ求めておくもので解の求められる順番が逐次実行の場合と同じになるという特徴をもっている.OR並列とはゴール節中の述語からの入力節の呼出しを並列に行うものでデータベース検索等の問題に有効な方式だと考えられる.処理系の実装は筆者の所属する研究室で試作されたブロードキャストメモリ結合形並列計算機上に行った.これは16ビットマイクロプロセッサ8086をCPU にしており 共通バスにより結合されている.いくつかの例題プログラムを両並列処理方式で実行した結果 バイプライニング並列ではプロセッサ台数が小さいときに良好なデータが得られており実行プロセス数の急激な増大もなく安定している.OR 並列では全プロセッサ台数を通じて台数に比例した値に近い実行速度の向上が見られるが 実行プロセス数が急激に増大する場合があり大容量のメモリが必要となるという結論が得られている.

著者

田村 直之 丹生 智也 番原 睦則

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.27, no.4, pp.4_183-4_196, 2010-10-26 (Released:2010-12-26)

---

本論文では,SAT変換に基づく制約ソルバーであるSugarの概要とその性能評価結果について述べる.Sugarは,制約充足問題(CSP),制約最適化問題(COP)および最大制約充足問題(Max-CSP)を,命題論理の充足可能性判定問題(SAT問題) に変換し,MiniSat等の高速なSATソルバーを用いて求解を行うシステムである.SAT変換には,order encodingと名付けた新しい方法を用いており,従来広く用いられているdirect encodingやsupport encodingよりも,多くの問題に対して高速な求解が可能である.本論文では,order encodingの説明を含めたSugarの概要について述べた後,2008年に開催された第3回国際CSPソルバー競技会およびMax-CSPソルバー競技会での結果を基にSugarの性能評価結果を報告する.なお,Sugarは同競技会の10部門のうち4部門で第1位となった.

著者

岡田 光弘 小林 直樹 照井 一成 田村 直之

出版者

慶應義塾大学

雑誌

基盤研究(B)

巻号頁・発行日

2003

---

次の3点を中心に研究を進めた。1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。