UNE PROCÉDURE DE DÉCISION POUR UN PROBLÈME DE SATISFIABILITE DANS UN UNIVERS ENSEMBLISTE HÉRÉDITAIREMENT FINI

摘要

Nous traitons, dans cet article, du problème de satisfiabilité d'un système de contraintes ensemblistes, dans un univers d'ensembles héréditairement finis. Ce problème est central dans l'intégration des ensembles dans les langages de programmation, en particulier, en programmation en logique avec contraintes. Nous proposons une approche fondée sur la réduction des systèmes de contraintes ensemblistes en un système équisatisfiable d'équations et d'inéquations linéaires en entiers. La complexité de cette réduction est en O (n~3).%In this paper, we deal with the satisfiability problem for systems of constraints over hereditarily finite sets. This problem is central for integrating sets in programming languages, and particularly for constraint logic programming languages. The approach we propose here is based on reducing systems of set constraints into systems of linear integer equalities and inequalities (with bounded domain). The complexity of the reduction is on O (n~3 ).