Une des méthodes priviligiée pour la résolution de problèmes en raisonnement qualitatif est la traduction en SAT pour déléguer la résolution à un solveur. Je présenterais un panel des encodages populaires pour les calculi RCC8 et Algèbre des Intervalles de Allen. Je pointerai notamment les différences en terme de pouvoir de propagation de ces différents encodages. Je terminerai par un encodage inédit pour RCC8 qui présente de meilleures propriétés de propagation que les encodages de l'état de l'art.