New implementation technique for model generation theorem provers to solve constraint satisfaction problems

Ryuzo Hasegawa, Hiroshi Fujita

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multi-environment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.

Original languageEnglish
Pages (from-to)57-62
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume4
Issue number1
Publication statusPublished - Mar 1 1999

Fingerprint

Constraint satisfaction problems
Restoration
Data structures
Chemical activation

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Cite this

@article{3c3726feb81c4d9cbfcb4bff1fca7c5a,
title = "New implementation technique for model generation theorem provers to solve constraint satisfaction problems",
abstract = "A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multi-environment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.",
author = "Ryuzo Hasegawa and Hiroshi Fujita",
year = "1999",
month = "3",
day = "1",
language = "English",
volume = "4",
pages = "57--62",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "1",

}

TY - JOUR

T1 - New implementation technique for model generation theorem provers to solve constraint satisfaction problems

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

PY - 1999/3/1

Y1 - 1999/3/1

N2 - A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multi-environment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.

AB - A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multi-environment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.

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

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

M3 - Article

AN - SCOPUS:0032674972

VL - 4

SP - 57

EP - 62

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

SN - 1342-3819

IS - 1

ER -