Complexity Results for Some Fragments of Set Theory Involving the Unordered Cartesian Product Operator

In the context of Computable Set Theory, we consider the satisfiability problem for various subcases of the fragment BST⊗ (Boolean Set Theory with the unordered Cartesian product ⊗), whose long-standing decision problem has received very recently a positive solution in the NEXPTIME complexity class. BST⊗ is the quantifier-free set theory involving the Boolean set operators of union (∪), intersection (∩), and set difference (∖), as well as the unordered Cartesian product operator (⊗), and the set equality (=) and inclusion (⊆) predicates, where the unordered Cartesian product 𝑠 ⊗ 𝑡 of two sets 𝑠 and 𝑡 is defined as the collection of all possible unordered pairs formed by selecting one element from 𝑠 and one element from 𝑡. It is an open problem whether the satisfiability problem for BST⊗ is NP-complete. Here, we delve into the specific case in which the number of distinct leading variables in literals of the form 𝑥 = 𝑦 ⊗ 𝑧 is O(log 𝑛), where 𝑛 represents the size of the BST⊗ formula that one wants to test for satisfiability, and prove its NP-completeness. We will also mention various additional NP-completeness and polynomial results concerning the decision problem for other subtheories of BST⊗.