R-SATCHMO: Refinements on I-SATCHMO.

Saved in:

Bibliographic Details
Title:	R-SATCHMO: Refinements on I-SATCHMO.
Authors:	He, Lifeng¹ helifeng@ist.aichi-pu.ac.jp, Chao, Yuyan² chao@nagoya-su.ac.jp, Itoh, Hidenori³ itoh@ics.nitech.ac.jp
Source:	Journal of Logic & Computation. Apr2004, Vol. 14 Issue 2, p117-143. 27p.
Subjects:	Backtrack programming, Young tableaux, Pruning, Borel sets, Néron models, Reasoning
Abstract:	In this paper, three refinements on I-SATCHMO are presented. I-SATCHMO is an application of the backjumping strategy for SATCHMO, which is a model generation theorem prover and is formalized as positive unit hyperresolution tableaux, to pruning away redundant branches. However, I-SATCHMO does not completely implement backjumping. Since marking an atom as useful whenever it contributes to a forward chaining reasoning, I-SATCHMO suffers from two problems. One is that the atoms that only contribute to irrelevant forward chaining reasoning are marked as ‘useful’. The other is that the atoms that are only useful for the sibling branches of the branch under consideration are taken as ‘useful’ for the branch. In both cases, I-SATCHMO might take some irrelevant violated clauses as ‘relevant’ and therefore use them to expand the search space. Moreover, not utilizing the partial reasoning results derivable during reasoning, I-SATCHMO might make repeated reasoning. Addressing these problems, our extension, called R-SATCHMO, refines I-SATCHMO in three ways: (1) only making the atoms that contribute to relevant forward chaining reasoning as useful; (2) it distinguishes between the set of useful atoms in different branches of a proof tree; (3) it summarizes the derived refutations as nogoods and utilizes them to avoid repeated reasoning. Hence, R-SATCHMO always searches a subspace of that which I-SATCHMO does. R-SATCHMO is optimal in the sense that during reasoning no same complete subtree is constructed in a proof tree. Moreover, R-SATCHMO can be used to generate minimal unsatisfiable subsets of an unsatisfiable set of clauses, and the strategies proposed in R-SATCHMO are applicable to minimal model generation procedures. We describe our refinements, present our implementation, prove the correctness, provide examples to demonstrate the power of our refinements, and discuss the application to minimal model generation. [ABSTRACT FROM PUBLISHER]
	Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	In this paper, three refinements on I-SATCHMO are presented. I-SATCHMO is an application of the backjumping strategy for SATCHMO, which is a model generation theorem prover and is formalized as positive unit hyperresolution tableaux, to pruning away redundant branches. However, I-SATCHMO does not completely implement backjumping. Since marking an atom as useful whenever it contributes to a forward chaining reasoning, I-SATCHMO suffers from two problems. One is that the atoms that only contribute to irrelevant forward chaining reasoning are marked as ‘useful’. The other is that the atoms that are only useful for the sibling branches of the branch under consideration are taken as ‘useful’ for the branch. In both cases, I-SATCHMO might take some irrelevant violated clauses as ‘relevant’ and therefore use them to expand the search space. Moreover, not utilizing the partial reasoning results derivable during reasoning, I-SATCHMO might make repeated reasoning. Addressing these problems, our extension, called R-SATCHMO, refines I-SATCHMO in three ways: (1) only making the atoms that contribute to relevant forward chaining reasoning as useful; (2) it distinguishes between the set of useful atoms in different branches of a proof tree; (3) it summarizes the derived refutations as nogoods and utilizes them to avoid repeated reasoning. Hence, R-SATCHMO always searches a subspace of that which I-SATCHMO does. R-SATCHMO is optimal in the sense that during reasoning no same complete subtree is constructed in a proof tree. Moreover, R-SATCHMO can be used to generate minimal unsatisfiable subsets of an unsatisfiable set of clauses, and the strategies proposed in R-SATCHMO are applicable to minimal model generation procedures. We describe our refinements, present our implementation, prove the correctness, provide examples to demonstrate the power of our refinements, and discuss the application to minimal model generation. [ABSTRACT FROM PUBLISHER]
ISSN:	0955792X