Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292677
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Wednesday, July 2, 2008 - 1:41:31 PM
Last modification on : Monday, March 30, 2020 - 8:48:21 AM
Long-term archiving on: : Friday, May 28, 2010 - 11:05:02 PM

File

pages-297-306-article9.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00292677, version 1

Citation

Richard Ostrowski, Lionel Paris. Des chaînes d'équivalences dans un codage CNF du problème XSAT. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.297-306. ⟨inria-00292677⟩

Share

Metrics

Record views

136

Files downloads

249