NP Satisfiability for Arrays as Powers

TL;DR

This paper proves that the satisfiability problem for arrays with cardinality constraints is in NP and extends array logic to include these constraints, independent of underlying theories.

Contribution

It introduces a new NP decision procedure for array satisfiability with cardinality and extends array logic to handle these constraints independently.

Findings

Satisfiability for arrays with cardinality constraints is in NP.

Extended array logic fragment handles cardinality constraints.

Framework is independent of base element and index set theories.

Abstract

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 combinatory array logic fragment to handle cardinality constraints. The resulting fragment is independent of the base element and index set theories.