Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator

We give a positive solution to the decidability problem for the fragment of set theory, dubbed BST⊗, consisting of quantifier-free formulae involving the Boolean set operators of union, intersection, and set difference, along with the unordered Cartesian product operator ⊗, and the equality predicate, but no membership. Specifically, we provide nondeterministic exponential decision procedures for both the ordinary and the finite satisfiability problems for BST⊗. We expect that these decision procedures can be adapted for the standard Cartesian product and, with added technicalities, to the cases involving membership, providing a solution to a longstanding problem in computable set theory.