A decision process for the satisfiability problem in a universe of hereditarily finite sets

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)).