É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)(2^0:2325n) ((O)(2^0: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.