Des chaînes d'équivalences dans un codage CNF du problème XSAT

Résumé : Étant donné une formule booléenne mise sous forme normale conjonctive (CNF), le problème de satisfiabilité XSAT, une variante du problème de satisfiabilité (SAT), consiste à trouver une interprétation des variables pour laquelle chaque clause est satisfaite par exactement un littéral. Le meilleur algorithme pour résoudre ce problème possède une complexité en temps en (O)(20:2325n) ((O)(20:1379n) pour X3SAT) [12]. Une autre possibilité pour résoudre ce problème consiste à transformer chaque clause dans un ensemble de clauses équivalentes pour le problème de satisfiabilité et d'utiliser des solveurs SAT modernes et puissants (zChaff [14], Berkmin [6], MiniSat [5], etc) pour trouver une telle interprétation. Dans ce papier, nous introduisons un nouveau codage du problème XSAT dans SAT qui contient beaucoup d'informations structurelles (en particulier les chaînes d'équivalences), qui sont cachées dans la transformation habituelle. Certains solveurs (LSAT [15], march_dl [7]) prennent en compte ce type d'informations structurelles pour faire des simplifications en prétraitement et accélérer la résolution. Puis, nous montrons l'intérêt de traiter le problème XSAT en introduisant un codage des CSP binaires et du problème de coloration de graphes sous forme de problèmes XSAT. Les résultats préliminaires sur le problème de coloration de graphes montrent l'importance du raisonnement sur les équivalences pour le problème XSAT.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.297-306, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00292677
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : mercredi 2 juillet 2008 - 13:41:31
Dernière modification le : jeudi 18 janvier 2018 - 02:20:49
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:05:02

Fichier

pages-297-306-article9.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00292677, version 1

Collections

Citation

Richard Ostrowski, Lionel Paris. Des chaînes d'équivalences dans un codage CNF du problème XSAT. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.297-306, 2008. 〈inria-00292677〉

Partager

Métriques

Consultations de la notice

87

Téléchargements de fichiers

116