Sentient : Lutter contre l'infini dans les solveurs de contraintes

Cet article explore les défis liés à la gestion de l'infini dans le solveur de contraintes Sentient. Sentient, un langage de programmation, traite les problèmes de satisfaction de contraintes en les traduisant en équations booléennes. Comme les entiers dans les ordinateurs sont représentés avec un nombre fini de bits, Sentient ne peut pas gérer directement les entiers infinis mathématiquement. L'auteur propose une solution basée sur l'approximation, en augmentant progressivement la taille en bits des entiers pour approcher l'espace infini. L'article discute de l'utilisation du solveur SAT incrémental IPASIR pour une meilleure efficacité, en évitant les recherches redondantes. Il explore également l'extension de cette approche à des scénarios plus complexes, tels que la gestion des tableaux et des problèmes d'optimisation, et aborde finalement la possibilité que Sentient atteigne la complétude de Turing à l'avenir.