Le SAT-solving est sans doute la technologie de base la plus importante pour la gestion des variantes, et pourtant presque personne ne la connaît. Dans les configurateurs de produits et les outils de gestion des variantes, ces algorithmes travaillent sous le capot — souvent sans que les utilisateurs se rendent compte de ce qui se passe réellement. C’est ce que je veux changer.
Que signifie « SAT » ?
SAT signifie Satisfiability — en français : satisfiabilité. Un problème SAT pose en substance la question suivante : existe-t-il une affectation de valeurs de vérité (vrai/faux) à un ensemble de variables qui satisfait une formule logique donnée ?
Cela paraît abstrait, mais c’est étonnamment utile. Car de nombreux problèmes de la vraie vie peuvent être traduits exactement sous cette forme — y compris la gestion des variantes.
La gestion des variantes a de nombreuses facettes
Je travaille beaucoup sur les produits riches en variantes. C’est un vaste domaine — de l’architecture produit aux règles de configuration, jusqu’aux outils qui gèrent tout cela. Et quand on regarde ces outils de plus près, on finit tôt ou tard par tomber sur le terme de SAT-solving.
Sans formation en informatique, c’est d’abord un mot étranger. Pourtant, c’est le fondement technique de nombreux configurateurs de produits et d’autres outils de gestion des variantes.
En simplifiant : on peut transmettre à un solveur SAT toutes les règles qui délimitent l’espace de variantes d’un produit. Par exemple, le fait qu’il n’existe des cabriolets que sans toit ouvrant — ou que la version sport d’une voiture nécessite un disque de frein plus grand. Le solveur peut alors vérifier si, avec toutes ces règles, il existe des variantes valides (donc « satisfiables ») — ou si les règles se contredisent à un point tel que rien ne serait plus constructible.
Comment pense le solveur SAT
Un solveur SAT reçoit une liste de contraintes — des expressions logiques — puis recherche une affectation qui les satisfait toutes simultanément. Dans la gestion des variantes, ces contraintes se présentent par exemple ainsi :
- « Si cabriolet, alors pas de toit ouvrant »
- « Si pack sport, alors disque de frein taille XL »
- « Sellerie cuir uniquement sur les versions 4 places »
Si je demande maintenant : « Existe-t-il des cabriolets avec sellerie cuir ? », le solveur doit vérifier s’il existe une variante qui satisfait simultanément « cabriolet » et « sellerie cuir ». Ce n’est pas trivial — car une telle règle directe n’existe peut-être pas du tout.
Mais elle pourrait exister indirectement : cuir uniquement sur les 4 places, cabriolet uniquement en 2 places — donc pas de cabriolet avec cuir. Le solveur SAT trouve cela même sans règle directe, car il a une vue d’ensemble sur tout le réseau de contraintes.
Dans ce cas, j’aurais bien envie d’avoir un petit mot avec le chef de produit responsable 😉 — mais le solveur a identifié de manière fiable une combinaison impossible.
Les solveurs SAT ouvrent de nombreux cas d’usage
Grâce à des requêtes formulées habilement, les solveurs SAT permettent de répondre à bien plus de questions que le simple « cette variante existe-t-elle ? » :
- Validation : l’ensemble de l’espace de variantes est-il sans contradiction ? Existe-t-il des variantes mortes, jamais constructibles à cause de règles qui se contredisent ?
- Guidage de configuration : lorsqu’un client a choisi « cabriolet », quelles options restent-elles sélectionnables, et lesquelles sont automatiquement exclues ?
- Analyse d’impact : lorsqu’une nouvelle règle est ajoutée — qu’est-ce qui change dans l’espace de variantes ?
- Analyse du portefeuille produits : combien de variantes valides existe-t-il au total ? Quelles combinaisons ne sont jamais attribuées ?
Pour des produits complexes comportant des dizaines ou des centaines de points de variation, ces analyses sont tout simplement impossibles à réaliser à la main. Un solveur SAT les effectue en quelques millisecondes.
Où les solveurs SAT sont utilisés
De nombreux outils commerciaux de gestion des variantes et de configuration de produits s’appuient sur le SAT-solving : ConfigIt, la configuration des variantes SAP, pure::variants — et cette technologie est également répandue dans des outils spécialisés pour l’automobile. La plupart des utilisateurs n’en perçoivent rien, car le solveur travaille en profondeur dans le système.
Celles et ceux qui souhaitent expérimenter eux-mêmes avec un solveur SAT n’ont pas besoin de monter tout un projet logiciel. MiniZinc est un outil libre qui intègre des solveurs SAT dans son propre langage de modélisation — et qui fonctionne même dans le navigateur. Je montre comment cela fonctionne précisément dans l’article suivant sur MiniZinc et les premiers pas avec les solveurs SAT.
Les solveurs SAT ne sont pas un simple jeu académique — ils constituent le fondement technique des configurateurs de produits modernes. Comprendre leur fonctionnement permet de mieux saisir pourquoi les règles de configuration doivent être formulées comme elles le sont, et pourquoi certaines questions sur l’espace de variantes peuvent recevoir une réponse étonnamment rapide.
