
Le raisonnement est une composante fondamentale de l'IA depuis ses débuts. Cependant, même des mécanismes très simples, basés sur une logique presque triviale, sont rapidement intraitables en pratique, en raison d'une explosion combinatoire inhérente. Malgré ces fortes limitations théoriques, les solveurs SAT ont montré des progrès impressionnants au cours des 20 dernières années, leur permettant de résoudre couramment des problèmes industriels avec des millions de variables. Dans cet exposé, nous passerons en revue l'histoire des solveurs SAT et présenterons comment des codages astucieux des problèmes, avec des structures de données et des algorithmes serrés, ont permis à ces solveurs de défier les limites théoriques des problèmes qu'ils traitent.