定理証明器SATCHMOに関する新しい効率化手法(<特集>システムLSIの設計技術と設計自動化)

スポンサーリンク

概要

論文の詳細を見る
定理証明器SATCHMOではすべての違反節を前向き推論に用いるため,関連がない非ホーン違反節が存在する場合は探索空間の爆発を起こしてしまうこともある.その問題の解決には関連がある違反節だけを前向き推論に用いる方法がいくつか提案されている.本稿では,SATCHMOの効率化を図るための新しい手法を組み込んだI-SATCHMOを提案する.I-SATCHMOでは,SATCHMOと同様,最初に発見した違反節を前向き推論に用いる.ただし,実際の推論に貢献した違反節の頭部アトムを有用アトムとしてマークする.また,前向き推論に用いられる違反節が証明に必要とされるのはその節のすべての頭部アトムが有用であるときに限られる.そのため,I-SATCHMOは処理中の違反節のある頭部アトムが有用でないと判明したとき,その節に関する残りの処理をカットする.このように,無駄な推論を防止することによって,証明の効率化を実現している.
一般社団法人情報処理学会の論文
2002-05-15

著者

関連論文

もっと見る

スポンサーリンク