著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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)

著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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について述べる.

著者

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

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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: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)

巻号頁・発行日

2010

---

組合せテストは,ソフトウェアの信頼性・安全性を高めるためのソフトウェア検証手法の 1つである.本研究では,組合せテストのテストケース生成の性能向上を目指し,SAT ソルバー,制約ソルバー,解集合ソルバーを用いたテストケース自動生成ツールに関する研究開発を行った.提案手法を実装した 3つのツールは,組合せデザイン・ハンドブック等に記載されているベンチマークに対して,様々な既存手法で得られた既知の最良値を更新することに成功した.

著者

川谷 宗之 岡本 英彰 松田 一人 北川 哲 大西秀志 番原 睦則 田村 直之

出版者

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

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.46, no.6, pp.61-61, 2005-04-15

---

制約プログラミングとは,「ユーザは解決したい問題を制約の形で宣言的に記述するだけで,あとは制約解消系がその制約を満たす解を求めてくれる」という問題解決手法であり,近年注目を集めている.1990 年代には商用の制約解消系が登場し,これまで制約プログラミング手法に基づく生産スケジューリング,資源割当てなどの,実用的なシステムが開発されている.しかしながら,大規模な問題に対しては,制約解消系の処理に大きな計算量が必要とされるという問題がある.一方,近年の急速なネットワークインフラの高速化,普及を受けて新しい分散処理形態であるGrid が注目を集めている.我々の研究チームでは,Grid 計算環境に制約解消系を実装することでそのパフォーマンスを向上させることを目的とし,Grid に適した制約解消系の設計および実装を進めている.本発表では,その一環として実装を行ったGrid 計算環境上の2 つの制約解消系について述べる.まずSunGrid Engine(S.G.E.)上の制約解消系の実装,次にGlobus Toolkit を用いた制約解消系の実装について説明し,最後に,これらの制約解消系と単体計算機上の制約解消系を用いてパフォーマンス比較を行った結果を示す.ベンチマークにはよく知られているJob Shop Scheduling 問題などを用いた.得られた結果のうち,多くの場合において,今回の2 つの制約解消系が単体の計算機上の制約解消系より良い結果を示しており,制約解消系をGrid 計算環境上に実装することによる有効性は十分にあると結論付ける.In constraint programming, all you have to do is to define problems as sets of constraint declaratively, and then, constraint solvers search solutions. Commercial constraint solvers appeared in 1990s and have been used for production scheduling, resource allocation, and others. Constraint solving systems are useful but there are some issues. One of them is that they need much computational power to solve large scaled problems. Meanwhile, the Grid computing is a hot topic on the recent spread of the network infrastructure. In this presentation, we show some experimental results of two constraint solving systems on the Grid. We have developed these two systems on Sun Grid Engine and Globus Toolkit respectively. In each system, constraint solvers are implemented using Cream developed by our group. Cream is a Java class library for constraint programming and provides various optimization algorithms such as Simulated Annealing, Taboo Search, etc. We use Job Shop Scheduling Problem as benchmarks. In performance, our systems on the Grid gave nice speedup compared with Cream on a single machine.