Analysis of Logics with Arithmetic

Benedikt, Michael; Lu, Chia-Hsuan; Tan, Tony

doi:10.4230/LIPIcs.CSL.2026.27

Analysis of Logics with Arithmetic

Michael Benedikt

University of Oxford, UK Chia-Hsuan Lu

University of Oxford, UK Tony Tan

University of Liverpool, UK

Abstract

We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional “global cardinality constraints”: restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

Keywords and phrases:

Presburger quantifiers, Spectrum, Guarded logics

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

This paper concerns the problem of determining whether a formula in some logic $\mathcal{L}$ is satisfied in some finite structure: the finite satisfiability problem for $\mathcal{L}$ . For the fragments of interest to us, the decidability of this problem will imply decidability of many other static analysis problems for the logic, such as validity of a sentence over finite structures and equivalence of two sentences over finite structures. The problem is known to be undecidable for first order logic [20]. In the last decades two paradigms for decidability emerged, one based on restricting to guarded quantification, and another restricting to two variable fragments. The two variable fragment of first order logic was shown to have decidable finite satisfiability problem and this was extended to allow “counting quantifiers”, of the form $\exists^{\geq k}y\nobreak\ \phi(x,y)$ , where $k$ is fixed. The complexity of the satisfiability problem for this logic, normally denoted $\mathsf{C^{2}}$ , over finite structures, as well as the complexity of satisfiability when considering arbitrary structures, was isolated in [15]. The same problem for the sublogic where quantification is guarded was shown to have slightly lower complexity [16].

In recent years there has been interest in adding more powerful arithmetic capabilities to these decidable logics. Instead of just asking whether the number of elements satisfying a property is above or below a constant, we can ask whether the cardinality is even, or whether the cardinality of several properties satisfies a linear inequality. Presburger logic focuses on linear inequalities between properties [2, 4, 3, 12], and local Presburger logic, $\mathsf{GP^{2}}$ , restricts to properties that involve neighbors of a given element. These logics are most naturally applied to finite models, to avoid dealing with addition or parity of infinity: thus in this work, finite satisfiability will always be our default, and we just refer to “satisfiability” henceforward. In [6] it was shown that local Presburger logics are in some sense equally expressive as certain variations of Graph Neural Networks (GNNs), and GNN verification problems can be reduced to satisfiability problems for these logics. It has been shown that satisfiability of Presburger logic is undecidable, while satisfiability of local Presburger logic is decidable [4]: the complexity of local Presburger logic is $\mathsf{NEXP}$ complete [3, 12], but the exact complexity of finite satisfiability had not been determined. Another way of enhancing logic with arithmetic involves global cardinality constraints. In such an enhancement, we can write a constraint that defines a constraint (e.g., a linear inequality) between one variable formulas. But we cannot have such a constraint parameterized by a second free variable. For example, we can write that unary predicate $U$ has cardinality below unary predicate $V$ . But if $E$ and $F$ are two binary predicates, we cannot express that the elements that are not $E$ adjacent to $x$ have greater cardinality than the elements that are not $F$ adjacent to $x$ .

As with local Presburger logic, it follows from prior results that $\mathsf{C^{2}}$ enhanced with global cardinality constraints has decidable (finite) satisfiability problem. The exact complexity is not explicitly studied in the literature, although in the case of global cardinality constraints consisting of linear inequalities, tight bounds follow from results of Rudolph in [18]. A natural approach to proving decidability for logics enhanced with global constraints follows is to show that the the spectrum of each tuple of unary formulas of the logic is effectively semilinear. The spectrum of a tuple of unary formulas $\phi_{1}(x)\ldots\phi_{k}(x)$ is the set of possible values that the tuple of cardinalities of the satisfiers of the formula can have within a finite model. For example, for the pair of formulas $\phi_{1}(x)=U(x),\phi_{2}(x)=U(x)\wedge V(x)$ the spectrum consists of all pairs $(m,n)$ with $n\leq m$ . The spectrum being effectively semilinear means that we can find a quantifier-free formula of arithmetic that defines it. From effective semilinearity of the spectrum, we easily obtain decidability with additional global constraints. Here we provide complexity bounds for several of these problems, one featuring arithmetic over counts of neighbors, another concerning computing the spectrum of formulas. See Table 1 for the summary of our new upper bounds. At the same time, we provide simpler proofs of two fundamental results in the area: decidability of (finite) satisfiability for $\mathsf{GP^{2}}$ (see Section 4), and effective semi-linearity of the spectrum for $\mathsf{C^{2}}$ (Section 5). We complement these positive results with a counterexample to semilinearity of spectra for $\mathsf{GP^{2}}$ unary formulas (Section 6).

2 Preliminaries

Basic notions.

A graph will always mean a finite directed graph without self-loops. A colored graph is a graph where nodes have a unique node label, and every pair of distinct nodes is connected by a unique edge (in one direction or the other), with node and edge vocabularies distinct. A multigraph is a finite directed graph without self-loops that allows a finite number of parallel edges (including no edge) between a pair of distinct nodes. A colored multigraph is defined similarly, but requiring each node to have a unique label. The multiplicity of a multigraph is defined as the maximum edge multiplicity within it.

The $i^{th}$ unit vector, denoted by $\mathbf{e}_{i}$ , has $i^{th}$ entry $1$ , and other entries are $0$ . We define $\mathbf{0}$ as the vector where all entries are $0$ , and $\mathbf{1}$ as the vector that all entries are $1$ . For $\mathbf{v},\mathbf{u}\in\mathbb{N}^{n}$ , $\mathbf{v}\preccurlyeq\mathbf{u}$ if, for $1\leq i\leq n$ , $\mathbf{v}_{i}\leq\mathbf{u}_{i}$ Let $\mathsf{proj}_{n}\left(\mathbf{v}\right)$ denote the projection operator that maps $\mathbf{v}$ to its first $n$ entries. Let $\left\|\mathbf{A}\right\|$ and $\left\|\mathbf{v}\right\|$ denote the maximal absolute values of the entries in $\mathbf{A}$ and $\mathbf{v}$ , respectively.

Linear algebra and Kleene star.

An integer linear constraint is an inequality $\sum_{i}a_{i}\cdot x_{i}\leq c$ involving integer coefficients $a_{i}$ , non-negative integer variables $x_{i}$ , and an integer constant $c$ . The set of solutions of such a constraint is called a modulus-free semilinear set, while if we include equations $x=c\mod p$ for integers $c,p>0$ it is a semilinear set. A constraint is homogeneous if $c=0$ .

For an integer linear system $\mathcal{Q}(\mathbf{x}):\mathbf{A}\mathbf{x}=\mathbf{c}$ , we denote by $\left\llbracket\mathcal{Q}(\mathbf{x})\right\rrbracket$ the set of solutions in $\mathbb{N}$ , i.e., $\left\llbracket\mathcal{Q}(\mathbf{x})\right\rrbracket:=\left\{\mathbf{v}\in% \mathbb{N}^{n}\middle|\ \mathbf{A}\mathbf{v}=\mathbf{c}\right\}$ , and similarly for a Boolean combination of linear systems. Note that if $\mathcal{Q}(\mathbf{x})$ is feasible, then it has a solution in which the number of non-zero assignments is bounded, and the values of the assignments are also bounded.

Lemma 1 ([13], [7], also see Corollary 2.2 in [12]).

There are constants $c_{1},c_{2}\in\mathbb{N}$ such that for every integer linear system $\mathcal{Q}(\mathbf{x})$ , if $\mathcal{Q}(\mathbf{x})$ admits a solution in $\mathbb{N}$ , then it admits a solution in $\mathbb{N}$ in which the number of variables assigned non-zero values is at most $c_{1}t\log\left(c_{2}tM\right)$ and every variable is assigned a value bounded by $c_{1}t(tM)^{c_{2}t}$ , where $t$ is the number of constraints in $\mathcal{Q}(\mathbf{x})$ and $M$ is the maximal absolute value of the coefficients in $\mathcal{Q}(\mathbf{x})$ .

Definition 2 (Kleene star).

For a set $\mathcal{S}\subseteq\mathbb{N}^{n}$ , the Kleene star of $\mathcal{S}$ is defined as

\mathsf{KleeneStar}\left(\mathcal{S}\right)\ :=\ \left\{\sum_{s\in\mathcal{S}^% {\prime}}s\middle|\ \text{$\mathcal{S}^{\prime}$ is a finite multisubset of $% \mathcal{S}$}\right\}.

Note that $\mathbf{0}\in\mathsf{KleeneStar}\left(\mathcal{S}\right)$ for any $\mathcal{S}$ .

If $\mathcal{S}$ is semilinear then its Kleene star is semilinear: this is closely-related to Parikh’s theorem which gives a correspondence between semi-linear sets and regular languages: see [14, 8]. We will be interested in bounding the complexity of the Kleene star of a semilinear set using numerical data associated to the set. Note that for an integer linear system $\mathcal{Q}(\mathbf{x}):\mathbf{A}\mathbf{x}=\mathbf{c}$ , if $\mathbf{c}=\mathbf{0}$ , then $\mathsf{KleeneStar}\left(\left\llbracket\mathcal{Q}(\mathbf{x})\right% \rrbracket\right)=\left\llbracket\mathcal{Q}(\mathbf{x})\right\rrbracket$ . The following result gives a bound when $\mathbf{c}\neq\mathbf{0}$ .

Lemma 3.

For every integer linear system $\mathcal{Q}(\mathbf{x}):\mathbf{A}\mathbf{x}=\mathbf{c}$ with $\mathbf{c}\neq\mathbf{0}$ , where $\mathbf{A}\in\mathbb{Z}^{m\times n}$ and $\mathbf{c}\in\mathbb{Z}^{m}$ , there exists $\tilde{\mathbf{A}}\in\mathbb{Z}^{(n+t)\times(n+k)}$ with $\left\|\tilde{\mathbf{A}}\right\|=1$ such that $\mathsf{KleeneStar}\left(\left\llbracket\mathcal{Q}(\mathbf{x})\right% \rrbracket\right)=\left\llbracket\tilde{\mathcal{Q}}(\mathbf{x})\right\rrbracket$ , where $\tilde{\mathcal{Q}}(\mathbf{x})$ is the Boolean combination of integer linear systems

\exists\mathbf{y}_{1},\mathbf{y}_{2}\ (\mathbf{x}\ =\ \mathsf{proj}_{n}\left(% \mathbf{y}_{1}\right)+\mathbf{y}_{2})\ \land\ (\tilde{\mathbf{A}}\mathbf{y}_{1% }\ =\ \mathbf{0})\ \land\ (\mathbf{A}\mathbf{y}_{2}\ =\ \mathbf{0})\ \land\ ((% \mathbf{y}_{1}=\mathbf{0})\to(\mathbf{y}_{2}=\mathbf{0})),

$k=n\cdot(2D+1)^{m}+1$ , $t\leq 2nk$ , and $D=n\cdot\left\|\mathbf{A}\right\|\cdot\left((n+1)\cdot\left\|\mathbf{A}\right% \|+\left\|\mathbf{c}\right\|+1\right)^{m}$ . Moreover, $\tilde{\mathbf{A}}$ can be computed in time $2^{\mathcal{O}\left(\log n+\log K+m^{2}\right)}$ , where $K:=\max\left(\left\|\mathbf{A}\right\|,\left\|\mathbf{c}\right\|\right)$ .

We defer the proof of this to the appendix.

Types.

Let $\sigma$ be a vocabulary with unary $U_{1},\ldots,U_{n}$ and binary $R_{1},\ldots,R_{m}$ .

Definition 4 (1- and 2-type).

A 1-type (w.r.t. $\sigma$ ) is a maximal consistent subset of

\bigcup_{i\in{\left[n\right]}}\left\{U_{i}(x),\neg U_{i}(x)\right\}\ \cup\ % \bigcup_{i\in{\left[m\right]}}\left\{R_{i}(x,x),\neg R_{i}(x,x)\right\}.

A 2-type (w.r.t. $\sigma$ ) is a maximal consistent subset of

\bigcup_{i\in{\left[m\right]}}\left\{R_{i}(x,y),\neg R_{i}(x,y),R_{i}(y,x),% \neg R_{i}(y,x)\right\}.

We denote the set of $1$ -types by $\mathsf{OneTps}$ and the set of $2$ -types $\mathsf{TwoTps}$ .

Given an element $v$ in a $\sigma$ -structure $\mathcal{G}$ , we let $\mathsf{OneTp}(v)$ denote its one-type in $\mathcal{G}$ and similarly for a pair of elements $v, u$ in $\mathcal{G}$ we let $\mathsf{TwoTp}(v,u)$ denote its two-type in $\mathcal{G}$ ; in both cases we omit the dependence on $\mathcal{G}$ for brevity.

The following definitions are variations of notions in Pratt-Hartmann’s [15, 16, 17].

Definition 5 (Silent 2-type).

The silent type, denoted by $\eta_{0}$ , is the unique 2-type that consists of only negated terms. If a type is not silent we say it is audible.

Definition 6 (Dual of 2-type).

For a 2-type $\eta$ , the dual of $\eta$ , denoted by $\widetilde{\eta}$ , it the unique 2-type that swaps $x$ and $y$ in $\eta$ .

We denote the set of all 2-types except $\eta_{0}$ by $\mathsf{TwoTps}^{+}$ , and the set of all 2-types that contain $R_{t}(x,y)$ by $\mathsf{TwoTps}_{t}$ for $1\leq t\leq m$ .

Note that ${\left|\mathsf{OneTps}\right|}=2^{n+m}$ , ${\left|\mathsf{TwoTps}\right|}=2^{2m}$ , ${\left|\mathsf{TwoTps}^{+}\right|}=2^{2m}-1$ , and ${\left|\mathsf{TwoTps}_{t}\right|}=2^{2m-1}$ .

We can abstract a model based on types:

Definition 7 (Type graph).

We associate to a $\sigma$ -structure in a binary vocabulary a colored graph with the same set of vertices in an exponentially larger vocabulary: each vertex is colored with a 1-type, and each edge is colored with a 2-type. This is the type graph of the $\sigma$ -structure.

Losing information, we can abstract a finite model based on cardinalities of $1$ -types. The notion will be crucial in Section 5:

Definition 8 ( $1$ -type cardinality vector of a $\sigma$ -structure).

Let $\mathcal{G}$ be a $\sigma$ -structure. The $1$ -type cardinality vector of $\mathcal{G}$ is a ${\left|\mathsf{OneTps}\right|}$ -dimensional vector where the $i^{th}$ component is the number of elements in $\mathcal{G}$ with 1-type $\pi_{i}$ .

3 Logics and prior complexity bounds concerning them

We fix a vocabulary $\sigma$ which consists of $n$ unary predicates $U_{1},\ldots,U_{n}$ and $m$ binary predicates $R_{1},\ldots,R_{m}$ . All of our logics will consist of formulas with at most two variables, $x$ and $y$ . We start by reviewing two variable logic with counting ( $\mathsf{C^{2}}$ ), built up from atomic formulas $U_{i}(x)$ , $U_{i}(y)$ , $R_{i}(x,y)$ , and $R_{i}(y,x)$ via the Boolean operators and the quantifier constructs $\rho(x):=\exists^{\geq k}y\ \phi(x,y)$ , where $\phi$ is a $\mathsf{C^{2}}$ formula and $k$ is a natural number, and similarly with the role of $x$ and $y$ swapped.

Our semantics will always be over finite structures interpreting the vocabulary $\sigma$ . The formula $\rho(y)$ above holds in a model $M$ at an element $u$ for $x$ when there are least $k$ elements $v$ such that $M\models\phi(u,v)$ . The case $k=1$ represents standard existential quantification.

Guarded two variable logic with counting ( $\mathsf{GC^{2}}$ ), restricts $\mathsf{C^{2}}$ by requiring quantification to be guarded by an atom. The quantifier rule now includes the forms:

\exists^{\geq k}y\ R_{i}(x,y)\land\phi(x,y),\quad\exists^{\geq k}y\ R_{i}(y,x)% \land\phi(x,y),\quad\text{or}\quad\exists^{\geq k}x\ \nobreak\ U_{i}(x)\land% \phi(x).

The logic $\mathsf{P^{2}}$ replaces $\mathsf{C^{2}}$ ’s counting quantifier with a Presburger quantifier:

\rho(x)\ :=\ \left(\sum_{t\in{\left[m\right]}}\kappa_{t}\cdot{\#_{y}\left[\phi% _{t}(x,y)\right]}\right)\ \circledast\ \delta,

where $\kappa_{t}$ are integers, $\circledast$ is an inequality or equality, and $\delta$ is an integer. In $\mathsf{P^{2}}$ we will also allow unguarded quantification over unary formulas: if $\phi(x)$ is a formula, so is $\exists x\ \phi(x)$ . For example, $\exists x\left({\#_{y}\left[R(x,y)\right]}-3\cdot{\#_{y}\left[R(y,x)\right]}=0\right)$ is a sentence of $\mathsf{P^{2}}$ that holds in a directed graph when there is an element that has 3 times as many outgoing edges as incoming edges.

The logic $\mathsf{GP^{2}}$ (guarded two variable logic with Presburger quantifiers) restricts $\mathsf{P^{2}}$ by requiring each $\phi_{i}$ in a Presburger quantifier to be guarded, although still allowing unguarded unary quantification. Note that global cardinality constraints can be expressed in $\mathsf{P^{2}}$ , but not in $\mathsf{GP^{2}}$ . Following prior papers [12], we do not allow a quantifier that tests the modulus of a linear combination of cardinalities of one dimensional sets, and thus our quantifiers are in a sense weaker than Presburger arithmetic. A Presburger modulus constraint is as above, but allowing $\circledast\ \delta$ to be replaced by $(=m\mod n)$ , for natural numbers $m, n$ with $m<n$ . Likewise, $\mathsf{C^{2}}^{+g}$ can be extended to allow modulus constraints. In the appendix we show that all of of our results on $\mathsf{GP^{2}}$ and $\mathsf{C^{2}}^{+g}$ also hold for the extension with modulus constraints; in the body of the paper we focus on plain $\mathsf{GP^{2}}$ and $\mathsf{C^{2}}^{+g}$ in the statements.

Given a unary formula $\phi(x)$ in some logic, and a finite model $M$ , we let $|\phi|_{M}$ be the cardinality of $\phi$ in $M$ ; we extend this notation to a tuple $\langle\phi_{1}(x)\ldots\phi_{k}(x)\rangle$ . Given such a tuple, its spectrum is the set of vectors of numbers of the form $|\phi_{1}(x)\ldots\phi_{k}(x)|_{M}$ . We say that such a spectrum is semi-linear if it can be represented as a set of linear inequalities. When we talk about computing the spectrum for a formula, we mean computing a semi-linear representation. If we have such a representation, we can clearly check whether an individual $\phi_{i}(x)$ is satisfiable, simply by seeing if the corresponding set of constraints is feasible. Thus, in cases, where the spectrum is known always to have such a representation, computing the spectrum can be seen as a generalization of the satisfiability pboelm.

The positive results in this paper, as well as the prior bounds, are summarized in Table 1. In the table, Sat Logic refers to the satisfiability problem for formulas of the logic over finite structures, while Spectrum refers to a bound on the size of a representation of the spectrum, again over finite structure. An entry of the form $X$ -c indicates that the problem is complete for complexity class $X$ .

Table 1: Complexity results, with those new to this work in bold.

	Sat Logic	Spectrum Size Bound
$\mathsf{GC^{2}}$	$\mathsf{EXP}$ -c [16]	$\mathsf{EXP}$ (formerly $\mathsf{2EXP}$ )
$\mathsf{C^{2}}$	$\mathsf{NEXP}$ -c [15]	$\mathsf{EXP}$ , Thm 25 (formerly $\mathsf{2EXP}$ [5])
$\mathsf{GP^{2}}$	$\mathsf{EXP}$ -c, Thm 9 (formerly $\mathsf{EXP}$ -hard, in $\mathsf{3NEXP}$ [4])	Open
$\mathsf{P^{2}}$	Undecidable [4]	No size bound

We give results on the spectrum, but they have applications to decidability of richer logics. $\mathsf{C^{2}}$ can be extended with global unary cardinality constraints: these are of the form $\rho:=\left(\sum_{t\in{\left[n\right]}}\kappa_{t}\cdot|\phi_{t}(x)|\right)\ % \circledast\ \delta$ , where $\phi_{t}$ are $\mathsf{C^{2}}$ formulas in one free variable, $\kappa_{t}$ are integers, $\circledast$ is an inequality or equality, and $\delta$ is an integer. $\rho$ is a sentence, and we define the semantics only for finite structures $M$ . Such $M$ satisfies $\rho$ if, letting $s_{t}$ be the number of elements in $M$ satisfying $\phi_{t}(x)$ , we have $\left(\sum_{t\in{\left[n\right]}}\kappa_{t}\cdot s_{t}\right)\ \circledast\ \delta$ . We write $\mathsf{C^{2}}^{+g}$ for the extension of $\mathsf{C^{2}}$ with global cardinality constraints. As we explain later, computation of the spectrum provides an approach to get tight bounds on these extended logics. In the case where the global constraints are in Presburger arithmetic, these can be seen as an alternative to the technique of [18], which obtains tight bounds for the logic through reduction to satisfiability of $\mathsf{C^{2}}$ itself.

4 Finite satisfiability of $\mathsf{GP^{2}}$ is in EXP

The goal of this section is to prove:

Theorem 9.

The finite satisfiability problem of $\mathsf{GP^{2}}$ is in $\mathsf{EXP}$ .

$\mathsf{GP^{2}}$ infrastructure.

We fix a vocabulary $\sigma$ which consists of $n$ unary predicates $U_{1},\ldots,U_{n}$ and $m$ binary predicates $R_{1},\ldots,R_{m}$ . We consider $\mathsf{GP^{2}}$ sentences $\varphi$ over $\sigma$ in normal form:

\varphi\ :=\ \forall x\ \gamma(x)\ \land\ \bigwedge_{i\in{\left[m\right]}}% \forall x\forall y\ \left(R_{i}(x,y)\land x\neq y\right)\to\alpha_{i}(x,y)\ % \land\ \bigwedge_{i\in{\left[n\right]}}\forall x\ U_{i}(x)\to P_{i}(x),

where $\gamma(x)$ is a quantifier-free formula, each $\alpha_{i}(x,y)$ is a quantifier-free formula, and each $P_{i}(x)$ is a Presburger quantified formula of the form:

P_{i}(x)\ :=\ \left(\sum_{t\in{\left[m\right]}}\lambda_{i,t}\cdot{\#_{y}\left[% R_{t}(x,y)\land x\neq y\right]}\right)\ \circledast_{i}\ \delta_{i}.

Note that in the normal form we allow $\forall x\forall y\ \left(R(x,y)\land x\neq y\right)\to\alpha(x,y)$ which is equivalent to a $\mathsf{GP^{2}}$ sentence.

There is a linear time algorithm that converts every $\mathsf{GP^{2}}$ sentence into an equi-satisfiable sentence in normal form [12], which is based on the standard renaming technique for $\mathsf{GC^{2}}$ introduced in [10, 16]. See the appendix for an argument.

Definition 10 (Compatibility of 1- and 2-types).

For a $\mathsf{GP^{2}}$ sentence $\varphi$ in the normal form above and a 1-type $\pi$ , we say $\pi$ is compatible with $\varphi$ , if $\pi(x)\models\gamma(x)$ , where $\gamma(x)$ is from the normal form, that is, the “unary universal part” of $\varphi$ .

For 1-types $\pi_{1}$ and $\pi_{2}$ , and a 2-type $\eta$ , we say that $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle$ is compatible with $\varphi$ , if

$\blacksquare$

$\pi_{1}(x)\land\eta(x,y)\land\pi_{2}(y)\models\bigwedge_{i\in{\left[m\right]}}% \left(R_{i}(x,y)\land x\neq y\right)\to\alpha_{i}(x,y)$ , and
$\blacksquare$

$\pi_{2}(x)\land\widetilde{\eta}(x,y)\land\pi_{1}(y)\models\bigwedge_{i\in{% \left[m\right]}}\left(R_{i}(x,y)\land x\neq y\right)\to\alpha_{i}(x,y)$ .

That is, the tuple satisfies the “binary universal part”.

We denote the set of 1-types compatible with $\varphi$ by $\mathsf{OneTps}^{\varphi}\subseteq\mathsf{OneTps}$ . Note that it takes time ${\mathcal{O}\left({\left|\varphi\right|}\right)}$ to check compatibility with $\varphi$ either for a $1$ -type $\pi$ or a tuple $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}\times\mathsf{% TwoTps}\times\mathsf{OneTps}$ .

In order to capture the counting conditions, we introduce behavior vectors. Informally, the behavior vector of a vertex encodes the configuration of its neighbors. We fix an ordering of the set $\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ , which has cardinality $2^{n+3m}-2^{n+m}$ . A behavior vector $\mathbf{f}$ is an element of $\mathbb{N}^{2^{n+3m}-2^{n+m}}$ . Abusing notation, we write $\mathbf{f}(\pi,\eta)$ to refer to the $i^{th}$ component of $\mathbf{f}$ , where $i$ is the index of the tuple $\left\langle\pi,\eta\right\rangle$ in the fixed ordering of $\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ .

Definition 11 (Behavior vector of a vertex).

For a $\sigma$ -structure $\mathcal{G}$ and a vertex $v$ in $\mathcal{G}$ , the behavior vector realized by $v$ , denoted by $\mathsf{bh}\left(v\right)$ , is an element of $\mathbb{N}^{2^{n+3m}-2^{n+m}}$ defined as follows: for every $\eta\in\mathsf{TwoTps}^{+}$ and $\pi\in\mathsf{OneTps}$ , $\mathsf{bh}\left(v\right)(\eta,\pi)$ is the number of edges $e$ in $\mathcal{G}$ adjacent to $v$ such that the 2-type of $e$ is $\eta$ and the 1-type of $e$ ’s destination is $\pi$ .

Definition 12 (Characteristic system).

For $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form and 1-type $\pi$ , the characteristic system of $\varphi$ and $\pi$ , denoted $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ , is the integer linear system defined:

$\blacksquare$

The variables of $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ are $x_{\eta,\pi^{\prime}}$ for every $\eta\in\mathsf{TwoTps}^{+}$ and $\pi^{\prime}\in\mathsf{OneTps}$ .
$\blacksquare$

(Compatibility) For every $\eta\in\mathsf{TwoTps}^{+}$ and $\pi^{\prime}\in\mathsf{OneTps}$ if $\pi^{\prime}$ or $\left\langle\pi,\eta,\pi^{\prime}\right\rangle$ is not compatible with $\varphi$ , then $x_{\eta,\pi^{\prime}}=0$ is a constraint in $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ .
$\blacksquare$

(Counting) For $1\leq i\leq n$ , if $U_{i}(x)\in\pi$ then the following constraint is in $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ :

$\left(\sum_{t\in{\left[m\right]}}\lambda_{i,t}\cdot\sum_{\eta\in\mathsf{TwoTps% }_{t}}\sum_{\pi^{\prime}\in\mathsf{OneTps}}x_{\eta,\pi^{\prime}}\right)\ % \circledast_{i}\ \delta_{i}.$

Note that there are ${\left|\mathsf{TwoTps}^{+}\times\mathsf{OneTps}\right|}$ variables and at most $n$ , the number of unary predicates, constraints in $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ . The absolute value of coefficients in $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ is bounded by $K$ , where $K$ is the maximal absolute value of coefficients in $\varphi$ .

Definition 13 (Compatibility of behavior vector).

For a $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form and a 1-type $\pi$ , we say that a behavior vector $\mathbf{f}$ is compatible with $\varphi$ and $\pi$ if $\mathbf{f}$ is a solution of $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ .

We denote the set of all behavior vectors that are compatible with $\varphi$ and $\pi$ by $\mathcal{B}^{\varphi}_{\pi}:=\left\llbracket\mathcal{C}^{\varphi}_{\pi}(% \mathbf{x})\right\rrbracket$ . Note that $\mathcal{B}^{\varphi}_{\pi}$ can be infinite but semilinear.

The following property restates satisfaction of a formula in a $\sigma$ -structure in terms of the type graph of the structure, where the types are identified with vertex- and edge-labels:

Proposition 14.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, $\varphi$ is finitely satisfiable if and only if there exists a colored graph $\mathcal{G}$ satisfying the following conditions:

$\blacksquare$

(1-type) For every vertex $v\in V$ , $\mathsf{OneTp}(v)$ is compatible with $\varphi$ .
$\blacksquare$

(2-type) For every pair of vertices $v_{1},v_{2}\in V$ , $\left\langle\mathsf{OneTp}(v_{1}),\mathsf{TwoTp}(v_{1},v_{2}),\mathsf{OneTp}(v% _{2})\right\rangle$ is compatible with $\varphi$ .
$\blacksquare$

(Counting) For every vertex $v\in V$ , $\mathsf{bh}\left(v\right)$ is compatible with $\mathsf{OneTp}(v)$ and $\varphi$ .

We say that a colored multiple graph in the vocabulary of types, $\mathcal{G}$ , is a finite pseudo-model of a $\mathsf{GP^{2}}$ sentence $\varphi$ if it satisfies all conditions in Proposition 14. Here we show that to establish the finite satisfiability of $\varphi$ , it is sufficient to construct a pseudo-model.

Lemma 15.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, $\varphi$ is finitely satisfiable if and only if it has a finite pseudo-model.

Proof.

Note that the type graph of a finite model of $\varphi$ is a finite pseudo-model of $\varphi$ . Thus we focus on the if direction, constructing (the type graph of) a finite model of $\varphi$ using a duplicating and swapping procedure.

Let $\mathcal{G}_{0}$ be a finite pseudo-model of $\varphi$ , and let $\mathcal{G}^{\prime}_{0}$ be a copy of $\mathcal{G}_{0}$ . Define $\mathcal{G}_{1}$ as the disjoint union of $\mathcal{G}_{0}$ and $\mathcal{G}^{\prime}_{0}$ , after iteratively applying the following swapping procedure: for every pair of vertices $v$ and $u$ in $\mathcal{G}_{0}$ with more than one edge between them, let $e$ be an edge between them, and let $e^{\prime}$ be the corresponding edge in $\mathcal{G}^{\prime}_{0}$ . We then swap the destinations of $e$ and $e^{\prime}$ in $\mathcal{G}_{1}$ .

It is straightforward to verify that $\mathcal{G}_{1}$ is a pseudo-model of $\varphi$ and its multiplicity is one less than $\mathcal{G}_{0}$ . We can repeat this procedure until we obtain a finite pseudo-model $\mathcal{G}_{t}$ where no two vertices have multiple edges. Finally, the type graph of the finite model of $\varphi$ is obtained by connecting all remaining pairs in $\mathcal{G}_{t}$ with the silent type. $\hfill\blacktriangleleft$

The main construction.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, we assume that for every 1-type $\pi\in\mathsf{OneTps}^{\varphi}$ , $\mathbf{0}\not\in\mathcal{B}^{\varphi}_{\pi}$ . Otherwise $\varphi$ is trivially satisfiable by a model with only one vertex with 1-type $\pi$ .

Lemma 16.

A $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form is finitely satisfiable if and only if there exists vectors $\mathbf{g}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ for each $\pi\in\mathsf{OneTps}^{\varphi}$ satisfying the following conditions.

$\blacksquare$

(Matching) For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , $\mathbf{g}_{\pi_{1}}(\eta,\pi_{2})=\mathbf{g}_{\pi_{2}}(\widetilde{\eta},\pi_{% 1})$ .
$\blacksquare$

(Non-triviality) There exists some $\pi\in\mathsf{OneTps}^{\varphi}$ such that $\mathbf{g}_{\pi}\neq\mathbf{0}$ .

Proof.

Suppose that $\varphi$ is finitely satisfiable with finite model $\mathcal{G}$ .

For a 1-type $\pi$ , let $V_{\pi}\subseteq V$ be the set of vertices $v$ in $\mathcal{G}$ with 1-type $\pi$ . Note that the $V_{\pi}$ partition $V$ . Since $\mathcal{G}\models\varphi$ , for every $v$ in $V_{\pi}$ , $\mathsf{bh}\left(v\right)\in\mathcal{B}^{\varphi}_{\pi}$ . We claim that $\mathbf{g}_{\pi}=\sum_{v\in V_{\pi}}\mathsf{bh}\left(v\right)\in\mathsf{% KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ satisfies the conditions.

$\blacksquare$

(Matching) For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , note that
$\displaystyle\sum_{v\in V_{\pi_{1}}}\mathsf{bh}\left(v\right)(\eta,\pi_{2})\ =$ $\displaystyle\sum_{v\in V_{\pi_{1}}}{\left|\left\{u\in V\middle|\ \text{$v\neq u% $, $\mathsf{TwoTp}(v,u)=\eta$, and $\mathsf{OneTp}(u)=\pi_{2}$}\right\}\right|}$ $\displaystyle\ =$ $\displaystyle{\left|\left\{(v,u)\in V^{2}\middle|\ \text{$v\neq u$, $\mathsf{% OneTp}(v)=\pi_{2}$, $\mathsf{TwoTp}(v,u)=\eta$, and $\mathsf{OneTp}(u)=\pi_{2}% $}\right\}\right|}.$

That is, $\mathbf{g}_{\pi_{1}}(\eta,\pi_{2})$ is the number of edges with types $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle$ in $\mathcal{G}$ . Similarly, $\mathbf{g}_{\pi_{2}}(\widetilde{\eta},\pi_{1})$ is the number of edges with types $\left\langle\pi_{2},\widetilde{\eta},\pi_{1}\right\rangle$ in $\mathcal{G}$ . Since the number of edges with types $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle$ and $\left\langle\pi_{2},\widetilde{\eta},\pi_{1}\right\rangle$ should be the same, the Matching constraint holds.
$\blacksquare$

(Non-triviality) Since $\mathcal{G}$ is non-empty, by our assumption, it has a vertex $v$ with 1-type $\pi$ satisfying that $\mathsf{bh}\left(v\right)\neq\mathbf{0}$ . Therefore, $\mathbf{g}_{\pi}=\mathsf{bh}\left(v\right)+\sum_{u\in V_{\pi}\setminus\left\{v% \right\}}\mathsf{bh}\left(u\right)\neq\mathbf{0}$ .

Suppose that there exists such $\mathbf{g}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ for $\pi\in\mathsf{OneTps}^{\varphi}$

. By the definition of Kleene star, for every $\pi\in\mathsf{OneTps}^{\varphi}$ , there exists $\mathbf{f}_{\pi,1},\ldots,\mathbf{f}_{\pi,\ell_{\pi}}\in\mathcal{B}^{\varphi}_% {\pi}$ , not necessarily distinct, such that $\mathbf{g}_{\pi}=\sum_{i\in{\left[\ell_{\pi}\right]}}\mathbf{f}_{\pi,i}$ . We construct a colored multigraph $\mathcal{G}$ , which will be the type graph of our structure, as follows. The vertices in $\mathcal{G}$ are $\bigcup_{\pi\in\mathsf{OneTps}^{\varphi}}\left\{v_{\pi,1},\ldots,v_{\pi,\ell_{% \pi}}\right\}$ . Each vertex $v_{\pi,i}$ is colored with a $1$ -type $\pi$ , and we let $V_{\pi}$ be the set of vertices colored with $\pi$ . For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , we add edges between $V_{\pi_{1}}$ and $V_{\pi_{2}}$ such that for each $v_{\pi_{1},i}$ , the number of edges connected to it with 2-type $\eta$ is $\mathbf{f}_{\pi_{1},i}(\eta,\pi_{2})$ and for each $v_{\pi_{2},i}$ , the number of edges connected to it with 2-type $\eta$ is $\mathbf{f}_{\pi_{2},i}(\widetilde{\eta},\pi_{1})$ . Note that by the Matching constraint, $\mathbf{g}_{\pi_{1}}(\eta,\pi_{2})=\mathbf{g}_{\pi_{2}}(\widetilde{\eta},\pi_{% 1})$ , so this construction is always possible. We claim that $\mathcal{G}$ is a pseudo-model of $\varphi$ . Note that each vertex in $\mathcal{G}$ is colored with 1-type in $\mathsf{OneTps}^{\varphi}$ , each edge in $\mathcal{G}$ is colored with 2-type in $\mathsf{TwoTps}^{+}$ , and it is routine to check that the behavior vector of $v_{\pi,i}$ is $\mathbf{f}_{\pi,i}$ . By the Non-triviality constraint, $\mathcal{G}$ is non-empty. Thus by Lemma 15, $\varphi$ is finitely satisfiable. $\hfill\blacktriangleleft$

Above we connected the finite satisfiability problem of $\mathsf{GP^{2}}$ sentence $\varphi$ and the Kleene star of behavior vectors. However, because the cardinality of the set $\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ is infinite, it is not clear how to determine the solvability of the conditions in Lemma 16. In addition, this representation does not tell us anything about the shape of the models.

Recall that the set of behavior vectors $\mathcal{B}^{\varphi}_{\pi}$ is the solution set of the characteristic system $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ . We can apply Lemma 3 and obtain that

\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)\ =\ \mathsf{% KleeneStar}\left(\left\llbracket\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})\right% \rrbracket\right)\ =\ \left\llbracket\tilde{\mathcal{C}}^{\varphi}_{\pi}(% \mathbf{x})\right\rrbracket.

Thus the conditions in Lemma 16 can be encoded in the following integer linear system.

Definition 17.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, the integer linear system $\mathcal{Q}^{\varphi}(\mathbf{x})$ is defined as follows.

$\blacksquare$

The variables of $\mathcal{Q}^{\varphi}(\mathbf{x})$ are $x_{\pi_{1},\eta,\pi_{2}}$ for every $\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}$ and $\eta\in\mathsf{TwoTps}^{+}$ . Let $\mathbf{x}_{\pi_{1}}$ denote the vector of variables $x_{\pi_{1},\eta,\pi_{2}}$ .
$\blacksquare$

(Structure) For every $\pi\in\mathsf{OneTps}^{\varphi}$ , $\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x}_{\pi})$ is part of $\mathcal{Q}^{\varphi}(\mathbf{x})$ , where $\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x})$ is the integer linear system obtained by applying Lemma 3 to the characteristic system $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ .
$\blacksquare$

(Matching) For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , the following constraint is in $\mathcal{Q}^{\varphi}(\mathbf{x})$ , $x_{\pi_{1},\eta,\pi_{2}}=x_{\pi_{2},\widetilde{\eta},\pi_{1}}$ , where we recall that $\widetilde{\eta}$ denotes the dual 2-type.
$\blacksquare$

(Non-triviality) $\sum_{\pi_{1}\in\mathsf{OneTps}^{\varphi}}\sum_{\eta\in\mathsf{TwoTps}^{+}}% \sum_{\pi_{2}\in\mathsf{OneTps}^{\varphi}}x_{\pi_{1},\eta,\pi_{2}}>0$ .

Lemma 18.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, $\varphi$ is finitely satisfiable if and only if $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ .

Proof.

Suppose that $\varphi$ is finitely satisfiable.

By Lemma 16, there exists $\mathbf{g}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ for $\pi\in\mathsf{OneTps}^{\varphi}$ satisfying the Matching and Non-triviality conditions.

For every $\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}$ and $\eta\in\mathsf{TwoTps}^{+}$ , let $a_{\pi_{1},\eta,\pi_{2}}:=\mathbf{g}_{\pi_{1}}(\eta,\pi_{2})$ . We claim that assigning $x_{\pi_{1},\eta,\pi_{2}}$ to $a_{\pi_{1},\eta,\pi_{2}}$ gives a solution of the system $\mathcal{Q}^{\varphi}(\mathbf{x})$ .

$\blacksquare$

(Structure) By definition, for every $\pi\in\mathsf{OneTps}^{\varphi}$ , $\mathbf{g}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ . By Lemma 3, $\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)=\mathsf{KleeneStar% }\left(\left\llbracket\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})\right\rrbracket% \right)=\left\llbracket\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x})\right\rrbracket$ . Thus, $\mathbf{a}_{\pi}$ is a solution of $\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x})$ .
$\blacksquare$

(Matching) For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , by the Matching condition in Lemma 16, $\mathbf{g}_{\pi_{1}}(\eta,\pi_{2})=\mathbf{g}_{\pi_{2}}(\widetilde{\eta},\pi_{% 1})$ . Thus $a_{\pi_{1},\eta,\pi_{2}}=a_{\pi_{2},\widetilde{\eta},\pi_{1}}$ .

\blacksquare

(Non-triviality) By the Non-triviality condition in Lemma 16, there exists a 1-type $\pi\in\mathsf{OneTps}^{\varphi}$ such that $\mathbf{g}_{\pi}\neq\mathbf{0}$ . Therefore,

	$\displaystyle\sum_{\pi_{1}\in\mathsf{OneTps}^{\varphi}}\sum_{\eta\in\mathsf{% TwoTps}^{+}}\sum_{\pi_{2}\in\mathsf{OneTps}^{\varphi}}a_{\pi_{1},\eta,\pi_{2}}\ =$	$\displaystyle\sum_{\pi_{1}\in\mathsf{OneTps}^{\varphi}}\sum_{\eta\in\mathsf{% TwoTps}^{+}}\sum_{\pi_{2}\in\mathsf{OneTps}^{\varphi}}\mathbf{g}_{\pi_{1}}(% \eta,\pi_{2})$
	$\displaystyle\ \geq$	$\displaystyle\sum_{\eta\in\mathsf{TwoTps}^{+}}\sum_{\pi_{2}\in\mathsf{OneTps}^% {\varphi}}\mathbf{g}_{\pi}(\eta,\pi_{2})\ >0.$

Suppose that $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution, assigning $x_{\pi_{1},\eta,\pi_{2}}$ to $a_{\pi_{1},\eta,\pi_{2}}$ .

For every $\pi\in\mathsf{OneTps}^{\varphi}$ , since $\mathbf{a}_{\pi}$ is a valid assignment of $\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x})$ , by Lemma 3, $\mathbf{a}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ . We claim that $\mathbf{a}_{\pi}$ are vectors satisfying the conditions in Lemma 16, which implies that $\varphi$ is finitely satisfiable. The proof of Non-triviality is routine. Here we focus on the Matching constraint. For every $\left\langle\pi_{1},\eta,\pi_{2}\right\rangle\in\mathsf{OneTps}^{\varphi}% \times\mathsf{TwoTps}^{+}\times\mathsf{OneTps}^{\varphi}$ , by the Matching condition of $\mathcal{Q}^{\varphi}$ , $a_{\pi_{1},\eta,\pi_{2}}=a_{\pi_{2},\widetilde{\eta},\pi_{1}}$ . Since $\mathbf{a}_{\pi_{1}}(\eta,\pi_{2})=a_{\pi_{1},\eta,\pi_{2}}$ , we have $\mathbf{a}_{\pi_{1}}(\eta,\pi_{2})=\mathbf{a}_{\pi_{2}}(\widetilde{\eta},\pi_{% 1})$ . $\hfill\blacktriangleleft$

The system $\mathcal{Q}^{\varphi}(\mathbf{x})$ is a Boolean combination of exponentially many integer linear constraints, and thus can be solved in $\mathsf{NEXP}$ . To get $\mathsf{EXP}$ , we apply an idea from [16], refining to get exponentially many homogeneous constraints.

Definition 19.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, for $M\in\mathbb{N}$ , the integer linear system $\mathcal{Q}_{M}^{\prime\varphi}(\mathbf{x})$ is the system $\mathcal{Q}^{\varphi}(\mathbf{x})$ where the Structure constraint is replaced with:

$\blacksquare$

(Structure^′) For every $\pi\in\mathsf{OneTps}^{\varphi}$ ,

$\exists\mathbf{y}_{1},\mathbf{y}_{2}\ (\mathbf{x}_{\pi}\ =\ \mathsf{proj}_{n}% \left(\mathbf{y}_{1}\right)+\mathbf{y}_{2})\ \land\ (\tilde{\mathbf{A}}\mathbf% {y}_{1}\ =\ \mathbf{0})\ \land\ (\mathbf{A}\mathbf{y}_{2}\ =\ \mathbf{0})\ % \land\ ((\mathbf{1}\cdot\mathbf{y}_{2})\leq M(\mathbf{1}\cdot\mathbf{y}_{2})),$

where $\tilde{\mathbf{A}}$ is the matrix obtained by applying Lemma 3 to the characteristic system $\mathcal{C}^{\varphi}_{\pi}(\mathbf{x})$ .

Lemma 20.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, there exists $M^{\varphi}\in\mathbb{N}$ , such that for every $M\geq M^{\varphi}$ , $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ if and only if $\mathcal{Q}_{M}^{\prime\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ .

Moreover, $M^{\varphi}$ can be computed directly from $\varphi$ in time exponential in the length of $\varphi$ , assuming binary encoding of coefficients.

Proof.

By Lemma 1, if $\mathcal{Q}^{\varphi}$ has a solution in $\mathbb{N}$ , then it has a “small solution”: every value is bounded by $M_{0}^{\varphi}=c_{1}t\left(t\widetilde{\lambda}\right)^{c_{2}t}$ , where $\widetilde{\lambda}$ is the maximal coefficient in $\varphi$ and $t$ is the number of constraints in $\mathcal{Q}^{\varphi}$ , which is exponential in the number of unary and binary predicates. Thus $M_{0}^{\varphi}$ can be computed directly from $\varphi$ in time exponential in the length of $\varphi$ , assuming binary encoding of coefficients. Let $M^{\varphi}=2^{n}M_{0}^{\varphi}$ .

Note that the only difference between $\mathcal{Q}^{\varphi}(\mathbf{x})$ and $\mathcal{Q}_{M}^{\prime\varphi}(\mathbf{x})$ pertains to constraints $(\mathbf{y}_{1}=\mathbf{0})\to(\mathbf{y}_{2}=\mathbf{0})$ and $((\mathbf{1}\cdot\mathbf{y}_{2})\leq M(\mathbf{1}\cdot\mathbf{y}_{1}))$ . We show that the two systems are equi-satisfiable, provided $M$ is sufficiently large.

Suppose that $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ .

We claim that a small solution $\mathbf{a}_{\pi}$ of $\mathcal{Q}^{\varphi}(\mathbf{x})$ is a solution of $\mathcal{Q}^{\prime\varphi}(\mathbf{x})$ . For every $\pi\in\mathsf{OneTps}^{\varphi}$ , let $\mathbf{b}_{1}$ and $\mathbf{b}_{2}$ be corresponding assignments for $\mathbf{y}_{1}$ and $\mathbf{y}_{2}$ in $\tilde{\mathcal{C}}^{\varphi}_{\pi}(\mathbf{x}_{\pi})$ . If $\mathbf{a}_{\pi}=\mathbf{0}$ , then $\mathbf{b}_{1}=\mathbf{0}$ and $\mathbf{b}_{2}=\mathbf{0}$ , which implies that $(\mathbf{1}\cdot\mathbf{b}_{2})\leq M^{\varphi}(\mathbf{1}\cdot\mathbf{b}_{1})$ holds trivially. On the other hand, if $\mathbf{a}_{\pi}\neq\mathbf{0}$ , then $\mathbf{b}_{1}\neq\mathbf{0}$ , which implies that $(\mathbf{1}\cdot\mathbf{b}_{1})\geq 1$ . Therefore $(\mathbf{1}\cdot\mathbf{b}_{2})\ \leq\ 2^{n}M_{0}^{\varphi}\ =\ M^{\varphi}\ % \leq\ M\ \leq\ M(\mathbf{1}\cdot\mathbf{b}_{1})$

Suppose that $\mathcal{Q}_{M}^{\prime\varphi}(\mathbf{x})$ has a solution $\mathbf{a}_{\pi}$ in $\mathbb{N}$ .

We claim that the $\mathbf{a}_{\pi}$ also form a solution to $\mathcal{Q}^{\varphi}(\mathbf{x})$ . It is sufficient to show that, for vectors $\mathbf{b}_{1}$ and $\mathbf{b}_{2}$ , if $(\mathbf{1}\cdot\mathbf{b}_{2})\leq M(\mathbf{1}\cdot\mathbf{b}_{1})$ , then $(\mathbf{b}_{1}=\mathbf{0})\to(\mathbf{b}_{2}=\mathbf{0})$ . If $\mathbf{b}_{1}=\mathbf{0}$ , then $(\mathbf{1}\cdot\mathbf{b}_{2})\leq M(\mathbf{1}\cdot\mathbf{b}_{1})=0$ , which implies that $\mathbf{b}_{2}=\mathbf{0}$ . Otherwise if $\mathbf{b}_{1}\neq\mathbf{0}$ , then $(\mathbf{b}_{1}=\mathbf{0})\to(\mathbf{b}_{2}=\mathbf{0})$ holds trivially. $\hfill\blacktriangleleft$

We are now ready to prove Theorem 9:

Proof.

For every $\mathsf{GP^{2}}$ sentence $\varphi$ in normal form, by Lemma 16, Lemma 18, and Lemma 20, $\varphi$ is finitely satisfiable if and only if $\mathcal{Q}_{M^{\varphi}}^{\prime\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ . Note that $\mathcal{Q}_{M^{\varphi}}^{\prime\varphi}(\mathbf{x})$ is an integer linear system with $2^{\mathcal{O}\left(m\left(n+\log K\right)\right)}$ variables, $2^{\mathcal{O}\left(m\left(n+\log K\right)\right)}$ constraints, and coefficients bounded by $M^{\varphi}$ . Moreover, $\mathcal{Q}_{M^{\varphi}}^{\prime\varphi}(\mathbf{x})$ is homogeneous. Thus, it has a solution in the natural numbers if and only if it has a rational solution. The feasibility of an integer linear system over the rationals can be checked in time polynomial in the number of variables, the number of equations, and the logarithm of the absolute value of the maximum coefficients [9]. Consequently, this process takes time exponential in the length of $\varphi$ , assuming binary encoding of coefficients $\hfill\blacktriangleleft$

Note that the solutions to the linear system used in proving Theorem 9 will contain a representation of every finite model: the vector of cardinalities of $1$ -types. But it contains additional vectors that do not correspond to the cardinalities of one types in any model. This is related to the fact that while existence of a pseudo-model implies existence of a model (Lemma 15), cardinalities are not preserved in moving from a pseudo-model to the corresponding model. We return to this in Section 6.

5 Spectra of $\mathsf{C^{2}}$ formulas

In this section we will consider converting formulas in logic with arithmetic into linear constraints. These constraints will characterize the set of models of a $\mathsf{C^{2}}$ formula. With this characterization in place, we have reduced finite satisfiability of the formula to a check for satisfiability of the conjunction of the linear constraints, which can be done via standard linear algebra solving. From this it will follow that $\mathsf{C^{2}}$ with a variety of global cardinality constraints is decidable: we just conjoined the cardinality constraints with the constraints characterizing the models.

We fix a vocabulary $\sigma$ which consists of $n$ unary predicates $U_{1},\ldots,U_{n}$ and $m$ binary predicates $R_{1},\ldots,R_{m}$ . We consider $\mathsf{C^{2}}$ sentence $\varphi$ over $\sigma$ in normal form:

\varphi\ :=\ \forall x\ \gamma(x)\ \land\ \forall x\ \forall y\ \left(x\neq y% \to\alpha(x,y)\right)\ \land\ \bigwedge_{i\in{\left[m^{\prime}\right]}}\forall x% \ \exists^{=k_{i}}y\ \left(R_{i}(x,y)\land x\neq y\right),

where $\gamma(x)$ and $\alpha(x,y)$ are quantifier-free, $R_{i}$ are binary predicates, $0\leq m^{\prime}\leq m$ , and $k_{i}\in\mathbb{N}$ .

Definition 21 (Count bound vector).

The count bound vector of $\varphi$ , denoted by $\mathbf{k}^{\varphi}$ , is the $m^{\prime}$ dimension vector such that the $i^{th}$ component of $\mathbf{k}^{\varphi}$ is $k_{i}$ .

We denote the sum of $k_{i}$ by $K^{\varphi}$ .

Definition 22 (Forward and backward characteristic vector of 2-types).

For $m^{\prime}$ as above and a 2-type $\eta$ , the forward characteristic vector of $\eta$ , denoted by $\eta^{\triangleright}$ , is an $m^{\prime}$ dimensional vector defined: for every $1\leq i\leq m^{\prime}$ , if $R_{i}(x,y)\in\eta$ , then the $i^{th}$ component of $\eta^{\triangleright}$ is 1. Otherwise, it is $0$ . The backward characteristic vector of $\eta$ , denoted by $\eta^{\triangleleft}$ , is defined similarly.

Definition 23 (Forward and backward silent 2-type).

For $m^{\prime}$ as above and a 2-type $\eta$ we say that $\eta$ is forward-silent if for $1\leq i\leq m^{\prime}$ , $\neg R_{i}(x,y)\in\eta$ . Backward-silent is defined similarly.

We define the notions of $\mathsf{OneTps}^{\varphi}$ and $\mathsf{TwoTps}^{\varphi}_{\pi_{1},\pi_{2}}$ similarly to those in $\mathsf{GP^{2}}$ . We also define $\mathsf{TwoTps}^{\varphi,\mathsf{silent}}_{\pi_{1},\pi_{2}}\subseteq\mathsf{% TwoTps}^{\varphi}_{\pi_{1},\pi_{2}}$ as the set of 2-types that are both forward- and backward-silent, $\mathsf{TwoTps}^{\varphi,\triangleright}_{\pi_{1},\pi_{2}}$ for 2-types that are not forward-silent but are backward-silent, and $\mathsf{TwoTps}^{\varphi,\triangleright\triangleleft}_{\pi_{1},\pi_{2}}$ for 2-types that are neither forward- nor backward-silent.

In the rest of the section, we deal only with normal form sentences. We explain how the results apply to arbitrary $\mathsf{C^{2}}$ sentences in the appendix.

Definition 24 (Spectrum and $1$ -type spectrum).

For every $\mathsf{C^{2}}$ sentence $\varphi$ , the spectrum of $\varphi$ , denoted by $\mathsf{SPEC}(\varphi)$ , is the set of natural numbers that are sizes of finite models of $\varphi$ .

The 1-type spectrum of $\varphi$ , denoted by $\Pi\text{-}\mathsf{SPEC}(\varphi)$ , is the set of 1-type cardinality vectors (see Definition 8) corresponding to finite models of $\varphi$ .

We aim to show:

Theorem 25.

For every $\mathsf{C^{2}}$ sentence $\varphi$ , $\mathsf{SPEC}(\varphi)$ and $\Pi\text{-}\mathsf{SPEC}(\varphi)$ are semilinear. Furthermore, each spectrum can be represented by an existential Presburger formula of size doubly exponential in $\varphi$ .

Definition 26 (Silent compatible 1-types).

For a pair of 1-types $\pi_{1}$ and $\pi_{2}$ , we say that $\pi_{1}$ and $\pi_{2}$ are silent-compatible w.r.t. $\varphi$ , if $\mathsf{TwoTps}^{\varphi,\mathsf{silent}}_{\pi_{1},\pi_{2}}$ is non-empty. Otherwise, we say, following [15], that $\pi_{1}$ and $\pi_{2}$ are a noisy pair.

Lemma 27.

For every $\mathsf{C^{2}}$ sentence $\varphi$ in normal form and $\sigma$ -structure $\mathcal{G}\models\varphi$ , for every pair of 1-types $\pi_{1}$ and $\pi_{2}$ , if $\pi_{1}$ and $\pi_{2}$ are a noisy pair (w.r.t. $\varphi$ ), then at least one of the 1-types $\pi_{1}$ or $\pi_{2}$ is realized by at most $2K^{\varphi}+1$ vertices in $\mathcal{G}$ .

Proof.

Recall that $V_{\pi}$ denotes the vertices in $V$ with 1-type $\pi$ . Because $\mathcal{G}\models\varphi$ , for vertex $v\in\mathcal{G}$ , $\sum_{u\in V\setminus\left\{v\right\}}\mathsf{TwoTp}^{\triangleright}(v,u)=% \mathbf{k}^{\varphi}$ . We consider two cases.

Suppose that $\pi_{1}=\pi_{2}$ .

Since $\mathsf{TwoTp}^{\triangleright}(v,u)=\mathsf{TwoTp}^{\triangleleft}(u,v)$ , we have

	$\displaystyle\sum_{v\in V_{\pi_{1}}}\sum_{u\in V_{\pi_{1}}\setminus\left\{v% \right\}}(\mathsf{TwoTp}^{\triangleright}(v,u)+\mathsf{TwoTp}^{\triangleleft}(% v,u))\ =$	$\displaystyle 2\sum_{v\in V_{\pi_{1}}}\sum_{u\in V_{\pi_{1}}\setminus\left\{v% \right\}}\mathsf{TwoTp}^{\triangleright}(v,u)$
	$\displaystyle\ \preccurlyeq$	$\displaystyle 2\sum_{v\in V_{\pi_{1}}}\sum_{u\in V\setminus\left\{v\right\}}% \mathsf{TwoTp}^{\triangleright}(v,u)\ =2{\left\|V_{\pi_{1}}\right\|}\mathbf{k}^{% \varphi}.$

For every pair of vertices $v$ and $u$ in $V_{\pi_{1}}$ with $v\neq u$ , by definition of noisy pair, the sum of components of $\mathsf{TwoTp}^{\triangleright}(v,u)+\mathsf{TwoTp}^{\triangleleft}(v,u)$ is at least $1$ . Therefore, we have

\sum_{v\in V_{\pi_{1}}}\sum_{u\in V_{\pi_{1}}\setminus\left\{v\right\}}1\ =\ {% \left|V_{\pi_{1}}\right|}\cdot({\left|V_{\pi_{1}}\right|}-1)\ \leq\ 2{\left|V_% {\pi_{1}}\right|}\cdot K^{\varphi},

which implies that ${\left|V_{\pi_{1}}\right|}\leq 2K^{\varphi}+1$ .

Suppose that $\pi_{1}\neq\pi_{2}$ .

By a similar argument, ${\left|V_{\pi_{1}}\right|}\cdot{\left|V_{\pi_{2}}\right|}\leq({\left|V_{\pi_{1% }}\right|}+{\left|V_{\pi_{2}}\right|})\cdot K^{\varphi}$ . If ${\left|V_{\pi_{1}}\right|}\leq 2K^{\varphi}+1$ we are done. So assume the opposite. Then we have

{\left|V_{\pi_{2}}\right|}\ \leq\ \frac{K^{\varphi}}{1-\frac{K^{\varphi}}{{% \left|V_{\pi_{1}}\right|}}}\ \leq\ \frac{K^{\varphi}}{1-\frac{K^{\varphi}}{2K^% {\varphi}+1}}\ \leq\ 2K^{\varphi}.\

$\hfill\blacktriangleleft$

The following straightforward proposition gives conditions that characterize the satisfiability of $\mathsf{C^{2}}$ by a model in terms of the prior constructs.

Proposition 28.

For every $\mathsf{C^{2}}$ sentence $\varphi$ in normal form and $\sigma$ -structure $\mathcal{G}$ , $\mathcal{G}$ is a model of $\varphi$ if and only if following conditions hold. For every $v,u\in V$ with $v\neq u$ ,

$\blacksquare$

(1-type) $\mathsf{OneTp}(v)\in\mathsf{OneTps}^{\varphi}$ ,
$\blacksquare$

(2-type) $\mathsf{TwoTp}(v,u)\in\mathsf{TwoTps}^{\varphi}_{\mathsf{OneTp}(v),\mathsf{% OneTp}(u)}$ , and
$\blacksquare$

(Counting) $\sum_{u\in V\setminus\left\{v\right\}}\mathsf{TwoTp}^{\triangleright}(v,u)=% \mathbf{k}^{\varphi}$ ,

where $\mathbf{k}^{\varphi}$ is the count bound vector of $\varphi$ .

Definition 29 (Partial model of $\mathsf{C^{2}}$ sentence).

For every $\mathsf{C^{2}}$ sentence $\varphi$ and $\sigma$ -structure $\mathcal{G}$ , we say that a complete colored graph $\mathcal{G}$ is a partial model of $\varphi$ if $\mathcal{G}$ satisfies the first two conditions in Proposition 28.

The following is obvious.

Lemma 30.

For every $\mathsf{C^{2}}$ sentence $\varphi$ in normal form, for every $\sigma$ -structure $\mathcal{G}\models\varphi$ , for every $\mathcal{H}\subseteq\mathcal{G}$ , $\mathcal{H}$ is a partial model of $\varphi$ .

Core of structures.

Definition 31.

For $\mathcal{G}$ a $\sigma$ -structure, $\ell\in\mathbb{N}$ , we say that substructure $\mathcal{H}\subseteq\mathcal{G}$ is an $\ell$ -core of $\mathcal{G}$ if

$\blacksquare$

for every 1-type $\pi$ , the number of vertices in $\mathcal{G}\setminus\mathcal{H}$ with 1-type $\pi$ is either $0$ or at least $\ell$
$\blacksquare$

for 1-types $\pi_{1}$ , $\pi_{2}$ , and 2-type $\eta$ , there are either $0$ and at least $\ell$ pairs of vertices $v,u\in\mathcal{G}\setminus\mathcal{H}$ satisfying that $v\neq u$ , $\mathsf{OneTp}(v)=\pi_{1}$ , $\mathsf{TwoTp}(v,u)=\eta$ , and $\mathsf{OneTp}(u)=\pi_{2}$ .

Note that the core of $\mathcal{G}$ is not unique, and $\mathcal{G}$ is trivially a core of itself for every $\ell\in\mathbb{N}$ . Therefore, we are interested in the existence of a small core of $\mathcal{G}$ . We can show that for every $\ell$ , every $\sigma$ -structure has an exponential-size core.

Lemma 32.

For every $\sigma$ -structure $\mathcal{G}$ , for every $\ell\in\mathbb{N}$ , $\mathcal{G}$ has an $\ell$ -core $\mathcal{H}$ with size at most $(2^{2n+4m+2})\cdot\ell$ .

The intuition behind the construction is to repeatedly select a 1-type or tuple that violates the $\ell$ -core condition and add the relevant vertices to $\mathcal{H}$ . Since there are only finitely many such choices, the process eventually stabilizes, and the size of the constructed core remains bounded: see the appendix for details.

For a $\mathsf{C^{2}}$ sentence $\varphi$ and a $\sigma$ -structure $\mathcal{G}\models\varphi$ , if $\mathcal{H}$ is a $\ell$ -core of $\mathcal{G}$ with sufficiently large $\ell$ , then we have the following important property of $\mathcal{G}\setminus\mathcal{H}$ :

Lemma 33.

For every $\mathsf{C^{2}}$ sentence $\varphi$ and $\sigma$ -structure $\mathcal{G}\models\varphi$ , for every $\ell$ -core $\mathcal{H}\subseteq\mathcal{G}$ with $\ell>2K^{\varphi}+1$ , the 1-types realized in $\mathcal{G}\setminus\mathcal{H}$ are silent-compatible (w.r.t. $\varphi$ ).

Proof.

Suppose that there exist 1-types $\pi_{1}$ and $\pi_{2}$ realized in $\mathcal{G}\setminus\mathcal{H}$ which are not silent-compatible. By Lemma 27, at least one of the 1-types $\pi_{1}$ or $\pi_{2}$ is realized by at most $2K^{\varphi}+1$ vertices in $\mathcal{G}$ . Without loss of generality, suppose that $\pi_{1}$ is realized by at most $2K^{\varphi}+1$ vertices in $\mathcal{G}$ , then there are at most $2K^{\varphi}+1<\ell$ vertices in $\mathcal{G}\setminus\mathcal{H}$ realized $\pi_{1}$ . However, by the definition of $\ell$ -core, since $\pi_{1}$ is realized in $\mathcal{G}\setminus\mathcal{H}$ , it is realized by at least $\ell$ vertices in $\mathcal{G}\setminus\mathcal{H}$ . This leads to a contradiction. $\hfill\blacktriangleleft$

In Section 4, we introduced the notion of behavior vectors to describe the number of edges connected to a given vertex with specific 2-types. In this section, we consider $\sigma$ -structures with a fixed core and extend the concept of behavior vectors to incorporate information about the core. Again, we fix an ordering of the set $\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ , which has cardinality $2^{n+3m}-2^{n+m}$ .

Definition 34 (Extended behavior).

Fixing a vocabulary $\sigma$ , an extended behavior w.r.t. a set of vertices $V$ is a tuple $\left\langle g,\mathbf{f}\right\rangle$ where $g$ is a mapping from a vertex $v\in V$ to a 2-type in $\mathsf{TwoTps}$ , and $\mathbf{f}$ is an element of $\mathbb{N}^{2^{n+3m}-2^{n+m}}$ .

Informally, each extended behavior consists of two components. The first one is a mapping from vertices in the core to 2-types, capturing the 2-type realized by the edge between a given vertex and core vertices. The second component is a behavior vector.

Abusing notation, for an extended behavior $\left\langle g,\mathbf{f}\right\rangle$ , we will write $g^{\triangleright}(v)$ for ${(g(v))}^{\triangleright}$ and $\widetilde{g}(v)$ for the dual of $g(v)$ . We will also write $\mathbf{f}(\eta,\pi)$ for the $i^{th}$ component of $\mathbf{f}$ , where $i$ is the index of the tuple $\left\langle\eta,\pi\right\rangle$ in the fixed ordering of $\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ .

Definition 35 (Compatibility of extended behaviors).

For a $\mathsf{C^{2}}$ sentence $\varphi$ in normal form, $\pi\in\mathsf{OneTps}^{\varphi}$ , and a $\sigma$ -structure $\mathcal{H}$ with vertices $V$ , we say that an extended behavior function $\left\langle g,\mathbf{f}\right\rangle$ w.r.t. $V$ is compatible with $\varphi$ , $\pi$ , and $\mathcal{H}$ if $f$ satisfies:

1.

(Compatibility with $\mathcal{H}$ ) For every $v\in V$ , $g(v)\in\mathsf{TwoTps}^{\varphi}_{\pi,\mathsf{OneTp}(v)}$ .
2.

(Compatibility with 1- and 2- types) For every $\left\langle\eta,\pi^{\prime}\right\rangle\in\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ , if $\pi^{\prime}\not\in\mathsf{OneTps}^{\varphi}$ or $\eta\not\in\mathsf{TwoTps}^{\varphi}_{\pi,\pi^{\prime}}$ , then $\mathbf{f}(\eta,\pi^{\prime})=0$ .
3.

(Forward-silent zero) For every $\left\langle\eta,\pi^{\prime}\right\rangle\in\mathsf{TwoTps}^{+}\times\mathsf{OneTps}$ , if $\eta$ is forward-silent, then $\mathbf{f}(\eta,\pi^{\prime})=0$ .

4.

(Counting) The remaining entries of $\mathbf{f}$ , that is, entries for $2$ -types that are not forward-silent, are bounded by the following constraint:

\sum_{v\in V}g^{\triangleright}(v)+\sum_{\pi^{\prime}\in\mathsf{OneTps}^{% \varphi}}\left(\sum_{\eta\in\mathsf{TwoTps}^{\varphi,\triangleright}_{\pi,\pi^% {\prime}}}\mathbf{f}(\eta,\pi^{\prime})\cdot\eta^{\triangleright}+\sum_{\eta% \in\mathsf{TwoTps}^{\varphi,\triangleright\triangleleft}_{\pi,\pi^{\prime}}}% \mathbf{f}(\eta,\pi^{\prime})\cdot\eta^{\triangleright}\right)\ =\ \mathbf{k}^% {\varphi}.

Note that this condition implies that if $\pi^{\prime}$ and $\eta$ are compatible with $\varphi$ , and $\eta$ is not forward-silent, then $\mathbf{f}(\eta,\pi^{\prime})$ is bounded by $K^{\varphi}$ .

Note that given an extended behavior, we can check whether it is compatible with $\pi$ and $\mathcal{H}$ in time polynomial in $2^{n}$ and ${\left|V\right|}$ . Let $\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}$ be the set of extended behaviors w.r.t. the vertices of $\mathcal{H}$ that are compatible with $\varphi$ , $\pi$ and $\mathcal{H}$ . For each $\left\langle g,\mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}$ , recall that every entry of $\mathbf{f}$ is bounded by ${\left|K^{\varphi}\right|}$ . Thus the cardinality of $\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}$ is bounded by ${\left|V\right|}^{\left|\mathsf{TwoTps}\right|}\cdot{\left|K^{\varphi}\right|}% ^{\left|\mathsf{TwoTps}\times\mathsf{OneTps}\right|}$ which is doubly exponential in the length of $\varphi$ .

Computing a semilinear representation of the spectrum of a $\mathsf{C^{2}}$ sentence.

We are now ready to show that the $1$ -type spectrum of a $\mathsf{C^{2}}$ sentence $\varphi$ in normal form is semilinear. For every finite model $\mathcal{G}$ of $\varphi$ , by Lemma 27, for sufficiently large $\ell$ , for every $\ell$ -core $\mathcal{H}$ of $\mathcal{G}$ and pair of 1-types $\pi_{1}$ and $\pi_{2}$ in $\mathcal{G}\setminus\mathcal{H}$ , $\pi_{1}$ and $\pi_{2}$ are silent-compatible w.r.t. $\varphi$ . Furthermore by Lemma 32, $\mathcal{G}$ has an $\ell$ -core whose size is exponential in $\varphi$ and $\ell$ . We prove Theorem 37 via a two-step construction. First we show that for every such core $\mathcal{H}$ , there exists an existential Presburger formula $\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})$ such that the solution set of $\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})$ corresponds to the set of 1-type cardinality vectors of finite models of $\varphi$ with $\ell$ -core $\mathcal{H}$ .

$\blacksquare$

The variables are $x_{\pi}$ for $\pi\in\mathsf{OneTps}^{\varphi}$ , and $y_{\pi,\left\langle g,\mathbf{f}\right\rangle}$ for $\pi\in\mathsf{OneTps}^{\varphi}$ and $\left\langle g,\mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}$ . Intuitively, $\mathbf{x}$ is the 1-type spectrum of the finite model $\mathcal{G}$ and $y_{\pi,\left\langle g,\mathbf{f}\right\rangle}$ is the number of vertices in $\mathcal{G}\setminus\mathcal{H}$ with 1-type $\pi$ and extended behavior $\left\langle g,\mathbf{f}\right\rangle$ .
$\blacksquare$

The formula $\mathsf{SUM}_{\mathcal{H}}(\mathbf{x},\mathbf{y})$ asserts that the 1-type spectrum of $\mathcal{G}$ is the sum of the 1-type spectrum of $\mathcal{H}$ and the $1$ -type spectrum of $\mathcal{G}\setminus\mathcal{H}$ . Let $s_{\pi}$ be the number of vertices in $\mathcal{H}$ with 1-type $\pi$ .

$\displaystyle\mathsf{SUM}_{\mathcal{H}}(\mathbf{x},\mathbf{y}):=\bigwedge_{\pi% \in\mathsf{OneTps}^{\varphi}}\left(x_{\pi}=s_{\pi}+\sum_{\left\langle g,% \mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}}y_{\pi,\left% \langle g,\mathbf{f}\right\rangle}\right)$ .
$\blacksquare$

The formula $\mathsf{COMP}_{\mathcal{H}}(\mathbf{y})$ guarantees that the vertices in $\mathcal{H}$ satisfies the Counting condition of Proposition 28. Let $V_{c}$ be the vertices in $\mathcal{H}$ .

$\displaystyle\mathsf{COMP}_{\mathcal{H}}(\mathbf{y}):=\bigwedge_{v\in V_{c}}% \left(\sum_{u\in V_{c}\setminus\left\{v\right\}}\mathsf{TwoTp}^{\triangleright% }(v,u)+\sum_{\pi\in\mathsf{OneTps}^{\varphi}}\sum_{\left\langle g,\mathbf{f}% \right\rangle\in\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}}g^{\triangleleft}(v)% \cdot y_{\pi,\left\langle g,\mathbf{f}\right\rangle}=\mathbf{k}^{\varphi}\right)$ .
$\blacksquare$

The formula $\mathsf{SILENT}(\mathbf{y})$ assert that 1-types realized in $\mathcal{G}\setminus\mathcal{H}$ are silent compatible.

$\displaystyle\mathsf{SILENT}_{\mathcal{H}}(\mathbf{y}):=\bigwedge_{\begin{% subarray}{c}\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}\\ \text{are not silent compatible}\end{subarray}}\left(\sum_{\left\langle g,% \mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi_{1},\mathcal{H}}}y_{\pi_{% 1},\left\langle g,\mathbf{f}\right\rangle}=0\right)\lor\left(\sum_{\left% \langle g,\mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi_{2},\mathcal{H}% }}y_{\pi_{2},\left\langle g,\mathbf{f}\right\rangle}=0\right)$ .
$\blacksquare$

The formula $\mathsf{BIG}_{\mathcal{H}}(\mathbf{y})$ guarantees that 1-types and tuples realized in $\mathcal{G}\setminus\mathcal{H}$ satisfy the requirements of a core.

$\begin{aligned} \mathsf{BIG}_{\mathcal{H}}(\mathbf{y})\ :=\ &\bigwedge_{\pi\in% \mathsf{OneTps}^{\varphi}}\exists z\ \left(z=\sum_{\left\langle g,\mathbf{f}% \right\rangle\in\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}}y_{\pi,\left\langle g,% \mathbf{f}\right\rangle}\right)\land\left(z=0\lor z\geq{(2K^{\varphi}+1)}^{2}% \right)\land\\ &\bigwedge_{\begin{subarray}{c}\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}\\ \eta\in\mathsf{TwoTps}^{\varphi,\triangleright\triangleleft}_{\pi_{1},\pi_{2}}% \end{subarray}}\exists z\ \left(z=\sum_{\left\langle g,\mathbf{f}\right\rangle% \in\mathcal{B}^{\varphi}_{\pi_{1},\mathcal{H}}}\mathbf{f}(\eta,\pi_{2})\cdot y% _{\pi_{1},\left\langle g,\mathbf{f}\right\rangle}\right)\land\left(z=0\lor z% \geq(2K^{\varphi}+1)^{2}\right).\end{aligned}$
$\blacksquare$

The formula $\mathsf{MATCH}_{1,\mathcal{H}}(\mathbf{y})$ encodes the edge matching condition for audible 2-types and vertices in $\mathcal{G}\setminus\mathcal{H}$ .

$\displaystyle\mathsf{MATCH}_{1,\mathcal{H}}(\mathbf{y}):=\bigwedge_{\begin{% subarray}{c}\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}\\ \eta\in\mathsf{TwoTps}^{\varphi,\triangleright\triangleleft}_{\pi_{1},\pi_{2}}% \end{subarray}}\left(\sum_{\left\langle g,\mathbf{f}\right\rangle\in\mathcal{B% }^{\varphi}_{\pi_{1},\mathcal{H}}}\mathbf{f}(\eta,\pi_{2})\cdot y_{\pi_{1},% \left\langle g,\mathbf{f}\right\rangle}=\sum_{\left\langle g,\mathbf{f}\right% \rangle\in\mathcal{B}^{\varphi}_{\pi_{2},\mathcal{H}}}\mathbf{f}(\widetilde{% \eta},\pi_{1})\cdot y_{\pi_{2},\left\langle g,\mathbf{f}\right\rangle}\right)$ .
$\blacksquare$

The formula $\mathsf{MATCH}_{2,\mathcal{H}}(\mathbf{y})$ encodes the edge matching condition for backward-silent but not forward-silent 2-types and vertices in $\mathcal{G}\setminus\mathcal{H}$ .

$\displaystyle\mathsf{MATCH}_{2,\mathcal{H}}(\mathbf{y}):=\bigwedge_{\begin{% subarray}{c}\pi_{1},\pi_{2}\in\mathsf{OneTps}^{\varphi}\\ \eta\in\mathsf{TwoTps}^{\varphi,\triangleright}_{\pi_{1},\pi_{2}}\end{subarray% }}\left(\left(\sum_{\left\langle g,\mathbf{f}\right\rangle\in\mathcal{B}^{% \varphi}_{\pi_{1},\mathcal{H}}}\mathbf{f}(\eta,\pi_{2})\cdot y_{\pi_{1},\left% \langle g,\mathbf{f}\right\rangle}>0\right)\to\left(\sum_{\left\langle g,% \mathbf{f}\right\rangle\in\mathcal{B}^{\varphi}_{\pi_{2},\mathcal{H}}}y_{\pi_{% 2},\left\langle g,\mathbf{f}\right\rangle}>0\right)\right)$ .

Keep in mind that we will always be considering solutions in the natural numbers. So this implication could be rewritten without summation: if for one of the extended behaviors for this triple, $\mathbf{f}(\eta,\pi_{2})\cdot y_{\pi_{1},\left\langle g,\mathbf{f}\right% \rangle}>0$ , then one of the numbers $y_{\pi_{2},\left\langle g,\mathbf{f}\right\rangle}>0$ .

Finally, $\displaystyle\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x}):=\exists\mathbf{y}\ % \mathsf{SUM}_{\mathcal{H}}(\mathbf{x},\mathbf{y})\land\mathsf{COMP}_{\mathcal{% H}}(\mathbf{y})\land\mathsf{SILENT}_{\mathcal{H}}(\mathbf{y})\land\mathsf{BIG}% _{\mathcal{H}}(\mathbf{y})\land\bigwedge_{i=1,2}\mathsf{MATCH}_{i,\mathcal{H}}% (\mathbf{y})$ .

This system characterizes the spectrum:

Lemma 36.

For every $\mathsf{C^{2}}$ sentence $\varphi$ and partial model $\mathcal{H}$ of $\varphi$ , a vector $\mathbf{v}$ is a solution of $\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})$ if and only if there exists a finite model $\mathcal{G}$ of $\varphi$ such that the 1-type cardinality vector of $\mathcal{G}$ is $\mathbf{v}$ , and $\mathcal{H}$ is a $(2K^{\varphi}+1)^{2}$ -core of $\mathcal{G}$ .

It is easy to see that vectors in the spectrum satisfy the equations. In the other direction, we extend the core $\mathcal{H}$ to a finite model $\mathcal{G}$ of $\varphi$ . Solutions to the equations tell us how many vertices of each $1$ -type and extended behavior to create in $\mathcal{G}$ . We assign edge colors so that each vertex realizes its intended extended behavior. This is always possible because the solution is sufficiently large, as ensured by the Big condition in the equation. This extra size gives us some leeway to match up $1$ -types via $2$ -types. Details are in the appendix.

Let $\mathfrak{H}$ be the collection of partial models of $\varphi$ with size at most $2^{2n+4m+2}\cdot(2K^{\varphi}+1)^{2}$ . We define the existential Presburger formula $\Psi^{\varphi}(\mathbf{x}):=\bigvee_{\mathcal{H}\in\mathfrak{H}}\Psi^{\varphi}% _{\mathcal{H}}(\mathbf{y}).$

Lemma 37.

For every $\mathsf{C^{2}}$ sentence $\varphi$ , $\left\llbracket\Psi^{\varphi}(\mathbf{x})\right\rrbracket=\Pi\text{-}\mathsf{% SPEC}(\varphi)$ .

Proof.

Suppose that $\mathbf{v}\in\left\llbracket\Psi^{\varphi}(\mathbf{x})\right\rrbracket$ , there exists $\mathcal{H}$ such that $\mathbf{v}\in\left\llbracket\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})\right\rrbracket$ . By Lemma 36, there exists a model $\mathcal{G}$ of $\varphi$ such that the 1-type cardinality vector of $\mathcal{G}$ is $\mathbf{v}$ . Thus $\mathbf{v}\in\Pi\text{-}\mathsf{SPEC}(\varphi)$ . On the other hand, suppose that $\mathbf{v}\in\Pi\text{-}\mathsf{SPEC}(\varphi)$ . Then there is a model $\mathcal{G}$ of $\varphi$ with 1-type cardinality vector $\mathbf{v}$ . By Lemma 32, $\mathcal{G}$ has a $(2K^{\varphi}+1)^{2}$ -core $\mathcal{H}$ with size at most $2^{2n+4m+2}(2K^{\varphi}+1)^{2}$ , which implies that $\mathcal{H}\in\mathfrak{H}$ . By Lemma 36, $\mathbf{v}\in\left\llbracket\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})\right\rrbracket$ . Since $\mathcal{H}\in\mathfrak{H}$ , $\mathbf{v}\in\left\llbracket\Psi^{\varphi}(\mathbf{x})\right\rrbracket$ . $\hfill\blacktriangleleft$

Theorem 25 follows immediately from Lemma 37.

Note that the length of the formula $\Psi^{\varphi}(\mathbf{x})$ is doubly exponential in the length of $\varphi$ , since the length of $\Psi^{\varphi}_{\mathcal{H}}(\mathbf{x})$ is already doubly exponential in the length of $\varphi$ , as the number of variables $y_{\pi,\left\langle g,\mathbf{f}\right\rangle}$ is doubly exponential. Moreover, there are doubly exponentially many possible cores $\mathcal{H}$ .

Consequences for finite satisfiability of $\mathsf{C^{2}}$ with global constraints.

Note that in Lemma 37, we show that for every $\mathsf{C^{2}}$ sentence $\varphi$ in normal form, there exists an existential Presburger formula $\Psi^{\varphi}(\mathbf{x})$ of doubly exponential size such that $\Pi\text{-}\mathsf{SPEC}{\varphi}=\left\llbracket\Psi^{\varphi}(\mathbf{x})\right\rrbracket$ . Since for every 1-type $\pi$ and partial model $\mathcal{H}$ of $\varphi$ , we can compute $\mathcal{B}^{\varphi}_{\pi,\mathcal{H}}$ in doubly exponential time in the length of $\varphi$ and $\mathcal{H}$ by a straightforward enumerate-and-check procedure, $\Psi^{\varphi}(\mathbf{x})$ can be computed from $\varphi$ in doubly exponential time. Note that global constraints of $\mathsf{C^{2}}$ sentences are linear constraints over the $1$ -type cardinality vector. Therefore the finite satisfiability problem of $\mathsf{C^{2}}$ with global constraints reduces to satisfiability problem of $\Psi^{\varphi}(\mathbf{x})$ together with those linear constraints. This naive approach yields a $2\text{-}\mathsf{NEXP}$ algorithm.

We observe that $\Psi^{\varphi}(\mathbf{x})$ can be rewritten as disjunctions of doubly exponentially many integer linear systems. Each system contains doubly exponentially many variables, but only exponentially many constraints. By Lemma 1, if such a system has a solution, then there exists a solution in which only exponentially many variables are assigned non-zero values.

Therefore, we can decide the finite satisfiability of $\mathsf{C^{2}}$ with global constraints using the $\mathsf{NEXP}$ procedure in Algorithm 1.

Algorithm 1 Algorithm for the finite satisfiability problem of

\mathsf{C^{2}}

with global constraints.

We emphasize again that the argument here is completely generic, and the same comment holds to show that for any decidability extension of Presburger arithmetic (e.g. Büchi Arithemetic or Semenov Arithmetic [19]), $\mathsf{C^{2}}$ with global cardinality constraints of that form is decidable, with the complexity the maximum of $\mathsf{NEXP}$ and the complexity of solving the corresponding constraints.

6 Negative results about the spectrum of $\mathsf{GP^{2}}$ sentences

The $1$ -type spectrum of a $\mathsf{C^{2}}$ sentence is semilinear, and we showed how to calculate it in the previous section. For $\mathsf{GP^{2}}$ , earlier in the paper we were able to characterize models by a linear system: but the solutions to this linear system are not in one-to-one correspondence with the number of satisfiers of $1$ -types. Thus a natural question is whether the $1$ -type spectrum of a $\mathsf{GP^{2}}$ sentence is semilinear. We answer this below in the negative.

Consider the following $\mathsf{GP^{2}}$ formula $\varphi$ over vocabulary $\left\{P_{1},P_{2},E\right\}$ :

	$\displaystyle\varphi\ =$	$\displaystyle\forall x\ \left(\left(\neg P_{1}(x)\land P_{2}(x)\right)\lor% \left(P_{1}(x)\land\neg P_{2}(x)\right)\right)\ \ \land\ \ \bigwedge_{1\leq i% \leq 2}\forall x\ P_{i}(x)\to\gamma_{i}(x)$
	$\displaystyle\gamma_{1}(x)\ =$	$\displaystyle{\#_{y}\left[E(x,y)\land P_{1}(y)\right]}-{\#_{y}\left[E(x,y)% \land P_{2}(y)\right]}=0$
	$\displaystyle\gamma_{2}(x)\ =$	$\displaystyle{\#_{y}\left[E(y,x)\land P_{1}(y)\right]}=1.$

Let $\mathcal{G}$ be a finite model of $\varphi$ . A vertex in $\mathcal{G}$ is labeled with either $P_{1}$ or $P_{2}$ . Let $V_{i}$ be the set of vertices in $\mathcal{G}$ with label $P_{i}$ . For every $v\in V_{1}$ , the number of edges from $v$ to $V_{1}$ is the same as the number of edges from $v$ to $V_{2}$ . For every vertex $v\in V_{2}$ , there exists exactly one edge from $V_{1}$ to $v$ . Therefore the cardinality of $V_{2}$ is the same as the number of edges between vertices of $V_{1}$ , which is bounded by ${\left|V_{1}\right|}\cdot({\left|V_{1}\right|}-1)$ . Thus the 1-type spectrum of $\varphi$ is $\left\{(0,a,b,0)\in\mathbb{N}^{4}\middle|\ b\leq a(a-1)\right\}$ . Hence we have the following negative result.

Theorem 38.

The 1-type spectrum of a $\mathsf{GP^{2}}$ sentence is not always semilinear.

This does not resolve whether the set of cardinalities of finite models is a semilinear set, and it leaves open whether $\mathsf{GP^{2}}$ with global cardinality constraints is decidable.

7 Related work

The logic $\mathsf{GP^{2}}$ was shown decidable in [4, 12], while the decidability of $\mathsf{C^{2}}$ with cardinality constraints is implicit in [11, 5]. Our complexity bound for $\mathsf{GP^{2}}$ refines the analysis of the Kleene star operator in [6], which in turn relies on [8]. Our analysis of $\mathsf{C^{2}}$ with constraints obviously relies heavily on the techniques developed by Pratt-Hartmann for analysis of $\mathsf{C^{2}}$ , in particular normal forms, the categorization of types, and the distinction between large and small number of realizers (e.g. the notion of Z-differentiated [15, 16]).

Although we borrow techniques from prior work, our approach gives a self-contained proof of decidability for $\mathsf{C^{2}}$ itself, and also for $\mathsf{C^{2}}$ with global constraints in extensions of Presburger arithmetic. An alternative approach to get bounds for $\mathsf{C^{2}}$ with Presburger global constraints is by reducing to decidability of $\mathsf{C^{2}}$ . This approach was presented by Rudolph in [18], relying on ideas from [1]. Although technically speaking the results in [18] are presented for description logics, they could easily be applied to give the same bounds for $\mathsf{C^{2}}$ .

In addition to contributing tight bounds for complexity for decidability of $\mathsf{GP^{2}}$ a well as the size of the spectrum for $\mathsf{C^{2}}$ , we note that [6] is phrased in terms of graph neural networks, while from the analysis of spectra in [11, 5] it would be difficult to see how semilinear representations are derived. Thus we believe our work additionally makes the analyses of logics with arithmetic substantially more accessible.

8 Conclusion

In the paper we isolate the complexity of satisfiability for two logics combining relational structure and arithmetic, $\mathsf{GP^{2}}$ and the logics $\mathsf{C^{2}}$ and $\mathsf{GC^{2}}$ extended with cardinality constraints. In the process we refine and simplify proof techniques for analyzing such logics. $\mathsf{GP^{2}}$ and $\mathsf{C^{2}}$ are incomparable in expressiveness. The former allows inductively forming open formulas that involve arithmetic between counts of neighbors, while in the latter arithmetic can only be used at top-level for forming sentences. On the other hand, $\mathsf{C^{2}}$ allows unguarded formulas. See the appendix for a formal argument. We leave open the question of the decidability of combinations of formulas in the two languages.

References

[1] Franz Baader. Expressive cardinality restrictions on concepts in a description logic with expressive number restrictions. SIGAPP Appl. Comput. Rev., 19(3), 2019.
[2] Bartosz Bednarczyk. One-variable logic meets presburger arithmetic. Theoretical Computer Science, 802:141–146, 2020. doi:10.1016/J.TCS.2019.09.028.
[3] Bartosz Bednarczyk and Oskar Fiuk. Presburger büchi tree automata with applications to logics with expressive counting. In Logic, Language, Information, and Computation, pages 295–308, Cham, 2022. Springer International Publishing. doi:10.1007/978-3-031-15298-6_19.
[4] Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. On classical decidable logics extended with percentage quantifiers and arithmetics. In FSTTCS, 2021.
[5] Michael Benedikt, Egor Kostylev, and Tony Tan. Two Variable Logic with Ultimately Periodic Counting. SIAM Journal on Computing, 53(4):884–968, 2024. doi:10.1137/22M1504792.
[6] Michael Benedikt, Chia-Hsuan Liu, Boris Motik, and Tony Tan. Verification of graph neural networks via logical characterizations. In ICALP, 2024.
[7] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564–568, 2006. doi:10.1016/J.ORL.2005.09.008.
[8] Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In LICS, 2019.
[9] Narendra Karmarkar. A new polynomial-time algorithm for linear programming. In STOC, 1984.
[10] Yevgeny Kazakov. A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment. In JELIA, 2004.
[11] Eryk Kopczynski and Tony Tan. Regular graphs and the spectra of two-variable logic with counting. SIAM J. Comput., 44(3):786–818, 2015. doi:10.1137/130943625.
[12] Chia-Hsuan Lu and Tony Tan. On two-variable guarded fragment logic with expressive local Presburger constraints. Logical Methods in Computer Science, 20, 2024. doi:10.46298/LMCS-20(3:16)2024.
[13] Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, 1981. doi:10.1145/322276.322287.
[14] Rohit Parikh. On Context-Free Languages. JACM, 13(4):570–581, 1966. doi:10.1145/321356.321364.
[15] Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic Language and Information, 14:369–395, 2005. doi:10.1007/S10849-005-5791-1.
[16] Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. Journal of Logic and Computation, 17(1):133–155, 2007. doi:10.1093/LOGCOM/EXL034.
[17] Ian Pratt-Hartmann. The two-variable fragment with counting. In WoLLIC, 2010.
[18] "Johann" Sebastian Rudolph. Presburger concept cardinality constraints in very expressive description logics - allegro sexagenarioso ma non ritardando. In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019. doi:10.1007/978-3-030-22102-7_25.
[19] Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587–618, 1984.
[20] Boris Trakhtenbrot. The Impossibility of an Algorithm for the Decidability Problem on Finite Classes. Proceedings of the USSR Academy of Sciences, 70(4):569–572, 1950.

[bib.bib1] [1] Franz Baader. Expressive cardinality restrictions on concepts in a description logic with expressive number restrictions. SIGAPP Appl. Comput. Rev., 19(3), 2019.

[bib.bib2] [2] Bartosz Bednarczyk. One-variable logic meets presburger arithmetic. Theoretical Computer Science, 802:141–146, 2020. doi:10.1016/J.TCS.2019.09.028.

[bib.bib3] [3] Bartosz Bednarczyk and Oskar Fiuk. Presburger büchi tree automata with applications to logics with expressive counting. In Logic, Language, Information, and Computation, pages 295–308, Cham, 2022. Springer International Publishing. doi:10.1007/978-3-031-15298-6_19.

[bib.bib4] [4] Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. On classical decidable logics extended with percentage quantifiers and arithmetics. In FSTTCS, 2021.

[bib.bib5] [5] Michael Benedikt, Egor Kostylev, and Tony Tan. Two Variable Logic with Ultimately Periodic Counting. SIAM Journal on Computing, 53(4):884–968, 2024. doi:10.1137/22M1504792.

[bib.bib6] [6] Michael Benedikt, Chia-Hsuan Liu, Boris Motik, and Tony Tan. Verification of graph neural networks via logical characterizations. In ICALP, 2024.

[bib.bib7] [7] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564–568, 2006. doi:10.1016/J.ORL.2005.09.008.

[bib.bib8] [8] Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In LICS, 2019.

[bib.bib9] [9] Narendra Karmarkar. A new polynomial-time algorithm for linear programming. In STOC, 1984.

[bib.bib10] [10] Yevgeny Kazakov. A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment. In JELIA, 2004.

[bib.bib11] [11] Eryk Kopczynski and Tony Tan. Regular graphs and the spectra of two-variable logic with counting. SIAM J. Comput., 44(3):786–818, 2015. doi:10.1137/130943625.

[bib.bib12] [12] Chia-Hsuan Lu and Tony Tan. On two-variable guarded fragment logic with expressive local Presburger constraints. Logical Methods in Computer Science, 20, 2024. doi:10.46298/LMCS-20(3:16)2024.

[bib.bib13] [13] Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, 1981. doi:10.1145/322276.322287.

[bib.bib14] [14] Rohit Parikh. On Context-Free Languages. JACM, 13(4):570–581, 1966. doi:10.1145/321356.321364.

[bib.bib15] [15] Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic Language and Information, 14:369–395, 2005. doi:10.1007/S10849-005-5791-1.

[bib.bib16] [16] Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. Journal of Logic and Computation, 17(1):133–155, 2007. doi:10.1093/LOGCOM/EXL034.

[bib.bib17] [17] Ian Pratt-Hartmann. The two-variable fragment with counting. In WoLLIC, 2010.

[bib.bib18] [18] "Johann" Sebastian Rudolph. Presburger concept cardinality constraints in very expressive description logics - allegro sexagenarioso ma non ritardando. In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019. doi:10.1007/978-3-030-22102-7_25.

[bib.bib19] [19] Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587–618, 1984.

[bib.bib20] [20] Boris Trakhtenbrot. The Impossibility of an Algorithm for the Decidability Problem on Finite Classes. Proceedings of the USSR Academy of Sciences, 70(4):569–572, 1950.

Analysis of Logics with Arithmetic

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

Basic notions.

Linear algebra and Kleene star.

Lemma 1 ([13], [7], also see Corollary 2.2 in [12]).

Definition 2 (Kleene star).

Lemma 3.

Types.

Definition 4 (1- and 2-type).

Definition 5 (Silent 2-type).

Definition 6 (Dual of 2-type).

Definition 7 (Type graph).

Definition 8 (1-type cardinality vector of a σ-structure).

3 Logics and prior complexity bounds concerning them

4 Finite satisfiability of 𝗚𝗣𝟮 is in EXP

Theorem 9.

𝗚𝗣𝟮 infrastructure.

Definition 10 (Compatibility of 1- and 2-types).

Definition 11 (Behavior vector of a vertex).

Definition 12 (Characteristic system).

Definition 13 (Compatibility of behavior vector).

Proposition 14.

Lemma 15.

Proof.

The main construction.

Lemma 16.

Proof.

Suppose that 𝝋 is finitely satisfiable with finite model 𝓖.

Suppose that there exists such 𝐠𝝅∈𝗞𝗹𝗲𝗲𝗻𝗲𝗦𝘁𝗮𝗿⁢(𝓑𝝅𝝋) for 𝝅∈𝗢𝗻𝗲𝗧𝗽𝘀𝝋

Definition 17.

Lemma 18.

Proof.

Suppose that 𝝋 is finitely satisfiable.

Suppose that 𝓠𝝋⁢(𝐱) has a solution, assigning 𝒙𝝅𝟏,𝜼,𝝅𝟐 to 𝒂𝝅𝟏,𝜼,𝝅𝟐.

Definition 19.

Lemma 20.

Proof.

Suppose that 𝓠𝝋⁢(𝐱) has a solution in ℕ.

Suppose that 𝓠𝑴′⁣𝝋⁢(𝐱) has a solution 𝐚𝝅 in ℕ.

Proof.

5 Spectra of 𝗖𝟮 formulas

Definition 21 (Count bound vector).

Definition 22 (Forward and backward characteristic vector of 2-types).

Definition 23 (Forward and backward silent 2-type).

Definition 24 (Spectrum and 1-type spectrum).

Theorem 25.

Definition 26 (Silent compatible 1-types).

Lemma 27.

Proof.

Suppose that 𝝅𝟏=𝝅𝟐.

Suppose that 𝝅𝟏≠𝝅𝟐.

Proposition 28.

Definition 29 (Partial model of 𝖢𝟤 sentence).

Lemma 30.

Core of structures.

Definition 31.

Lemma 32.

Lemma 33.

Proof.

Definition 34 (Extended behavior).

Definition 35 (Compatibility of extended behaviors).

Computing a semilinear representation of the spectrum of a 𝗖𝟮 sentence.

Lemma 36.

Lemma 37.

Proof.

Consequences for finite satisfiability of 𝗖𝟮 with global constraints.

6 Negative results about the spectrum of 𝗚𝗣𝟮 sentences

Theorem 38.

7 Related work

8 Conclusion

Definition 8 ( $1$ -type cardinality vector of a $\sigma$ -structure).

4 Finite satisfiability of $\mathsf{GP^{2}}$ is in EXP

$\mathsf{GP^{2}}$ infrastructure.

Suppose that $\varphi$ is finitely satisfiable with finite model $\mathcal{G}$ .

Suppose that there exists such $\mathbf{g}_{\pi}\in\mathsf{KleeneStar}\left(\mathcal{B}^{\varphi}_{\pi}\right)$ for $\pi\in\mathsf{OneTps}^{\varphi}$

Suppose that $\varphi$ is finitely satisfiable.

Suppose that $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution, assigning $x_{\pi_{1},\eta,\pi_{2}}$ to $a_{\pi_{1},\eta,\pi_{2}}$ .

Suppose that $\mathcal{Q}^{\varphi}(\mathbf{x})$ has a solution in $\mathbb{N}$ .

Suppose that $\mathcal{Q}_{M}^{\prime\varphi}(\mathbf{x})$ has a solution $\mathbf{a}_{\pi}$ in $\mathbb{N}$ .

5 Spectra of $\mathsf{C^{2}}$ formulas

Definition 24 (Spectrum and $1$ -type spectrum).

Suppose that $\pi_{1}=\pi_{2}$ .

Suppose that $\pi_{1}\neq\pi_{2}$ .

Definition 29 (Partial model of $\mathsf{C^{2}}$ sentence).

Computing a semilinear representation of the spectrum of a $\mathsf{C^{2}}$ sentence.

Consequences for finite satisfiability of $\mathsf{C^{2}}$ with global constraints.

6 Negative results about the spectrum of $\mathsf{GP^{2}}$ sentences