| 研究課題/領域番号 |
26870011
|
|---|
| 研究機関 | 電気通信大学 |
|---|
研究代表者 |
戸田 貴久 電気通信大学, その他の研究科, 助教 (50451159)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | SATソルバー / ALLSAT / BDD / 論理関数の双対化 / 並列化 |
|---|
| 研究実績の概要 |
本研究では，極小ヒッティング集合の列挙問題(TRANS-ENUM)および関連する諸問題を計算する実用的技法の開発を目的としている.申請者は，TRANS-ENUMの実用的なアルゴリズム開発に携わり，二分決定グラフと呼ばれる圧縮データ表現に基づく計算法を提案した.本研究の構想は，様々な応用問題をTRANS-ENUMや関連する諸問題に帰着し，汎用的な計算基盤の上でそれらを統一的かつ効率的に処理するための枠組みを開発することである.
平成26年度の研究概要は以下の通りである.提案法の並列化：一般に，BDD/ZDD演算の並列化は困難であることが知られているが，単項演算に限定することで，提案法で用いられている単項演算を含む幅広い単項演算に対して，一般的な並列化の枠組みを与えることに成功した.
BDD構築法の解析：実用上効率的であると知られている，二分決定グラフを伴うほとんどの計算法に対して，効率性を理論的に評価する手立てはほとんど知られていない.本研究では，DNFが与えられ，BDDを構築する問題に対して，DNFを表現するZDDのセパレータサイズをパラメタとして用いる解析手法を開発した.
ALLSATソルバーの開発：TRANS-ENUM，DUALIZATIONなどを含む，より広いクラスの問題としてALLSATがある.本研究では，SATソルバーの強力な枝刈技法とBDDの強力なキャシング技法とを組み合せた新しいタイプのALLSATソルバーを開発した.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成26年度は，おおむね，当初予定していたとおりに研究が進んだ.具体的には，提案法の並列化に関しては，並列化アルゴリズムを開発し，国際会議論文（査読あり）として発表した.BDDサイズの解析に関しては，ZDDのセパレータサイズをパラメタとして評価し，国際会議論文（査読あり）として発表した.さらに，SATソルバーと二分決定グラフの技術を融合させるという新たな展開が得られた.開発した技術は国際会議論文（査読あり）として発表し，実装はインターネットで公開している.この研究は，TRANS-ENUMの関連問題として位置づけられ，平成27年度以降の研究を先行して実施した形となっている.今後予定している応用研究に向けて，企業の研究者との連携も進めた.
|
| 今後の研究の推進方策 |
平成26年度の研究成果として，TRANS-ENUMの関連問題の研究として，ALLSATソルバーの開発を行った.当初の計画では，TRANS-ENUMとその一般化であるDUALIZATIONを対象としていたが，研究を進めるうちに，ALLSAT問題の重要性を認識し，ALLSATソルバーの開発に着手した.TRANS-ENUMやDUALIZATIONはALLSATに一定の制限を加えたものと位置づけられるので，ALLSATを解くことで，より広い応用を見込めるようになる.TRANS-ENUMやDUALIZATIONに関してはすでに一定の成果が得られたので，今後の計画では，ALLSATソルバー自体の高速化，ALLSATに基づく応用研究に対してより注力していきたい.平成26年度から，国内外のSAT関係の研究会に参加し，最新の情報を収集するとともに，SAT関係者との交流を深めているので，平成27年度以降も同様の形で展開する予定である.
今後の課題は，開発したシステムを個別の応用問題に適用し，その効果を評価する必要がある.このために，有望な応用問題のサーベイを今後も進めていく.
|
| 次年度使用額が生じた理由 |
国際会議や国内出張が想定よりも少なかったため。研究成果発表としての出張は予定どおりだったが、情報収集や聴講目的での出張としての予定分が余ってしまった。
|
| 次年度使用額の使用計画 |
次年度以降，研究成果の発表，聴講，研究打合せなどのため出張費用として使用する.
|
| 備考 |
開発プログラムの公開
|
