|
令和2年度は、主に（１）命題論理式の投射モデル集合を表現するBDD（以降、投射BDD）を構成するソルバpc2bddの改良と、（２）阻止節追加型投射モデル計数法の実装と阻止節縮小法の効果の評価を行った。
（１）投射BDDを構成するソルバpc2bddの性能向上のため、基盤SATソルバの変更とBDD構築途中での簡約化の実装を行った。本ソルバが基にしたcnf2obdd同様に基盤となるSATソルバは minisat v1.14であったが、今回鍋島らによって開発された高速なSATソルバ glueminisat をベースに新たに実装しなおした。また、前実装では、構築途中にメモリ不足が原因でBDD構築を完了できないケースが多く発生していた。構築途中のBDDサイズが膨らんでいることが主な原因と考えられたため、構成途中のBDDを簡約化された状態で維持するようにした。これによりメモリ不足になったケースでもBDD構築が可能となった。以上の成果について人工知能学会人工知能基本問題研究会にて報告した。
（２）我々がこれまでに開発してきた成分分割・キャッシュを利用したソルバGPMCとBDDを利用したpc2bdd以外のソルバとして、阻止節追加型投射モデル計数法の実装を glueminisat をベースに試作を行った。そして、阻止節（見つかったモデルの否定を表す節）を追加する際にその節から冗長なリテラルを取り除く手法を投射モデル計数において利用できるように改良を行った。阻止節の増加や縮小化にかかるコストの影響が無視できないため他ソルバと比べて一長一短があるものの、高速に解けるCNF式が存在することを確認できた。
|
