# Complexity assessments for decidable fragments of Set Theory. IV: A quadratic reduction of constraints over nested sets to Boolean formulae

arXiv: https://arxiv.org/abs/2112.04797 · HTML: https://mlsanity.com/paper/2112.04797/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 1 of its 27 references that are in the map.
- First posted on arXiv 9 Dec 2021.

## Builds on (most cited first, 1 of 1)

- [Integrating Cardinality Constraints into Constraint Logic Programming with Sets](https://mlsanity.com/paper/2102.05422/) (2021)

## Abstract (arXiv)

As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms x=ysetminus z, x neq ysetminus z, and z =x, 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 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=ysetminus z, xneq ysetminus 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.