著者

安藤類央 武藤佳恭

出版者

一般社団法人情報処理学会

雑誌

情報処理学会研究報告数理モデル化と問題解決(MPS) (ISSN:09196072)

巻号頁・発行日

vol.2006, no.29, pp.77-80, 2006-03-17

---

本論文では、N色グラフ彩色可能判定問題に関して、パラモジュレーション(等号調整導出)をベースにした定理証明に、Hot List Strategyと呼ばれる計算戦略を適用することの有効性を示す。同計算戦略を用いると、等価代入の手法によっては目的する節が導出される前に冗長な節生成が起きる場合について、冗長な節の生成(遅延)によるCPU時間の削減を行うことが可能になる。グラフのN彩色判定問題において、等号調整導出による推論が適用できること、さらに等号調整導出の推論プロセスは、Hot List Strategyに対して効果的な適合をすることを示した。評価実験では、非ハミルトングラフであるぺテルセングラフを対象にし、彩色判定の際の生成節数やCPU時間を測定し、その結果推論の遅延と計算コストを削減できることが明らかになった。In this paper, we discuss the effectiveness of applying hot list strategy for paramodulation based N-coloring graph problem. This ATP (automated theorem proving) strategy reduces is designed to deal with a substantial delay in going to a retained conclusion, which makes it possible to reduce the CPU time occurred by redundant generated clauses. We show that paramodulation could used for formulating graph coloring problem and hot list strategy is suitable for controlling paramoudlation based resolution. In experiment, CPU time and the number of generated clauses is presented in solving coloring problem of Petersen graphs.