A translation is proposed of conjunctions of literals of the
forms x = y z, x /= y z, and x ∈ y, where x, y, z stand for variables
ranging over the von Neumann universe of sets, into unquantified Boolean
formulae of a rather simple conjunctive normal form. The formulae in
the target language involve variables ranging over a Boolean field 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, 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.
