Hot list strategy for faster paramodulation based graph coloring

Ruo Ando, Yoshiyasu Takefuji

研究成果: Article査読


In this paper, we discuss the effectiveness of applying the ATP (automated theorem proving) strategy called hot list strategy for N-coloring graph problem The process of graph coloring is formulated by equality substitution of paramodulation. It is showed that hot list strategy is useful to control the reasoning process driven by paramodulation. This ATP strategy are 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. Hot list strategy enables reasoning program to look ahead for faster resolution. In proposal graph coloring method, hot list strategy prevents paramodulation to generate much retained information thus reduce CPU time to reach the conclusion. Experiment shows that paramodulation could used for formulating graph coloring problem and hot list strategy is suitable for controlling paramoudlation based resolution. We measured CPU time and the number of generated clauses in solving coloring problem of Petersen graphs. Five kinds of Petersen graphs are formulated and processed by proposal theorem proving program.

ジャーナルWSEAS Transactions on Computers
出版ステータスPublished - 2006 7 1

ASJC Scopus subject areas

  • Computer Science(all)

フィンガープリント 「Hot list strategy for faster paramodulation based graph coloring」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。