R-SATCHMO: Refinements on I-SATCHMO.
Saved in:
| Title: | R-SATCHMO: Refinements on I-SATCHMO. |
|---|---|
| Authors: | He, Lifeng1 helifeng@ist.aichi-pu.ac.jp, Chao, Yuyan2 chao@nagoya-su.ac.jp, Itoh, Hidenori3 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 44441348 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: R-SATCHMO: Refinements on I-SATCHMO. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22He%2C+Lifeng%22">He, Lifeng</searchLink><relatesTo>1</relatesTo><i> helifeng@ist.aichi-pu.ac.jp</i><br /><searchLink fieldCode="AR" term="%22Chao%2C+Yuyan%22">Chao, Yuyan</searchLink><relatesTo>2</relatesTo><i> chao@nagoya-su.ac.jp</i><br /><searchLink fieldCode="AR" term="%22Itoh%2C+Hidenori%22">Itoh, Hidenori</searchLink><relatesTo>3</relatesTo><i> itoh@ics.nitech.ac.jp</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Apr2004, Vol. 14 Issue 2, p117-143. 27p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Backtrack+programming%22">Backtrack programming</searchLink><br /><searchLink fieldCode="DE" term="%22Young+tableaux%22">Young tableaux</searchLink><br /><searchLink fieldCode="DE" term="%22Pruning%22">Pruning</searchLink><br /><searchLink fieldCode="DE" term="%22Borel+sets%22">Borel sets</searchLink><br /><searchLink fieldCode="DE" term="%22Néron+models%22">Néron models</searchLink><br /><searchLink fieldCode="DE" term="%22Reasoning%22">Reasoning</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=44441348 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 27 StartPage: 117 Subjects: – SubjectFull: Backtrack programming Type: general – SubjectFull: Young tableaux Type: general – SubjectFull: Pruning Type: general – SubjectFull: Borel sets Type: general – SubjectFull: Néron models Type: general – SubjectFull: Reasoning Type: general Titles: – TitleFull: R-SATCHMO: Refinements on I-SATCHMO. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: He, Lifeng – PersonEntity: Name: NameFull: Chao, Yuyan – PersonEntity: Name: NameFull: Itoh, Hidenori IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 04 Text: Apr2004 Type: published Y: 2004 Identifiers: – Type: issn-print Value: 0955792X Numbering: – Type: volume Value: 14 – Type: issue Value: 2 Titles: – TitleFull: Journal of Logic & Computation Type: main |
| ResultId | 1 |
