| 研究課題/領域番号 |
26870011
|
|---|
| 研究機関 | 電気通信大学 |
|---|
研究代表者 |
戸田 貴久 電気通信大学, その他の研究科, 助教 (50451159)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | AllSAT / モデル列挙 / 二分決定グラフ / SATソルバー / 論理関数の双対化 |
|---|
| 研究実績の概要 |
論理関数の双対化は、論理式の表現形式の変換（CNF-DNF変換）の一種であり、昔からよく研究されてきた基本的な問題である。ただ、この分野では、実用性を重視する最近の研究がほとんどないため、本研究で推進する必要があると考え、取り組んだ。平成27年度は、複数の既存アルゴリズムの実装、追加実験、論文改訂などを行った。実装コードをすべて公開している。
極小ヒッティング集合の列挙問題や論理関数の双対化問題を含むより広いクラスの問題であるAll Solutions SAT問題（AllSAT問題）に取り組んだ。AllSAT問題は、計算機科学において最も重要な問題の一つとしてみなされている充足可能性問題（SAT）の派生問題としても位置づけられる。SAT問題を解くソフトウェア（SATソルバー）の開発は世界的に活発に行われている。それに比べてAllSATは、モデル検査などの重要な応用があるにもかかわらずあまり研究されていない。AllSAT問題のアルゴリズムは体系的に整理されておらず、実装は公開されていなかった。そこで、従来研究を世界に先駆けて体系的に整理した。また、体系化の過程において、これまで盲点となっていた複数の新手法も提案した。主要な全てのアルゴリズムを実装した（全２８種類）。SATソルバーの評価のために共通して用いられる数千ものデータを用いた大規模な評価実験を行った。これにより、はじめて、ソルバーごとの特性や実用上効率的なソルバーが明らかになり、現在までのAllSAT研究の全貌が明らかになった。サーベイ論文としてまとめて論文誌に投稿した（現在査読されている）。実装したコードおよび関連情報をまとめたウェブサイトAll Solutions SAT Repository（http://www.sd.is.uec.ac.jp/toda/code/allsat.html）を公開している。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成26年度の研究を踏まえて、平成27年度はヒッティング集合の列挙の派生問題の一つであるAllSAT問題に取り組むことを計画していた。AllSATに関する従来研究の調査などを進めるうちに、この分野が十分体系的に整理されていないこと、従来手法の実装がまったく公開されていないことなどの問題が明らかになったので、本年度は新しいAllSAT技術の研究を進める前に従来のAllSAT研究の体系化を試みた。この結果をサーベイ論文にまとめ、実装コードや関連情報などをウェブサイトで公開した。これにより、現在までのAllSAT研究の全貌、そして最先端が明らかになった。そしてAllSAT研究をさらに発展させていくための基礎をしっかり固めることができた。
|
| 今後の研究の推進方策 |
AllSAT研究の体系化に一区切りが付いたので、今後はこれまでの基礎の上にAllSAT研究をさらに発展させていきたい。今後の方針としては、最新のAllSATアルゴリズムを応用問題に適用することを目指したい。このために、従来から知られている各種の応用に最新技法を適用することを検討している。また、新たなAllSAT応用についても探求したい。
別の方向としては、全ての解を列挙することに縛られないで、例えば出来るだけ多くの多様な解を計算することや、何らかの評価尺度に関して上位k個を計算することなどのような関連問題にも取り組みたい。これにより、応用分野のニーズに即した汎用的な計算基盤を提供していきたい。
より応用に近い研究となるため、各種研究会や国内外の会議などに参加して、最新のトレンドを把握するとともに、様々な分野の研究者との交流・議論を進めていきたい。また、応用分野に詳しい共同研究者と適宜協力して研究を進めていきたい。
|
| 次年度使用額が生じた理由 |
本年度の研究成果を論文誌にまとめたが、その英文校正費用や投稿料は次年度に必要となる予定である。
|
| 次年度使用額の使用計画 |
論文誌の英文校正費および投稿料（オープンアクセスのための追加費用含む）
|
