Diagnostiquer un système consiste à déterminer si le fonctionnement du système est normal ou défectueux grâce à des observations sur ce fonctionnement. Dans le cadre des systèmes à événements discrets (SED), lorsqu'un modèle complet est fourni, cela revient à calculer sur le modèle les comportements compatibles avec les observations et tester la normalité de ces comportements. Nous montrons que les problèmes de diagnostic de SED peuvent être traduits en problèmes de satisfiabilité propositionnelle (SAT) de formules booléennes sous forme normale conjonctive CNF). Nous résolvons ensuite le problème SAT à l'aide des meilleurs solveurs actuels. Les résultats montrent que les algorithmes SAT permettent de résoudre des problèmes que les algorithmes traditionnels de diagnostic ne peuvent traiter.