Abstract
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 language | English |
|---|---|
| Pages (from-to) | 1596-1599 |
| Number of pages | 4 |
| Journal | WSEAS Transactions on Computers |
| Volume | 5 |
| Issue number | 7 |
| Publication status | Published - 2006 Jul 1 |
Keywords
- Automated reasoning
- Graph coloring problem
- Host list strategy
- Paramodulation
- Reducing CPU time
ASJC Scopus subject areas
- Computer Science(all)