Abstract FR:

Les interpreteurs de programmes logiques avec contraintes, sur lesquels reposent l'efficacite de ce type de langages, doivent faire face a des objectifs parfois contradictoires. A la fois explorateurs d'espace de recherche et presentateurs de resultats, une de leur tache essentielle reste la resolution de contraintes. Dans cette these nous nous interessons aux interpreteurs specialises dans le traitement de contraintes lineaires sur les nombres rationnels. Dans un premier temps nous comparons et optimisons differentes methodes de resolution, dans un deuxieme nous donnons une methode pour desengorger les systemes de contraintes en eliminant dynamiquement une majorite de leurs variables. Les algorithmes decrits ont ete implementes et rendus publics par l'intermediaire de multisolver(q), un interpreteur plc, et de solver(q), une bibliotheque de fonctions c.