Approximation d'ensembles horn strong backdoor par recherche locale

Résumé : Dans ce papier, nous proposons une nouvelle approche pour calculer un strong backdoor pour des formules mises sous forme normale conjonctive (CNF). Elle est basée sur une utilisation originale d'une méthode de recherche locale qui fournit un renommage maximisant la sous-formule horn-renommable d'une CNF donnée. Plus précisément, à chaque étape, on choisit de renommer la variable qui fait le plus diminuer le nombre de clauses non-horn. S'il ne reste plus de clauses strictement positives (ou strictement négatives) ou de clauses non-horn dans la formule, notre méthode répond au problème de satisfaisabilité de la formule originale; sinon, on utilise la plus petite sous-formule qui ne soit pas de horn pour en extraire un ensemble de variables (strong backdoor) tel qu'une fois ces variables instanciées, le reste du problème appartient à une classe polynômiale. Les premiers résultats expérimentaux montrent que notre approche est prometteuse sur un grand nombre d'instances SAT.
Type de document :
Communication dans un congrès
Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00085807
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 15:17:42
Dernière modification le : jeudi 15 mars 2018 - 16:56:06
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:09:44

Fichier

Identifiants

  • HAL Id : inria-00085807, version 1

Collections

Citation

Lionel Paris, Richard Ostrowski, Lakhdar Saïs, Pierre Siegel. Approximation d'ensembles horn strong backdoor par recherche locale. Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006. 〈inria-00085807〉

Partager

Métriques

Consultations de la notice

172

Téléchargements de fichiers

337