節集合の対称性を利用したSATCHMOによる充足可能性判定

書誌事項

タイトル別名
  • セツシュウゴウ ノ タイショウセイ オ リヨウシタ SATCH
  • Testing the Satisfiability of a Clause Set by SATCHMO with Symmetry
  • 知識処理

この論文をさがす

抄録

ボトムアップ型の定理証明器としてこれまでにDavis?Putnam手続きやSATCHMOなどを考案されている.しかし,命問論理の充足可能性判定問題はNP完全であるため,いかに高性能な定理証明器を用いても問題のサイズが大きくなれば証明時間が爆発的に増大してしまう.大きな定理証明問題をこれ以上速く解くには,定理証明問題の持つ特性を利用しなくてはならない.そこで本研究では,ボトムアップ定理証明器SATCHMOへシンメトリ(対称性)の概念を導入する.また,単位リテラル規則・純リテラル規則を導入して命題節集合の縮小化を行う.さらに,実験により充足可能性の判定を効率良くできることを確認する.

The Davis-Putnam procedure and SATCHMO have worked out as efficient bottom-up propositional provers until now.However,it takes much time to solve large problems,because solving the satisfiablility problem of propositional calculus is NP-complete.Then,solving these problems quickly,we must utilize the characteristics of a given set of clauses.Therefore,we implement the symmetry finding method on the bottom-up prover SATCHMO and cut many branches of proof trees by symmetries.To implement this,we add One-literal rule and Pure-literal rule to SATCHMO(called SATCHMOST).Experimental results show that SATCHMOST has a good performance and can be used practically.

収録刊行物

参考文献 (8)*注記

もっと見る

キーワード

詳細情報

問題の指摘

ページトップへ