Complexity Assessments for Decidable Fragments of Set Theory. IV: A Quadratic Reduction from Constraints over Nested Sets to Boolean Formulae

As a contribution to automated set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms x = y \z, x ̸= y \z, and z = {x}, where x, y, z stand for variables ranging over the von Neumann universe of sets, into quantifier-free Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean ring of sets, along with a difference operator and relators designating equality, non-disjointness, and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms x = y \z and x ̸= y \z and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides reflecting a simple and natural semantics, which ensures satisfiability preservation, the proposed translation has quadratic algorithmic time complexity and bridges two languages, both of which are known to have an NP-complete satisfiability problem.