Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combinatory Array Logic with Sums

Rodrigo Raya

TL;DR

The paper addresses the satisfiability problem for a theory of integer-indexed arrays augmented with index-ordering and summation constraints, proving an NP upper bound for the existential fragment of the generalized power structure $Th_{\exists^*}(\mathcal{P}(\mathcal{A},I))$ and extending combinatory array logic with sums. It achieves this via a semantic reduction to generalized power structures, encoding array operations and sums, and reducing satisfiability to a chain of eliminations that culminate in $LIA^{card}$, an NP problem. A key insight is that allowing element-constants undermines decidability, while restricting the element theory enables a polynomially bounded, certificate-based NP procedure. The work advances SMT theories of arrays by linking combinatory array logic with summation constraints to powerful model-theoretic constructions, offering a practical complexity result and guiding future extensions to richer element sorts.

Abstract

We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combinatory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.

Combinatory Array Logic with Sums

TL;DR

The paper addresses the satisfiability problem for a theory of integer-indexed arrays augmented with index-ordering and summation constraints, proving an NP upper bound for the existential fragment of the generalized power structure and extending combinatory array logic with sums. It achieves this via a semantic reduction to generalized power structures, encoding array operations and sums, and reducing satisfiability to a chain of eliminations that culminate in , an NP problem. A key insight is that allowing element-constants undermines decidability, while restricting the element theory enables a polynomially bounded, certificate-based NP procedure. The work advances SMT theories of arrays by linking combinatory array logic with summation constraints to powerful model-theoretic constructions, offering a practical complexity result and guiding future extensions to richer element sorts.

Abstract

We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combinatory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.
Paper Structure (8 sections, 10 theorems, 16 equations, 1 figure)

This paper contains 8 sections, 10 theorems, 16 equations, 1 figure.

Table of Contents

  1. Introduction
  2. First-order model theory
  3. Array theories
  4. Decision Procedure
  5. Conclusion
  6. Elimination of Boolean algebra with Cardinalities terms
  7. Elimination of the multiset comprehension
  8. $\NP$ membership of $\textsf{LIA}^{card}$

Key Result

Proposition 1

The existential closure of the satisfiable formulas in the quantifier-free fragment of $T_A$ is the set $Th_{\exists^*}(Ax)$. Conversely, if we drop the existential prefixes in $Th_{\exists^*}(Ax)$, we obtain the satisfiable formulas of the quantifier-free fragment of $T_A$.

Figures (1)

  • Figure 1: Verifier for $LIA^{card}$.

Theorems & Definitions (17)

  • Proposition 1
  • proof
  • Definition 2
  • Theorem 3
  • Theorem 4
  • Definition 5
  • Corollary 6
  • proof
  • Proposition 7: Multiset elimination
  • Definition 8
  • ...and 7 more