Convex and Reverse Convex Prequadratics Constraints for Decidable Logics of Relations with Cardinalities

We investigate decision procedures for quantifier-free fragments of set theory extended with relational and cardinality constraints. While the satisfiability problem for the general fragment is undecidable due to the existence of reductions from Hilbert's 10th problem, in this paper we show that extensions of existential Presburger arithmetic with atoms of the form \(x≤ yᵈ\) or of the form \(yᵈ≤ x\) , where \(d\) , are decidable in non-deterministic polynomial time. We apply these results to fragments of quantifier-free relational logic. Our methods rely on a normal form for linear constraints, which may be of independent interest.