NP Satisfiability for Arrays as Powers

Rodrigo Raya, Viktor Kunčak

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinator…