ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique

APPEL À
CONTRIBUTION
Masses de données hétérogènes
En savoir plus >>
Autres revues >>

Revue d'Intelligence Artificielle

0992-499X
Revue des Sciences et Technologies de l'Information
 

 ARTICLE VOL 22/2 - 2008  - pp.161-181  - doi:10.3166/ria.22.161-181
TITRE
Extraction d'ensembles minimaux incohérents basée sur la recherche locale

RÉSUMÉ
SAT est probablement l'un des problèmes de satisfaction de contraintes les plus étudiés. Dans cet article, une nouvelle technique pour l'approximation et l'extraction d'ensembles minimaux incohérents de clauses (MUS) au sein d'instances SAT insatisfiables est présentée. Elle est basée sur une heuristique originale de comptage qui, greffée à une recherche locale, explore un voisinage partiel de l'interprétation courante d'une manière nouvelle, en utilisant le concept de clause critique. Intuitivement, une clause critique est une clause falsifiée qui ne devient satisfaite par un « flip » de la recherche locale que si une autre clause devient fausse par cette opération. Dans ce papier, le concept de clause critique est étudié. On montre qu'il est la pierre angulaire de l'efficacité de notre approche, qui dépasse les techniques les plus efficaces d'extraction de MUS et d'ensembles de MUS, la plupart du temps.


ABSTRACT
SAT is probably one of the most-studied constraint satisfaction problems. In this paper, a new hybrid technique based on local search is introduced in order to approximate and extract minimally unsatisfiable subformulas (in short, MUSes) of unsatisfiable SAT instances. It is based on an original counting heuristic grafted to a local search algorithm, which explores the neighborhood of the current interpretation in an original manner, making use of a critical clause concept. Intuitively, a critical clause is a falsified clause that becomes true thanks to a local search flip only when some other clauses become false at the same time. In the paper, the critical clause concept is investigated. It is shown to be the cornerstone of the efficiency of our approach, which outperforms competing ones to compute MUSes, inconsistent covers and sets of MUSes, most of the time.


AUTEUR(S)
Éric GRÉGOIRE, Bertrand MAZURE, Cédric PIETTE

MOTS-CLÉS
SAT, recherche locale, MUS, ensemble minimalement incohérent, clause critique, couverture inconsistante.

KEYWORDS
SAT, local search, MUS, Minimally Unsatisfiable Subformula, critical clause, inconsistent cover.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (245 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier