Résolution du problème des Reines LinkedIn avec SMT : Plus facile qu'avec SAT !
Cet article détaille la résolution du casse-tête des « Reines LinkedIn », une variante du problème classique des N-Reines avec des contraintes régionales supplémentaires, à l'aide du solveur SMT Z3. L'auteur montre que l'expression du problème en SMT, en utilisant des variables entières et des contraintes, est considérablement plus simple que la formulation SAT équivalente, qui nécessite de nombreuses clauses booléennes. Bien que les solveurs SMT puissent être plus lents que les solveurs SAT hautement optimisés comme Glucose, la facilité d'encodage rend le SMT préférable pour beaucoup. L'article inclut le code complet et des vérifications de bon fonctionnement utiles pour vérifier l'exactitude du modèle. Cela fournit une explication convaincante de la préférence de l'industrie pour les outils qui compilent en SAT plutôt que d'utiliser directement SAT.