Boosting complete techniques thanks to local search methods

In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge‐bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to gu...

Full description

Saved in:
Bibliographic Details
Published in:Annals of mathematics and artificial intelligence 1998-01, Vol.22 (3-4), p.319-331
Main Authors: Mazure, Bertrand, Saïs, Lakhdar, Grégoire, Éric
Format: Article
Language:English
Subjects:
Search methods
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge‐bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to guide the branching strategy of logically complete techniques like Davis and Putnam's one, giving rise to significant performance improvements, in particular when addressing locally inconsistent problems. Moreover, this approach appears very competitive in the context of consistent SAT instances, too.
ISSN:1012-2443
1573-7470
DOI:10.1023/A:1018999721141