量的情報流解析のための投射モデル計数ソルバの開発

2017 Fiscal Year Research-status Report

• Project/Area Number: 17K00098
• Research Institution: Nagoya University
• Principal Investigator: 橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
• Project Period (FY): 2017-04-01 – 2020-03-31
• Keywords: 投射モデル計数 / 成分キャッシュ

Outline of Annual Research Achievements

平成２９年度は、命題論理式のモデル計数に関する既存技術の文献調査と、命題論理式の投射モデル計数における成分キャッシュの削除ヒューリスティクスについての実験調査を行った。これまでに、我々の研究グループでは与えられた命題論理式全体を真にする変数への真理値割当て（モデル）のうち、指定された変数集合に関して異なるモデルがいくつか存在するかを計数するソルバを開発している。その計数ソルバの中で、互いに独立した成分（部分CNF論理式）に動的に分割しながら、成分ごとの計数結果を組み合わせて全体のモデル数の計数を行っている。計数途中で同じ成分が複数回出現する場合があるため、計数が一度終了した成分についてはその結果を記憶し再利用することで高速化を図っている。しかしながら、成分キャッシュのために使用されるメモリ量は大きいため、適宜キャッシュの削減が必要となる。既存の計数ソルバでは、キャッシュサイズが一定値を超えたときに、単純に古いものから半分程度に削減するという方法が採用されている。本年度は、キャッシュ削減に関する知見を得るために、成分のサイズ（変数や節の数）や計数にかかった時間あるいはステップ数、キャッシュヒットの回数などを指標に、より効果的な削減ヒューリスティクスの検討を行った。残念ながら現状は検討するのに十分な実験が行えていないこともあり、有意に効果的な削減ヒューリスティクスの発見には至っていない。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

概要でも述べた通り、命題論理式の投射モデル計数における成分キャッシュの削除ヒューリスティクスの検討のための実験が十分に行えていない。実験の準備に手間取ってしまったことや予備実験と現状までの結果からは有益な知見が得られていない。また、成分キャッシュ部分の変更後に開発中のモデル計数ソルバの公開を想定していたがこちらもまだ準備中である。

Strategy for Future Research Activity

まず昨年度までに終了できなかった成分キャッシュの削除ヒューリスティクスの検討のための実験を引き続き行う。次に、モデル計数手法の１つである知識コンパイルを利用した方法について調査し、モデル計数がインクリメンタルに行われる場合など、論理式に部分的な変更が加えられる状況を想定した場合のモデル計数における有効性を調査する。また、プログラムの量的情報流解析のための、プログラムの事前解析とその結果に基づく計数戦略の検討を開始する予定である。

Causes of Carryover

昨年度に行う予定であった実験ではメモリ使用量が大きいものを想定していたが、現状ではまだそこまで規模が大きくない予備的な実験にとどまっている。予備実験の結果に応じて実験に必要となる計算機の選定を行う予定であったため、計算機の購入を次年度へと繰り越すこととした。