Modèles d'optimisation pour la couverture de sous-ensembles

Dans un article de newsletter récent, je me plaignais de la façon dont les chercheurs trompent sur l'applicabilité de leurs travaux. J'ai donné les solveurs SAT comme exemple. Les gens ont fourni des exemples intéressants en réponse, mais ce qui était nouveau pour moi était le concept de SMT (Satisfiability Modulo Theories), une extension de SAT. Le SMT semble avoir plus d'utilisations pratiques que le SAT classique (voir la newsletter pour plus de détails). Je voulais prendre un peu de temps pour explorer les solveurs SMT, et je suis tombé sur Z3, un solveur SMT open-source de Microsoft.