2019 Fiscal Year Research-status Report
| Project/Area Number |
17K00098
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 投射モデル計数 / BDD / 変数順序 |
|---|
| Outline of Annual Research Achievements |
前年度に開発した投射モデル集合を表現するBDDやd-DNNFの構築ツールを量的情報流解析へ応用した研究成果が信学会論文誌に採録された。
令和元年度は主に、与えられた命題論理式の投射モデル集合を表現するBDD（以降，投射BDD）を構成するソルバにおいて、BDDの変数順序に関するヒューリスティクスを利用することによる効率に関する効果の調査を行った。投射モデルではない通常モデル集合を表現するBDD構築においては、適切な変数順序に基づいて構築することでBDDサイズの縮小および構築時間の短縮が可能であることが知られている。そこで、投射BDD構築においても、実行効率向上のため、既存の変数順序ヒューリスティクスの実装であるFORCEを利用することを考えた。我々の投射BDD構築ツールには、基としている投射モデル発見手法のために、投射変数が非投射変数よりも優先しなければならない制約がある。そのため、基本方針としてFORCEにより計算された変数全体における順序を基に、投射変数間と非投射変数間のそれぞれにおいて相対的な順序関係は保存しつつ、すべての投射変数はどの非投射変数より優先されるように変数順序の変更を行う前処理を実装し、評価を行った。通常のBDD構築同様に効率が向上することを予想していたが、結果として提案する変数順序変更によるサイズ・構築時間に大きな変化は得られなかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
研究代表者の長期海外派遣などにより、これまで開発してきたソルバと異なるタイプのソルバとの連携手法についての調査があまり進んでいない。また、BDD構築ソルバについては、当初想定していた変数順序変更による効率の向上が見られなかった。現在は、ソルバの空間計算量の見直しと、限られた時間内でモデル数の上界・下界を計算する手法についての研究課題に変更して取り組んでいる。
|
| Strategy for Future Research Activity |
昨年度に引き続き、我々の投射モデル計数ソルバと他の既存ソルバとの特徴の違いについて実験を通して調査し、それらのソルバの適切な連携方法について検討する。その過程として、阻止節を利用するタイプのソルバの開発と改良も行う。また、正確なモデル数を指定時間内に計算できない場合に、その時点までの計算結果から絞り込めるモデル数の上界・下界をなるべく正確に計算する手法の開発にも取り組む。
|
| Causes of Carryover |
本年度はあまり成果があげられておらず、加えて年度末に計画していた成果発表や研究調査の予定もなくなった。次年度に、本年度に予定していた課題において必要な計算機の購入や成果発表等に利用する予定である。
|
