Hot list strategy for faster paramodulation based graph coloring

Ruo Ando, Yoshiyasu Takefuji

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Pages (from-to)1596-1599
Number of pages4
JournalWSEAS Transactions on Computers
Issue number7
Publication statusPublished - 2006 Jul 1


  • Automated reasoning
  • Graph coloring problem
  • Host list strategy
  • Paramodulation
  • Reducing CPU time

ASJC Scopus subject areas

  • General Computer Science


Dive into the research topics of 'Hot list strategy for faster paramodulation based graph coloring'. Together they form a unique fingerprint.

Cite this