A quadratic reduction of constraints over nested sets to purely boolean formulae in CNF

A translation is proposed of conjunctions of literals of the forms x = y n z, x ≠ y n z, and x 2 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, nondisjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms x = y nz, x ≠ y nz 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 reecting a simple and natural semantics, which ensures satisfi- ability-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.