Hot list strategy for faster paramodulation based graph coloring

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)1596-1599
Number of pages4
JournalWSEAS Transactions on Computers
Volume5
Issue number7
Publication statusPublished - 2006 Jul

Fingerprint

Coloring
Theorem proving
Program processors
Substitution reactions
Experiments

Keywords

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

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Hot list strategy for faster paramodulation based graph coloring. / Ando, Ruo; Takefuji, Yoshiyasu.

In: WSEAS Transactions on Computers, Vol. 5, No. 7, 07.2006, p. 1596-1599.

Research output: Contribution to journalArticle

@article{095aa9d7e7004e91932a8903a18b743b,
title = "Hot list strategy for faster paramodulation based graph coloring",
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.",
keywords = "Automated reasoning, Graph coloring problem, Host list strategy, Paramodulation, Reducing CPU time",
author = "Ruo Ando and Yoshiyasu Takefuji",
year = "2006",
month = "7",
language = "English",
volume = "5",
pages = "1596--1599",
journal = "WSEAS Transactions on Computers",
issn = "1109-2750",
publisher = "World Scientific and Engineering Academy and Society",
number = "7",

}

TY - JOUR

T1 - Hot list strategy for faster paramodulation based graph coloring

AU - Ando, Ruo

AU - Takefuji, Yoshiyasu

PY - 2006/7

Y1 - 2006/7

N2 - 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.

AB - 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.

KW - Automated reasoning

KW - Graph coloring problem

KW - Host list strategy

KW - Paramodulation

KW - Reducing CPU time

UR - http://www.scopus.com/inward/record.url?scp=33745485447&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33745485447&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:33745485447

VL - 5

SP - 1596

EP - 1599

JO - WSEAS Transactions on Computers

JF - WSEAS Transactions on Computers

SN - 1109-2750

IS - 7

ER -