# Designs in compact symmetric spaces and applications of great antipodal sets

Bang-Yen Chen  Department of Mathematics, Michigan State University, East
Lansing, MI 48824, USA<EMAIL_ADDRESS>
###### Abstract.

The theory of designs is an important branch of combinatorial mathematics. It
is well-known in the theory of designs that a finite subset of a sphere is a
tight spherical 1-design if and only if it is a pair of antipodal points. On
the other hand, antipodal sets and 2-number for a Riemannian manifold are
introduced by B.-Y. Chen and T. Nagano [21] in 1982. An antipodal set is
called a great antipodal set if its cardinality is equal to the 2-number. The
main purpose of this paper is to provide a survey on important results in
compact symmetric spaces with great antipodal sets as the designs. In the last
two sections of this paper, we present some important applications of 2-number
and great antipodal sets to topology and group theory.
Mathematics Subject Classification (2020): Primary 05B30; Secondary 05-02,
65D32.
Key words: Spherical design, $t$-design, great antipodal set, cubature
formula, Delsarte theory.

##  1\. Introduction

The theory of designs is an important branch of combinatorial mathematics that
deals with the existence, construction and properties of systems of finite
sets whose arrangements satisfy generalized concepts of balance and/or
symmetry.

The concept of $t$-designs of points on an $n$-sphere
$S^{n}\subset\mathbb{R}^{n+1}$ was initiated by P. Delsarte, J. M. Goethals
and J. J. Seidel as an analogy with combinatorial $r$-designs [26]. These
spherical $t$-designs have interesting properties which are related to several
important areas of mathematics [29]. These ideas were later extended to the
notion of $r$-designs in Delsarte spaces by A. Neumaier in [47]. The notion of
spherical $t$-designs was also extended as spherical designs of harmonic index
$t$. E. Bannai, T. Okuda and M. Tagami [10] studied lower bounds and “tight”
examples of spherical designs of harmonic index $t$. A theory of designs in
compact symmetric spaces of rank one was given by S. G. Hoggar in [32].
Moreover, the classification of tight designs were developed by E. Bannai and
S. G. Hoggar [8, 9], Y. I. Lyubich [42] and S. G. Hoggar [32, 33], among
others.

On the other hand, it is not an easy task to study similar theories in compact
symmetric spaces of higher rank. Nevertheless, there are several studies in
theory of designs in Grassmannian manifolds (see, e.g., [5, 4, 38, 49]).
Furthermore, some studies of design theories on unitary groups and complex
spheres can be found in [45, 50, 51], among others.

The concept of the antipodal points in spheres was generalized and developed
to antipodal sets in compact symmetric spaces by B.-Y. Chen and T. Nagano in
[21, 22]. Note that every antipodal set for any compact symmetric space is a
finite set and the maximum cardinality is called the 2-number. An antipodal
set on a compact symmetric space $M$ is called a great antipodal set whenever
its cardinality is equal to the 2-number of $M$.

The main purpose of this paper is to provide a survey on important results in
compact symmetric spaces with great antipodal sets as designs. Furthermore, in
the last two sections of this paper, we present some applications of 2-number
and great antipodal sets to topology and group theory. This paper can be
regarded as a natural continuation of my earlier articles [16, 17, 18].

##  2\. Spherical designs

The spherical codes and designs on an $n$-sphere $S^{n}$ are finite subsets.
In 1973, P. Delsarte [24] unified the theories of codes and designs on
association schemes, and gave the upper bounds for codes and the lower bound
for designs by applying linear programming for polynomials associated with
metric or cometric association schemes. From code theoretical viewpoint, a
spherical code is to find a finite set $X\subset S^{n}$ such that points on
$X$ are scattered on $S^{n}$ as far as possible. On the other hand, from
design theoretical viewpoint, it is to try to find $X$ which globally
approximates the sphere $S^{n}$ very well.

Of course, “What does approximate the sphere $S^{n}$ well mean?” is an
interesting question. For this question, there exists one very reasonable
answer given in 1977 by P. Delsarte, J. M. Goethals and J. J. Seidel defined
as follows.

######  Definition 2.1.

[26] For a natural number $t$, a finite subset $X\subset S^{n}$ is called a
spherical $t$-design if we have

$\frac{1}{|S^{n}|}\int_{\bf x\in S^{n}}f({\bf x})d\sigma({\bf
x})=\frac{1}{|X|}\sum_{u\in X}f(u)$

for any polynomial $f({\bf x})=f(x_{1},\ldots,x_{n+1})$ of degree at most $t$,
with the usual integral on the unit sphere, where $\sigma$ is the normalized
Haar measure and $|X|$ denotes the cardinality of $X$.

This notion of spherical $t$-designs is an analogue of the classical concept
of combinatorial $t$-designs studied in the traditional theory of designs in
combinatorics which has caught the hearts of many combinatorialists. This
research subject has been investigated on its own but also in connection with
several other theories such as lattices, association schemes and number theory
as well as cubature formulas. Further, sphere packing problems are found to be
related with quantum error correcting codes in the mid of 1990s (see [12, 23,
52]). Moreover, there is a very nice analogy between the theories of codes and
designs in the frame work of association schemes formulated in 1973 by P.
Delsarte [24] and the theory of spherical codes and designs formulated in 1977
by Delsarte, J. M. Goethals and J. J. Seidel [26], which are known today as
Delsarte’s theory on association schemes and Delsarte theory on spheres, or
slightly more broadly, algebraic combinatorics on association schemes or
algebraic combinatorics on spheres (see [7] for details). The essential tool
in their works is the addition formula for polynomials; polynomials associated
with metric or cometric association schemes, or the Gegenbauer polynomials
associated with spheres. In general, the theory of designs can be given on the
Delsarte spaces.

It is well-known that the images of spherical $t$-designs under an orthogonal
transformation are also spherical $t$-designs. Furthermore, it is also well-
known that for any given fixed $n$ and $t$, there always exists a spherical
$t$-design $X\subset S^{n}$ whenever the cardinality $|X|$ of $X$ is
sufficiently large.

The spherical $t$-designs have been extended in 1980 by A. Neumaier [47] to
the concept of $r$-designs in Delsarte spaces, which was so named by an
analogy with the $Q$-polynomial association schemes of Delsarte (see, e.g.,
[24, 47]). The concept of spherical $t$-designs is also generalized as
spherical designs of harmonic index $t$. A finite subset $Y$ on $n$-sphere
$S^{n}$ is called a spherical design of harmonic index $t$ if it satisfied
$\sum_{{\bf x}\in Y}f({\bf x})=0$ for any $f\in{\rm Harm}_{t}(S^{n})$ (see [7]
for more detail). For instance, E. Bannai, T. Okuda and M. Tagami investigated
in [10] lower bounds and studied examples of tight spherical designs of
harmonic index $t$. For the study of bounds on antipodal spherical designs
with few angles, we refer to [58].

A tight design is a design whose cardinality is equal to the known natural
lower bound. Any pair of antipodal points in a sphere is known to be a tight
1-design. Recently, the classification of tight spherical $t$-designs have
been a very attractive research subject.

##  3\. Design theory in compact symmetric spaces

In this section, we discuss some generalizations of spherical designs and
codes to compact symmetric spaces such as real and complex projective spaces
and Grassmannian manifolds (cf. [7, 30] for more details).

(1) Real and complex projective spaces. There are several attempts to
generalize the theory of spherical codes and designs to other spaces. Before
Delsarte, Goethals and Seidel studied spherical designs and codes in [26],
they also considered systems of lines in $\mathbb{R}^{n}$ and $\mathbb{C}^{n}$
(see [25]). This study is essentially equivalent to considering points in real
and complex projective spaces in which Jacobi polynomials appeared instead of
the Gegenbauer polynomials. Their attempts tried to find a common framework to
study finite subsets in these projective spaces and subsets in certain
association schemes. They also introduced several notions, such as Delsarte
spaces (see [46, 47, 28]) and polynomial spaces (see [39, 40, 41]). The
similarities of the theories between these continuous spaces and association
schemes provided evidence from of Delsarte’s 1973 works [24] and the 1977
works of Delsarte, Goethals and Seidel given in [26]. The most natural set up
for the continuous spaces are compact symmetric spaces of rank one. This
theory was first developed in that framework by S. G. Hoggar [32] in 1982.
Furthermore, in the theory of codes and designs, the concept of tight
$t$-designs and the classification problems of tight $t$-designs were
developed in a series of papers by E. Bannai and S. G. Hoggar in [8, 7, 33,
34, 35].

(2) Grassmannian manifolds. The Grassmannian manifolds are natural
generalization of projective spaces in which one-dimensional subspaces are
considered. As a well-known fact, we may regarded Grassmannian manifolds
$G^{\mathbb{F}}(n,k)$ as the set of $k$-dimensional subspaces of an
$n$-dimensional vector space $V$ over the field
$\mathbb{F}=\mathbb{R},\mathbb{C}$ or $\mathbb{H}$. Obviously, Grassmannian
manifolds are compact symmetric spaces of higher ranks if $k>1$.

The concept of $t$-designs in Grassmannian manifolds was first introduced in
2002 by C. Bachoc, R. Coulangeon and G. Nebe in [5]. Basic properties
$t$-designs in Grassmannian manifolds were also studied in [5]. Some types of
Delsarte theory as well as the formulation of tight $t$-designs was further
investigated in 2004 by C. Bachoc, E. Bannai and R. Coulangeon [4]. On the
other hand, the classification problems of tight $t$-designs remain open til
now. For further works on algebraic combinatorics of Grassmannian manifolds,
we refer to [2, 3, 6], among others.

##  4\. Spherical 1-designs, great antipodal sets and 2-number

The following results are well-known in spherical design theory. Let $Y$ be a
finite subset of an $n$-sphere $S^{n}$. Then we have:

  * (1)

If $Y$ is a spherical 1-design (or equivalently, a spherical design of
harmonic index 1), then the cardinality of $Y$ satisfies $|Y|\geq 2$.

  * (2)

$Y$ is a spherical 1-design with $|Y|=2$ if and only if $Y$ is a pair of
antipodal points.

  * (3)

Let $T$ be a set of integers $t$ such that a pair of antipodal points on
$S^{n}$ is a spherical design of harmonic index $t$. Then $T$ consists of all
odd natural numbers.

Recall the following definition from [21, 22].

######  Definition 4.1.

An antipodal set $A(M)$ of a Riemannian manifold $M$ is a discrete subset of
$M$ such that any two points in $A(M)$ are antipodal on some closed geodesic
of $M$. A maximal antipodal set of $M$ is an antipodal set which is not a
proper subset of any other antipodal set.

Note that the cardinalities of antipodal sets are bounded for each compact
Riemannian manifold (for a clear proof, see [56]). The notions of maximal
antipodal sets allow us to define “2-number”, denoted by $\\#_{2}M$, which is
the largest cardinal number among all maximal antipodal sets. A maximal
antipodal set $A(M)$ is called a great antipodal set if $A(M)$ satisfies
$\\#(A(M))=\\#_{2}M,$ where $\\#(A(M))$ denotes the cardinal number of $A(M)$.

For 2-number of Riemannian manifolds, we have [22]

(a) $\\#_{2}M\geq 2$ for every compact Riemannian manifold $M$;

(b) $\\#_{2}S^{n}=2$ and $\\#_{2}RP^{n}=n+1$.

######  Remark 4.1.

Statement (a) follows from the fact that every compact Riemannian manifold
admits a closed geodesic (see [43]).

The notion of symmetric $R$-spaces were defined in 1965 independently by
Nagano [44] and Takeuchi [53] as $R$-spaces which are at the same time compact
symmetric spaces. Hence, a symmetric $R$-spaces admits a transitive action of
a center-free non-compact semi-simple Lie group and the corresponding
stabilizer of a point is a certain maximal parabolic subgroup. But the name
“symmetric R-space” was coined by M. Takeuchi in [53].

The family of symmetric $R$-spaces have been completely classified by S.
Kobayashi and T. Nagano in [36] which consists of (up to minor modifications)

  * (a)

All Hermitian symmetric spaces of compact type.

  * (b)

Grassmann manifolds $O(p+q)/O(p)\times O(q),Sp(p+q)/Sp(p)\times Sp(q)$.

  * (c)

The classical groups $SO(m),\,U(m),\,Sp(m)$.

  * (d)

$U(2m)/Sp(m),\,U(m)/O(m)$.

  * (e)

$(SO(p+1)\times SO(q+1))/S(O(p)\times O(q))$, where $S(O(p)\times O(q))$ is
the subgroup of $SO(p+1)\times SO(q+1)$ consisting of matrices of the form:

$\begin{pmatrix}\epsilon&0&&\\\ 0&A&&\\\ &&\epsilon&0\\\
&&0&B\end{pmatrix},\quad\epsilon=\pm 1,\quad A\in O(p),\quad B\in O(q),$

(This symmetric $R$-space is covered twice by $S^{p}\times S^{q}$).

  * (f)

The Cayley projective plane $FII={\mathcal{O}}P^{2}$.

  * (g)

The three exceptional spaces $E_{6}/Spin(10)\times S^{1},E_{7}/E_{6}\times
S^{1},$ and $E_{6}/F_{4}.$

Great antipodal sets and the 2-number on symmetric $R$-spaces have several
nice properties; for examples, we have:

  * (i)

Great antipodal sets on a symmetric $R$-space are unique up to congruence (see
[55, 56]).

  * (ii)

Great antipodal sets on a symmetric $R$-space are certain orbits of Weyl
groups (see [54]).

##  5\. Unitary groups with great antipodal sets as designs

The compact simple Lie group $U(n)$ is a compact symmetric space (with respect
to a bi-invariant metric) and it has the point-symmetry at each given point in
$U(n)$. A great antipodal set on $U(n)$ is an analogue of a pair of antipodal
points on spheres which is a tight spherical 1-design.

Let $G$ be a compact group together with a closed subgroup $K$. Put $M=G/K$
and let $\mu$ be a positive finite $G$-invariant measure on $M$. Suppose
$\rho$ is the natural unitary representation of $G$ on the Hilbert space
$L^{2}(M,\mu)$. Choose a $\rho(G)$-invariant irreducible closed subspace
$\mathcal{H}$ of $L^{2}(M,\mu)$. Denote by ${\mathcal{C}}(U(n))$ the space of
$\mathbb{C}$-valued continuous functions on $U(n)$. Then ${\mathcal{C}}(U(n))$
is a $G$-space as

$G\times{\mathcal{C}}(U(n))\to{\mathcal{C}}(U(n));\;\;(x_{1},x_{2})\cdot
f(x)=f(x_{1}^{-1}xx_{2}).$

Let ${\mathcal{H}}_{\lambda}$ be a $G$-subspace of ${\mathcal{C}}(U(n))$ which
is isomorphic to $\rho_{\lambda}\boxtimes\rho_{\lambda}^{*}$. Then it is known
that the structure of ${\mathcal{H}}_{\lambda}$ in ${\mathcal{C}}(U(n))$
exists uniquely, i.e., if $W\subset{\mathcal{C}}(U(n))$ is a subrepresentation
which is isomorphic to $\rho_{\lambda}\boxtimes\rho_{\lambda}^{*}$, then we
have $W={\mathcal{H}}_{\lambda}$ (see [37] for more details).

In 2001, H. Kurihara [37] investigated the relationship between great
antipodal sets on $U(n)$ and design theory on $U(n)$. He established a nice
link between great antipodal sets on $U(n)$ and designs. He also obtained a
nice link between great antipodal sets on $U(n)$ and the Hamming cube graph
${\mathcal{Q}}_{n}$.

######  Definition 5.1.

Fix a subset ${\mathcal{T}}\subset(\mathbb{Z}^{n})_{+}$ and let $Y$ be a
finite subset of $U(n)$. Then $Y$ is called a ${\mathcal{T}}$-design if the
following formula:

$\int_{U(n)}f({\bf x})d\sigma({\bf x})=\frac{1}{|Y|}\sum_{x\in Y}f(\bf x)$

is satisfied for every
$f\in\oplus_{\lambda\in{\mathcal{T}}}{\mathcal{H}}_{\lambda}$. When the subset
${\mathcal{T}}$ is a singleton $\lambda$, then $Y$ is called a
$\lambda$-design.

For $\lambda=(\lambda_{1},\ldots,\lambda_{n})\in(\mathbb{Z}^{n})_{+}$, let us
put ${\rm diff}(\lambda):=\lambda_{1}-\lambda_{n}$. Note that ${\rm
diff}(\lambda)$ is invariant for the equivalence relation $\sim$. Thus we may
define ${\rm diff}([\lambda])$.

H. Kurihara [37] proved the following result for a great antipodal set $S$ on
$U(n)$.

######  Theorem 5.1.

For a great antipodal set $S$ on $U(n)$,

  * (1)

If $[\lambda]$ is odd, then S is a $[\lambda]$-design.

  * (2)

If $[\lambda]$ is even and S is a $[\lambda]$-design, then ${\rm
diff}([\lambda])<n-1$. In particular, there exist only finitely many even
$[\lambda]$ such that $S$ is a $[\lambda]$-design.

######  Remark 5.1.

Theorem 5.1 shows that great antipodal sets are “good” designs on $U(n)$.

H. Kurihara also provided the following examples in [37].

######  Example 5.1.

For small $n$, the condition on $[\lambda]$ carries that a great antipodal set
$S$ is a $[\lambda]$-design.

  * (1)

When $n=2$, $S$ on $U(2)$ is an even $[\lambda]$-design if and only if
$[\lambda]=[(1,1)]$.

  * (2)

When $n=3$, $S$ on $U(3)$ is an even $[\lambda]$-design if and only if
$[\lambda]=[(1,1,0)]$ or $[\lambda]=[(2,1,1)]$.

  * (3)

$S$ on $U(4)$ is an even $[\lambda]$-design if and only if the following six
classes: $[\lambda]=$
$[(1,1,0,0)],[(2,1,1,0)],[(1,1,1,1)],[(3,1,1,1)],[(2,2,1,1)],[(3,3,3,1)]$.

  * (4)

$S$ on $U(5)$ is an even $[\lambda]$-design if and only if the following 12
classes: $[\lambda]=$
$[(1,1,0,0,0)],[(2,1,1,0,0)],[(1,1,1,1,0)],[(3,1,1,1,0)],[(2,2,1,1,0)]$,
$[(3,3,3,3,0)],[(2,1,1,1,1)],\,[(4,1,1,1,1)],(3,2,1,1,1)],[(2,2,2,1,1)],$
$[(3,3,3,2,1)],\;[(4,3,3,3,1)]$.

Let $[n]$ denote the set $\\{1,2,...,n\\}$ and $Q$ be the $n$-ary Cartesian
product of the two elements set $\\{1,-1\\}$. The Hamming cube graph
$\mathcal{Q}_{n}$ of degree $n$ is the graph with the vertex set $Q$ and two
vertices are adjacent if they differ in precisely one coordinate.

Let $g$ be a bi-invariant metric on $U(n)$ and let

${\rm dist}_{g}:U(n)\times U(n)\to\mathbb{R}$

be the distance function on $U(n)$ via $g.$ For a great antipodal set $S$ of
$U(n)$, we define the minimum distance of $S$ with respect to $g$ by

${\rm md}_{g}(S):=\min\\{{\rm dist}_{g}(x,y):x,y\in S,x\neq y\\}.$

Now, consider the graph defined as follows: The vertices set is $S$ and two
vertices $x$ and $y$ in $S$ are adjacent if we have ${\rm dist}_{g}(x,y)={\rm
md}_{g}(S)$. Let $E_{g}$ denotes the edge set of this graph.

In [37], H. Kurihara also proved the following link between great antipodal
sets on $U(n)$ and the Hamming cube graph ${\mathcal{Q}}_{n}$.

######  Theorem 5.2.

For any bi-invariant metric $g$ on $U(n)$, the graph $(S,E_{g})$ is a Hamming
cube $\mathcal{Q}_{n}$.

######  Remark 5.2.

For further results in this direction, see H. Kurihara [37]. For tight
4-designs in Hamming association schemes, we refer to A. Gavrilyuk, S. Suda
and J. Vidali [27].

##  6\. Grassmannian manifolds with great antipodal sets as designs

In this section we present some results on characterizations of great
antipodal sets as design in complex Grassmannian manifolds among certain
designs with the smallest cardinalities. Note that great antipodal sets are in
differential geometry. On the other hand, the theory of designs is related to
algebraic combinatorics or representation theory.

For a 1-design $X$ on a complex projective $n$-space ${\mathbb{C}}P^{n}$, we
have the following inequality:

$|X|\geq n+1,$

and $X$ is tight if $|X|=n+1$ (see [32]).

It is also known that for a complex projective space, great antipodal sets can
be characterized by tight 1-designs. Therefore, we have the following result
[38, Fact 3.1, page 440].

######  Theorem 6.1.

Let $S$ be a finite subset of a complex projective space. Then the following
two statements are equivalent:

  * (a)

$S$ is a great antipodal set.

  * (b)

$S$ is a tight 1-design.

In order to state the main results of this section, we put

(6.1)
$\displaystyle{\mathcal{E}}=\\{(\overbrace{1,\ldots,1}^{i},\overbrace{0,\ldots,0}^{m-i}:i=0,1,\ldots,m\\},$
(6.2)
$\displaystyle{\mathcal{F}}=\\{((2,\overbrace{1,\ldots,1}^{i-1},\overbrace{0,\ldots,0}^{m-i}):i=0,1,\ldots,m\\}.$

For great antipodal sets of a complex Grassmannian manifold, H. Kurihara and
T. Okuda [38] proved the following two main results of this section.

######  Theorem 6.2.

A great antipodal set of a complex Grassmannian manifold $G^{\mathbb{C}}(m,n)$
is an ${\mathcal{E}}$-design with the smallest cardinality.

######  Theorem 6.3.

Let $S$ be a finite subset of $G^{\mathbb{C}}(m,n)$. Then the following
conditions are equivalent:

  * (i)

$S$ is a great antipodal set on $G^{\mathbb{C}}(m,n)$.

  * (ii)

$S$ is an ${\mathcal{E}}\cup{\mathcal{F}}$-design on $G^{\mathbb{C}}(m,n)$
with the smallest cardinality.

######  Remark 6.1.

Theorems 6.2 and 6.3 show that great antipodal sets are “good” designs for
complex Grassmannian manifolds [38].

######  Remark 6.2.

A great antipodal set $S$ is a 1-design on of a complex Grassmannian manifold
according to Theorem 6.2. However, it cannot be a 2-design in general
according to [38, Remark A.1, page 463].

##  7\. Cubature formulas for great antipodal sets in Delsarte theory

Let $\Omega$ be a subset of a Euclidean $n$-space $\mathbb{R}^{n}$. Consider
the following integral:

$\int_{\Omega}f(\bf x)\mu(\bf x)d\bf x$

where $\mu$ is a positive weight function on $\Omega$, where we assume that
all polynomials of up to sufficiently large degrees are always integrable. We
also assume that the weight function $\mu(x)$ is normalized such that
$\int_{\Omega}\mu(\bf x)d\bf x=1$ holds.

######  Definition 7.1.

[31, 48] $($Cubature formula of degree $t)$. Let $X=\\{u_{1},\ldots,u_{N}\\}$
be a finite subset of $\Omega\subset\mathbb{R}^{n}$. Then, for any polynomial
$f(\bf x)$ of degree $t$ over real field $\mathbb{R}$ and $N$ positive real
numbers $\lambda_{1},\ldots,\lambda_{N}$, the equation:

${\int_{\Omega}f({\bf x})\mu({\bf x})d{\bf
x}}=\sum_{i=1}^{N}\lambda_{i}f(u_{i})$

is called a cubature formula of degree $t$ with $N$ points, where
$\lambda_{1},\ldots,\lambda_{N}$ are independent of the choice of the
polynomial $f(\bf x)$.

T. Okuda and H. Kurihara [48] established a formulation of Delsarte theory for
finite subsets of compact symmetric spaces. As an application, they proved
that great antipodal subsets of complex Grassmannian manifolds give rise to
the following cubature formulas.

######  Theorem 7.1.

[48] Let $X$ be a great antipodal set of $G^{\mathbb{C}}(m,n)$ and
$\mathcal{S}$ be a finite-dimensional functional space on
$G^{\mathbb{C}}(m,n)$. Then the following cubature formula:

(7.1) $\frac{1}{{\rm
vol}(G^{\mathbb{C}}(m,n))}\int_{G^{\mathbb{C}}(m,n)}fd_{\mu_{G^{\mathbb{C}}(m,n)}}=\frac{1}{|X|}\sum_{x\in
X}f(x),\;\;\forall f\in\mathcal{S},$

holds, where $\mu_{G^{\mathbb{C}}(m,n)}$ is a $U(n)$-invariant Haar measure
and ${\rm vol}(G^{\mathbb{C}}(m,n))$ is the volume of $G^{\mathbb{C}}(m,n)$
with respect to the measure $\mu_{G^{\mathbb{C}}(m,n)}$. Furthermore, any
great antipodal subset $X$ has the minimum cardinality as a finite subset of
$G^{\mathbb{C}}(m,n)$ such that the formula (7.1) holds

##  8\. Links between Euler number and 2-number

###  8.1. 2-number and Euler number

The author and T. Nagano proved in [22] the following links between 2-number
and Euler number.

######  Theorem 8.1.

$\\#_{2}M\geq\chi(M)$ for a compact symmetric space $M$.

######  Theorem 8.2.

$\\#_{2}M=\chi(M)$ for a compact Hermitian symmetric space of semi-simple
type.

###  8.2. 2-number and covering map

The following links between 2-number and covering map were also obtained in
[22].

######  Theorem 8.3.

Let $M$ and $M^{\prime\prime}$ be compact symmetric spaces. If $M$ is a double
covering of $M^{\prime\prime}$, then we have $\\#_{2}M\leq
2\,\\#_{2}(M^{\prime\prime}).$

######  Remark 8.1.

Inequality $\\#_{2}M\leq 2\,\\#_{2}(M^{\prime\prime})$ in Theorem 8.3 is
optimal, because the equality holds for group manifold $SO(2m)$, $m>2$.

For $k$-fold coverings with odd $k$, we have

######  Theorem 8.4.

Let $\phi:M\to N$ be a $k$-fold covering between compact symmetric spaces.
When $k$ is odd, we have $\\#_{2}M=\\#_{2}(N).$

######  Remark 8.2.

Recently, M. S. Tanaka and H. Tasaki established a refinement of Theorem 8.4
in the case of compact Lie groups, see [57] for details.

###  8.3. 2-number and homology

M. Takeuchi [54] proved in 1989 the following link between 2-number and
$\mathbb{Z}_{2}$-homology for symmetric $R$-spaces.

######  Theorem 8.5.

$\,\\#_{2}M=\dim H(M,\mathbb{Z}_{2})$ for every symmetric $R$-space $M$, where
$H(M,\mathbb{Z}_{2})$ is the $\mathbb{Z}_{2}$-homology group of $M$.

##  9\. Applications to group theory

In 1953, A. Borel and J.-P. Serre [11] defined the 2-rank, $r_{2}G$, of a
compact Lie group $G$ as the maximal possible rank of the elementary
2-subgroups of $G$. In [11] they also proved the following two results:

  * (1)

$rk(G)\leq r_{2}(G)\leq 2\,rk(G)$ and

  * (2)

$G$ has 2-torsion if $rk(G)<r_{2}(G)$

for any compact connected Lie group $G$, where $rk(G)$ is the ordinary rank of
$G$.

Borel and Serre [11] were able to determine the 2-rank of simply-connected
simple Lie groups $SO(n),Sp(n),U(n),G_{2}$ and $F_{4}$. They also proved that
$G_{2}$, $F_{4}$ and $E_{8}$ have 2-torsion. On the other hand, they pointed
out in [11, page 139] that they were unable to determine 2-rank for $E_{6}$
and $E_{7}$ among others. To settle this Borel–Serre’s problem, the author and
T. Nagano established in [21] the following simple links between 2-number and
2-rank.

######  Theorem 9.1.

For a connected compact Lie group $G$, we have $\\#_{2}G=2^{r_{2}G}.$

######  Theorem 9.2.

[21] For two connected compact Lie groups $G_{1}$ and $G_{2}$, we have
$\\#_{2}(G_{1}\times G_{2})=2^{r_{2}G_{1}+r_{2}G_{2}}.$

Since we are able to determine 2-numbers for (most) compact symmetric spaces
in [22] via our $(M_{+},M_{-})$-theory developed earlier in 1970s–1980s, we
are able to settle this problem of Borel and Serre’s problem on 2-ranks of Lie
groups (see [19, 20, 21, 22] and [13, 14, 15, 16, 17]).

Now, we state the 2-ranks of compact Lie groups as follows.

###  9.1. Classical groups

For classical groups we have:

######  Theorem 9.3.

For the unitary group $U(n)$, we have

$r_{2}(U(n)/{\mathbb{Z}}\mu)=\begin{cases}n+1&\text{if $\mu$ is even and $n=2$
or $4$;}\\\ n&\text{otherwise,}\end{cases}$

where ${\mathbb{Z}}\mu$ is a cyclic normal subgroup of order $\mu$.

######  Theorem 9.4.

For $SU(n)$, we have

$r_{2}(SU(n)/{\mathbb{Z}}\mu)=\begin{cases}n+1&\text{for $(n,\mu)=(4,2)$;}\\\
n&\text{for $(n,\mu)=(2,2)$ or $(4,4)$;}\\\ n-1&\text{for the other
cases.}\end{cases}$

######  Theorem 9.5.

One has $r_{2}(SO(n))=n-1$, and for $SO(n)^{*}$ we have

$r_{2}(SO(n)^{*})=\begin{cases}4&\text{for $n=4$;}\\\ n-2&\text{for $n$ even
$>4$}.\end{cases}$

######  Theorem 9.6.

We have

  * (a)

$r_{2}(O(n))=n$;

  * (b)

$r_{2}(O(n)^{*})$ is $n=2$ or $4$, while it is $n-1$ otherwise,

where $O(n)^{*}=O(n)/\\{\pm 1\\}$.

######  Theorem 9.7.

We have $r_{2}(Sp(n))=n$, and for $Sp(n)^{*}$ we have

$r_{2}(Sp(n)^{*})=\begin{cases}n+2&\text{for $n=2$ or $4$}\\\
n+1&\text{otherwise}.\end{cases}$

###  9.2. Spinors, semi-spinors and $Pin(n)$

For spinor we have the following.

######  Theorem 9.8.

We have

$r_{2}(Spin(n))=\begin{cases}r+1&\text{if $\,n\equiv-1,0$ or {\rm 1 (mod
8)}}\\\ r&\text{otherwise}.\end{cases}$

where $r=[\frac{n}{2}]$ is the rank of $Spin(n)$.

######  Theorem 9.9.

We have $r_{2}(Spin(n+8))=r_{2}(Spin(n))+4$ for $n\geq 0.$

For semi-spinor group $SO(4m)^{\\#}=Spin(4m)/\\{1,e_{((4m))}\\}$, we have

######  Theorem 9.10.

Let $r$ be the rank $2m$ of $SO(4m)^{\\#}$. Then we have:

$r_{2}(SO(4m)^{\\#})=\begin{cases}3&\text{if $m=1$}\\\ 6&\text{if $m=2$,}\\\
r+1&\text{if $m$ is even $>2$, }\\\ r&\text{if $m$ is odd $>1$}.\end{cases}$

$Pin(n)$ was introduced by M. F. Atiyah, R. Bott and A. Shapiro in [1].

######  Theorem 9.11.

We have $r_{2}(Pin(n))=r_{2}(Spin(n+1))$, $n\geq 0$.

###  9.3. Exceptional groups

For exceptional Lie groups we have

######  Theorem 9.12.

$r_{2}G_{2}=3,\,r_{2}F_{4}=5,\,r_{2}E_{6}=6,\,r_{2}E_{7}=7,\,r_{2}E_{8}=9$ and
$r_{2}E^{*}_{6}=6$.

######  Remark 9.1.

$r_{2}G_{2}=3$ and $r_{2}F_{4}=5$ above are due to A. Borel and J.-P. Serre
[11].

## References

  * [1] M. F. Atiyah, R. Bott and A. Shapiro,  Clifford modules,  Topology 3, (1964), Suppl. 1, 3–38.
  * [2] C. Bachoc,  Designs, groups and lattices, J. Theor. Nombres Bordeaux 17 (2005), 25–44.
  * [3] C. Bachoc,  Linear programming bounds for codes in Grassmannian spaces,  IEEE Trans. Inform. Theory 52 (2006), 2111–2125.
  * [4] C. Bachoc, E. Bannai and R. Coulangeon,  Codes and designs in Grassmannian spaces. Discrete Math. 277 (2004), 15–28.
  * [5] C. Bachoc, R. Coulangeon and G. Nebe,  Designs in Grassmannian spaces and lattices.  J. Algebraic Combin. 16 (2002), 5–19.
  * [6] A. Barg and D. Nogin,  A bound on Grassmannian codes, J. Combin. Theory Ser. A 113 (2006), 1629–1635.
  * [7] E. Bannai and E. Bannai,  A survey on spherical designs and algebraic combinatorics on spheres, European J. Combin. 30 (2009), 1392–1425.
  * [8] E. Bannai and S. G. Hoggar,  On tight $t$-designs in compact symmetric spaces of rank one, Proc. Japan Acad. Ser. A Math. Sci. 61 (1985), 78–82.
  * [9] E. Bannai and S. G. Hoggar,  Tight $t$-designs and squarefree integers, European J. Combin. 10 (1989), 113–135.
  * [10] E. Bannai, T. Okuda and M. Tagami,  Spherical designs of harmonic index t,  J. Approx. Theory 195 (2015), 1–18.
  * [11] A. Borel and J.-P. Serre,  Sur certains sousgroupes des groupes de Lie compacts,  Comm. Math. Helv. 27 (1953), 128–139.
  * [12] A. E. Brouwer, A. M. Cohen and A. Neumaier,  Distance-regular graphs, Ergebnisse der Mathematik und ihrer Grenzgebiete (3), volume 18 (1989).  Springer-Verlag, Berlin.
  * [13] B.-Y. Chen,  A new approach to compact symmetric spaces and applications,  Katholieke Universiteit Leuven, Louvain, Belgium, 1987.
  * [14] B.-Y. Chen,  Symmetries of compact symmetric spaces,  Geometry and Topology of Submanifolds (Marseille, 1987), 38–48, World Sci. Publ., Teaneck, NJ, 1989.
  * [15] B.-Y. Chen,  The 2-ranks of connected compact Lie groups,  Taiwanese J. Math. 17 (2013), no. 3, 815–831.
  * [16] B.-Y. Chen,  Two-numbers and their applications – a survey,  Bull. Belg. Math. Soc. Simon Stevin 25 (2018), no. 4, 565–596.
  * [17] B.-Y. Chen,  The $(M_{+},M_{-})$-method on compact symmetric spaces and its applications,  Contemp. Math. 777 (2022), 41–64. DOI: 10.1090/conm/777/15624
  * [18] B.-Y. Chen,  Geometry and topology of maximal antipodal sets and related topics,  Rom. J. Math. Comput. Sci. 13 (2023), no. 2, 6–25.
  * [19] B.-Y. Chen and T. Nagano,  Totally geodesic submanifolds of symmetric spaces I,  Duke Math. J. 44 (1977), 745–755.
  * [20] B.-Y. Chen and T. Nagano,  Totally geodesic submanifolds of symmetric spaces II,  Duke Math. J. 45 (1978), 405–425.
  * [21] B.-Y. Chen and T. Nagano,  Un invariant géométrique riemannien,  C. R. Acad. Math. 295 (1982), 389–391.
  * [22] B.-Y. Chen and T. Nagano,  A Riemannian Geometric Invariant and its Applications to a Problem of Borel and Serre. Trans. Amer. Math. Soc. 308 (1988), 273–297.
  * [23] J. H. Conway, R. H. Hardin and N. J. A. Sloane,  Packing lines, planes, etc.: Packings in Grassmannian spaces,  Exp. Math. 5 (1996) 139–159.
  * [24] P. Delsarte,  An algebraic approach to the association schemes of coding theory, Philips Res. Rep. Suppl. (1973), vi+97 pp.
  * [25] P. Delsarte, J. M. Goethals and J. J. Seidel,  Bounds for systems of lines, and Jacobi polynomials, Philips Res. Rep. 30 (1975), 91–105.
  * [26] P. Delsarte, J. M. Goethals and J. J. Seidel,  Spherical codes and designs, Geom. Dedicata 6 (1977), 363–388.
  * [27] A. Gavrilyuk, S. Suda and J. Vidali,  On tight 4-designs in Hamming association schemes,  Combinatorica 40 (2020), 345–362.
  * [28] C. D. Godsil,  Algebraic combinatorics,  Chapman and Hall Mathematics Series, New York, 1993.
  * [29] J. M. Goethals and J. J. Seidel,  Spherical designs,  Proc. Symp. Pure Math. 34 (1979), 255–272.
  * [30] S. Helgason,  Differential Geometry, Lie Groups and Symmetric Spaces,  Academic Press, New York, NY (1978).
  * [31] M. Hirao, T. Okuda and M. Sawa,  Some remarks on cubature formulas with linear operators,  J. Math. Soc. Japan 68 (2016), 711–735.
  * [32] S. G. Hoggar,  $t$-designs in projective spaces, European J. Combin. 3 (1982), 233–254.
  * [33] S. G. Hoggar,  Parameters of $t$-designs in $FP^{d-1}$, European J. Combin. 5 (1984), 29–36.
  * [34] S. G. Hoggar,  Tight 4- and 5-designs in projective spaces, Graphs Combin. 5 (1989), 87–94.
  * [35] S. G. Hoggar,  $t$-designs in Delsarte spaces,  in: Coding Theory and Design Theory, Part II, in: IMA Vol. Math. Appl., vol. 21, 1990, pp. 144–165.
  * [36] S. Kobayashi and T. Nagano,  On filtered Lie algebras and geometric structures I,  J. Math. Mech. 13 (1964), 875–907.
  * [37] H. Kurihara,  Antipodal sets and designs on unitary groups,  Graphs and Combin. 37(5) (2021), 1559–1583.
  * [38] H. Kurihara and T. Okuda,  Great antipodal sets of complex Grassmannian manifolds as designs with the smallest cardinalities,  J. Algebra 559 (2020), 432–466.
  * [39] V. I. Levenshtein,  Designs as maximum codes in polynomial metric spaces. Interactions between algebra and combinatorics, Acta Appl. Math. 29 (1992), 1–82.
  * [40] V. I. Levenshtein.  Universal bounds for codes and designs, in:  Handbook of Coding Theory, vol. I, II.  North-Holland, Amsterdam, 1998, pp. 499–648.
  * [41] V. I. Levenshtein,  On designs in compact metric spaces and a universal bound on their size, Discrete Math. 192 (1998), 251–271.
  * [42] Y. I. Lyubich,  On tight projective designs, Des. Codes Cryptogr. 51 (2009), 21–31.
  * [43] L. A. Lyusternik and A. I. Fet,  Variational problems on closed manifolds,  Doklady Akad. Nauk SSSR (N.S.) 81 (1951). 17–18.
  * [44] T. Nagano,  Transformation groups on compact symmetric spaces,  Trans. Amer. Math. Soc. 118 (1965), 428–453.
  * [45] Y. Nakata, C. Hirche, C. Morgan and A. Winter,  Unitary 2-designs from random X-and Z-diagonal unitaries,  J. Math. Phys. 58 (2017), no. 5, Paper No. 052203, 16 pp.
  * [46] A. Neumaier.  Distances, graphs and designs,  European J. Combin. 1 (1980) 163–174.
  * [47] A. Neumaier,  Combinatorial configurations in terms of distances, Memorandum 81–09 (Dept. of Mathematics), Eindhoven University of Technology, 1981.
  * [48] T. Okuda,  Cubature formulas for great antipodal sets on complex Grassmann manifolds,  RIMS Kokyuroku (2017), 2039, pp. 79–89. Research Institute for Mathematical Sciences, Kyoto University. http://hdl.handle.net/2433/236889
  * [49] A. Roy,  Bounds for codes and designs in complex subspaces, J. Algebraic Combin. 31 (2010), 1–32.
  * [50] A. Roy and A. J. Scott,  Unitary designs and codes, Des. Codes Cryptogr. 53 (2009), 13–31.
  * [51] A. Roy and S. Suda,  Complex spherical designs and codes, J. Comb. Des. 22 (2014), 105–148.
  * [52] P. W. Shor and N. J. A. Sloane,  A family of optimal packings in Grassmannian manifolds,  J. Algebraic Combin. 7 (1998) 157–163.
  * [53] M. Takeuchi,  Cell decompositions and Morse equalities on certain symmetric spaces,  J. Fac. Sci. Univ. Tokyo 12 (1965), 81–192.
  * [54] M. Takeuchi,  Two-number of symmetric $R$-spaces. Nagoya Math. J. 115 (1989), 43–46,
  * [55] M. S. Tanaka and H. Tasaki,  The intersections of two real forms in Hermitian symmetric spaces of compact type, J. Math. Soc. Japan 64 (2012), 1297–1332.
  * [56] M. S. Tanaka and H. Tasaki,  Antipodal sets of symmetric R-spaces, Osaka J. Math, 50 (2013), 161–169.
  * [57] M. S. Tanaka and H. Tasaki,  Maximal antipodal subgroups and covering homomorphisms with odd degree, Int. Electron. J. Geom. 17 (2024), 153–156.
  * [58] Z. Xu, Z. Xu and W.-H. Yu,  Bounds on antipodal spherical designs with few angles,  Electron. J. Combin. 28 (2021), Paper No. 3.39.


# On two-variable guarded fragment logic with expressive local Presburger
constraints

Chia-Hsuan Lu  and  Tony Tan  National Taiwan University, No. 1, Sec. 4,
Roosevelt Rd., Taipei 10617, Taiwan<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

We consider the extension of two-variable guarded fragment logic with local
Presburger quantifiers. These are quantifiers that can express properties such
as “the number of incoming blue edges plus twice the number of outgoing red
edges is at most three times the number of incoming green edges” and captures
various description logics with counting, but without constant symbols. We
show that the satisfiability of this logic is EXP-complete. While the lower
bound already holds for the standard two-variable guarded fragment logic, the
upper bound is established by a novel, yet simple deterministic graph
theoretic based algorithm.

###### Key words and phrases:

Two-variable guarded fragment, local counting constraints, satisfiability,
$\exp$-complete

##  1\. Introduction

In this paper we consider the extension of two-variable guarded fragment logic
with the so called local Presburger quantifiers, which we denote by
$\textsf{GP}^{2}$. These are quantifiers that can express local numerical
properties such as “the number of outgoing red edges plus twice the number of
incoming green edges is at most three times the number of outgoing blue
edges.” It was first considered in [BOPT21] and captures various description
logics up to $\mathcal{ALCIH}b^{\textsf{self}}$ [BHLS17, BCM+03, Grä98].
Recently Bednarczyk, et. al. [BOPT21] showed that both satisfiability and
finite satisfiability are in 3-NEXP by reduction to the two-variable logic
with counting quantifiers.

We show that the satisfiability of this logic is EXP-complete. The lower bound
is already known for the standard two-variable guarded-fragment logic [Grä99].
The contribution is the upper bound, which is established by a novel, yet
simple deterministic exponential time algorithm. Intuitively, the algorithm
starts by representing the input sentence as a graph whose vertices and edges
represent the allowed types. It then successively eliminates the vertex/edge
that contradicts the input sentence until there is no more vertex/edge to
eliminate. The flavor is quite similar to the notion of type-elimination,
first introduced by Pratt [Pra79].

On the other hand, our algorithm has a markedly different flavor from the
standard tableaux method usually used to establish the upper bound of guarded
fragment logics. Note that tableaux method usually works by exploiting the so
called tree-like model property, where it tries to construct a tree-like model
using polynomial space alternating Turing machine. To apply this, it is
essential that there is only a polynomial bound on the number of branching
from each node in the tree and it is not clear whether this bound still holds
for $\textsf{GP}^{2}$. In fact, already for $\textsf{GC}^{2}$ (two-variable
guarded fragment with counting quantifiers), the exponential time upper bound
is established by first reducing it to three-variable guarded fragment, before
the tableaux method can be applied [Kaz04]. It is not clear a priori how this
technique can be extended to $\textsf{GP}^{2}$.

#### Acknowledgement.

Recently in [BF22] Bednarczyk and Fiuk independently obtained the same EXP
upper bound for $\textsf{GP}^{2}$. Their proof uses automata theoretic method
and yields a rather involved alternating polynomial space algorithm. A brief
comparison between their algorithm and ours is presented in Sect. 3.6.

#### Other related work.

The guarded fragment is one of the most prominent decidable fragments of
first-order logic [ANvB98]. The satisfiability is 2-EXP-complete and drops to
EXP-complete when the number of variables or the arity of the signature is
fixed [Grä99]. Various DL and ML (description and modal logics) are captured
by the fragment when the arity is fixed to two [Grä98, BCM+03, BHLS17]. The
key reason for the decidability of the guarded fragment is the tree-like model
property which allows the application of the tableaux method [Var96].

Recently, a deterministic exponential time algorithm for the two-variable
guarded-fragment was proposed in [LLT21]. The algorithm there is also a graph-
based algorithm, which also has a similar flavor to type-elimination
algorithm, but, it is not clear, a priori, how their algorithm can be extended
to $\textsf{GP}^{2}$.

Pratt-Hartmann [Pra07] proposed an elegant reduction of $\textsf{GC}^{2}$
formulas to (exponential size) “homogeneous” instances of Integer Linear
Programming (ILP) which are of the form $A\bar{x}=0\wedge
B\bar{x}\geqslant\bar{c}$, where $A$ and $B$ are matrices with integer
entries, $\bar{x}$ is a (column) vector of variables and $\bar{c}$ is a vector
of integers. Note that to check whether $A\bar{x}=0\wedge
B\bar{x}\geqslant\bar{c}$ admits a solution in $\mathbb{N}$, it is sufficient
to check whether it admits a solution in $\mathbb{Q}$, which is known to be in
PTIME. This implies the EXP upper bound for both satisfiability and finite
satisfiability of $\textsf{GC}^{2}$.

In general, $\textsf{GP}^{2}$ captures various description logics with
counting such as $\mathcal{ALCIHQ}$ and $\mathcal{ALCIH}b^{\textsf{self}}$,
but without constant symbol [BCM+03]. Note that adding constant symbols to
even $\textsf{GC}^{2}$ makes the complexity of satisfiability jumps to NEXP-
complete [Tob01].

Some logics that allow similar quantifiers as the local Presburger quantifiers
were proposed and studied various researchers [Baa17, BBR20, DL10, KP10]. The
decidability result is obtained by the tableaux method, but their logics do
not allow the inverses of binary relations.

The extension of one-variable logic with quantifiers of the form
$\exists^{S}x\ \phi(x)$, where $S$ is a ultimately periodic set, is NP-
complete [Bed20]. Semantically $\exists^{S}x\ \phi(x)$ means the number of $x$
where $\phi(x)$ holds is in the set $S$. The extension of two-variable logic
with such quantifiers is later shown to be $2$-NEXP [BKT20] whose proof makes
heavy use of the biregular graph method introduced in [KT15] to analyze the
spectrum of two-variable logic with counting quantifiers. The proofs and
results in [BKT20, KT15] do not apply in our setting since the logics they
considered already subsume full two-variable logic.

#### Organization

This paper is organized as follows. In Section 2 we present the formal
definition of $\textsf{GP}^{2}$. The main result is presented in Section 3. We
conclude with Section 4.

##  2\. Two-variable guarded fragment with local Presburger constraints
$(\textsf{GP}^{2})$

Let $\mathbb{N}$ denote the set of natural numbers $\\{0,1,2,\ldots\\}$. We
fix a vocabulary $\Sigma$ consisting of only unary and binary predicates and
there is no constant symbol. We will consider the logic with the equality
predicate. As usual, for a vector $\bar{x}$ of variables, we write
$\varphi(\bar{x})$ to denote that the free variables in the formula $\varphi$
are exactly those in $\bar{x}$.

Let $\mathcal{A}$ be a structure and let $a$ be an element in $\mathcal{A}$.
For a formula $\varphi(x,y)$, we denote by
$|\varphi(x,y)|^{x/a}_{\mathcal{A}}$ the number of element $b$ such that
$\mathcal{A},x/a,y/b\models\varphi(x,y)$.

#### Local Presburger (LP) quantifiers.

These are quantifiers of the form:

$\mathcal{P}(x)\quad:=\quad\sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{r_{i}}[\varphi_{i}(x,y)]\quad\circledast\quad\delta$

where $\lambda_{i}$, $\delta$ are integers; $r_{i}$ is either $R(x,y)$ or
$R(y,x)$ for some binary relation $R$; $\varphi_{i}(x,y)$ is a formula with
free variables $x$ and $y$; and $\circledast$ is one of $=$, $\neq$,
$\leqslant$, $\geqslant$, $<$, $>$, $\equiv_{d}$ or $\not\equiv_{d}$, where
$d\in\mathbb{N}$. Here $\equiv_{d}$ denotes the congruence modulo $d$. Note
that $\mathcal{P}(x)$ has one free variable $x$.

The semantics is defined as $\mathcal{A},x/a\models\mathcal{P}(x)$, if the
(in)equality $\circledast$ holds when each $\\#_{y}^{r_{i}}[\varphi_{i}(x,y)]$
is substituted with $|r_{i}(x,y)\wedge\varphi_{i}(x,y)|^{x/a}_{\mathcal{A}}$
and each $|r_{i}(x,y)\wedge\varphi_{i}(x,y)|^{x/a}_{\mathcal{A}}$ is finite.

The quantifier $\mathcal{P}(x)$ is in basic form, if it is of the form:

$\mathcal{P}(x)\quad:=\quad\sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{R_{i}(x,y)}[x\neq y]\quad\circledast\quad\delta$

That is, each $\varphi_{i}(x,y)$ is simply the inequality $x\neq y$. In other
words, an LP quantifier in basic form is a linear constraint on the number of
its outgoing $R_{i}$-edges.

Note that for $\mathcal{A},x/a\models\mathcal{P}(x)$, we insist that each
$|r_{i}(x,y)\wedge\varphi_{i}(x,y)|^{x/a}_{\mathcal{A}}$ is finite. The
purpose is only to avoid clutter. Obviously, we can easily modify it to allow
for the case when $|r_{i}(x,y)\wedge\varphi_{i}(x,y)|^{x/a}_{\mathcal{A}}$ is
$\infty$ and this will be discussed in Sect. 3.5.

#### The guarded fragment class.

The class GF of guarded fragment logic is the smallest set of first-order
formulas such that the following holds.111In this paper
$\bar{x},\bar{y},\bar{z}$ denote vectors of variables and
$\bar{x}\subseteq\bar{z}$ means the variables that appear in $\bar{x}$ also
appears in $\bar{z}$.

  * •

GF contains all atomic formulas $R(\bar{x})$ and equalities between variables.

  * •

GF is closed under boolean combinations.

  * •

If $\varphi(\bar{x})$ is in GF, $R(\bar{z})$ is an atomic predicate and
$\bar{x},\bar{y}\subseteq\bar{z}$, then both $\exists\bar{y}\
R(\bar{z})\wedge\varphi(\bar{x})$ and $\forall\bar{y}\
R(\bar{z})\to\varphi(\bar{x})$ are also in GF.

We define the class GP to be the extension of GF with LP quantifiers, i.e., by
adding the following rule.

  * •

An LP quantifier $\mathcal{P}(x):=\sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{r_{i}}[\varphi_{i}(x,y)]\ \circledast\ \delta$ is in
GP if and only if each $\varphi_{i}(x,y)$ is in GP.

We denote by $\textsf{GP}^{2}$ the restriction of GP to formulas using only
two variables: $x$ and $y$.

We denote by $\text{SAT}(\textsf{GP}^{2})$ the problem that on input
$\textsf{GP}^{2}$ formula $\varphi$, decide if it is satisfiable. The
following lemma states that it suffices to consider only $\textsf{GP}^{2}$
formulas in a normal form.

######  Lemma 1.

There is a linear time algorithm that converts a $\textsf{GP}^{2}$ formula
into the following equisatisfiable normal form (over an extended signature):

$\Psi:=\forall x\ \gamma(x)\quad\wedge\quad\bigwedge_{i=1}^{k}\forall x\forall
y\ \alpha_{i}(x,y)\wedge\ \bigwedge_{i=1}^{\ell}\forall x\
\big{(}q_{i}(x)\to\mathcal{P}_{i}(x)\big{)}$ (1)

where

  * •

$\gamma(x)$ is quantifier free formula,

  * •

each $\alpha_{i}(x,y)$ is a quantifier free formula of the form:

$(R(x,y)\wedge x\neq y)\ \to\ \beta(x,y)$

where $R(x,y)$ is an atomic predicate and $\beta(x,y)$ is quantifier free
formula,

  * •

each $q_{i}(x)$ is an atomic predicate,

  * •

each $\mathcal{P}_{i}(x)$ is an LP quantifier in basic form.

######  Proof 2.1.

The proof uses a routine renaming technique (see, e.g., [Kaz04, Pra07]). For
completeness, we present it here.

Intuitively, we rename each subformula of one free variable with a fresh unary
predicate. The renaming is done bottom-up starting from the subformula with
the lowest quantifier rank. The detail is as follows. We consider the
following three cases.

  * •

Case 1: A subformula in the form of an LP quantifier:

$\displaystyle\mathcal{P}(x)\ $ $\displaystyle:=\ \sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{r_{i}}[\varphi_{i}(x,y)]\quad\circledast\quad\delta$
(2)

where each $\varphi_{i}(x,y)$ is quantifier free.

  * •

Case 2: A subformula with one free variable $x$ of the form:

$\displaystyle\psi(x)\ $ $\displaystyle:=\ \forall y\ r(x,y)\to\varphi(x,y)$
(3)

where $\varphi(x,y)$ is quantifier free.

  * •

Case 3: A subformula with one free variable $x$ of the form:

$\displaystyle\psi(x)\ $ $\displaystyle:=\ \exists y\ r(x,y)\ \wedge\
\varphi(x,y)$ (4)

where $\varphi(x,y)$ is quantifier-free,

All the other cases can be handled symmetrically.

We start with Case 1. Let $\mathcal{P}(x)$ be an LP quantifier in form of (2).
We will first convert it to the basic form. For each $1\leqslant i\leqslant
n$, we introduce a new binary predicate symbol $R_{i}(x,y)$ and rewrite
$\mathcal{P}(x)$ into $\mathcal{P}^{\prime}(x)$ as follows.

$\displaystyle\mathcal{P}^{\prime}(x)\ $ $\displaystyle:=\ \sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{R_{i}(x,y)}[x\neq y]\quad\circledast\quad\delta$

We also add the following conjunct.

$\displaystyle\bigwedge_{i=1}^{n}\forall x\forall y\ R_{i}(x,y)\ \to\
\big{(}r_{i}(x,y)\wedge\varphi_{i}(x,y)\big{)}$ $\displaystyle\wedge\ $
$\displaystyle\bigwedge_{i=1}^{n}\forall x\forall y\ r_{i}(x,y)\ \to\
(\varphi_{i}(x,y)\ \to\ R_{i}(x,y))$

Obviously, $\mathcal{P}^{\prime}(x)$ is in basic form. We then replace
$\mathcal{P}^{\prime}(x)$ with a fresh unary predicate symbol $q(x)$ and add
the following conjunct.

$\forall x\ \ \big{(}q(x)\ \to\ \mathcal{P}^{\prime}(x)\big{)}$

Next, we consider Case 2, i.e., a subformula $\psi(x)$ in the form of (3).
First, we replace $\psi(x)$ with a fresh unary predicate symbol $q(x)$ and add
the following conjunct.

$\forall x\ q(x)\ \to\ \big{(}\forall y\ r(x,y)\ \to\ \varphi(x,y)\big{)}$

Note that this conjunct can be rewritten into:

$\forall x\forall y\ r(x,y)\ \to\ \big{(}q(x)\ \to\ \varphi(x,y)\big{)}$

which in turn can be rewritten into:

$\displaystyle\forall x\ q(x)\ \to\ \big{(}r(x,x)\ \to\ \varphi(x,x)\big{)}$
$\displaystyle\wedge\quad$ $\displaystyle\forall x\forall y\
\big{(}r(x,y)\wedge x\neq y\big{)}\ \to\ \big{(}q(x)\ \to\
\varphi(x,y)\big{)}$

Finally, we consider Case 3, i.e., a subformula $\psi(x)$ in the form of (4).
In this case $\psi(x)$ can be first rewritten into the form: $\neg\forall y\
r(x,y)\ \to\ \neg\varphi(x,y)$, after which we can proceed as in Case 2.

We perform such renaming procedure repeatedly until we obtain a
$\textsf{GP}^{2}$ sentence in normal form (1). This completes the proof of
Lemma 1.

######  Remark 2.

We stress that if the sentence $\Psi$ in normal form (1) is satisfiable, then
it is satisfied in an infinite model. Indeed, let $\mathcal{A}$ be a model of
$\Psi$. We make an infinitely many copies of $\mathcal{A}$, denoted by
$\mathcal{A}_{1},\mathcal{A}_{2},\ldots$, and disjoint union them all to
obtain a new model $\mathcal{B}$. For every pair $(a,b)$, where $a$ and $b$ do
not come from the same $\mathcal{A}_{i}$, we set $(a,b)$ not to be in any
binary relation $R^{\mathcal{B}}$. It is routine to verify that $\mathcal{B}$
still satisfies $\Psi$.

On the other hand, there is a $\textsf{GP}^{2}$ sentence that is satisfied
only by infinite models. Consider the following sentence with one unary
predicate $U$ and one binary predicate $R$.

$\displaystyle\Phi\ $ $\displaystyle:=\ \forall x\ U(x)\ \wedge\ \forall
x\big{(}U(x)\ \to\ \\#^{R(x,y)}_{y}[\top]=2\big{)}\ \wedge\ \forall
x\big{(}U(x)\ \to\ \\#^{R(y,x)}_{y}[\top]\leqslant 1\big{)}$

Intuitively, $\Phi$ states that every element must belong to the unary
predicate $U$ and that every element has exactly two outgoing $R$-edges and at
most one incoming $R$-edge. It is routine to verify that an infinite binary
tree (whose vertices are all in $U$) satisfies $\Phi$ and that every model of
$\Phi$ must be infinite.

##  3\. The satisfiability of $\textsf{GP}^{2}$

We introduce some terminology in Section 3.1. Then, we show how to represent
$\textsf{GP}^{2}$ formulas as graphs in Section 3.2. The algorithm is
presented in Section 3.3. Throughout this section we fix a sentence $\Psi$ in
the normal form (1) over the signature $\Sigma$. We assume that the signature
$\Sigma$ is finite.

###  3.1. Terminology

A _unary type_ (over $\Sigma$) is a maximally consistent set of unary
predicates from $\Sigma$ or their negations, where each atom uses only the
variable $x$. Similarly, a binary type is a maximally consistent set of binary
predicates from $\Sigma$ or their negations containing the atom $x\neq y$,
where each atom or its negation uses two variables $x$ and $y$.222In the
standard definition of 2-type, such as in [GKV97, Pra05], a 2-type contains
unary predicates or its negation involving variable $x$ or $y$. For our
purpose, we define a binary type as consisting of only binary predicates that
strictly use both variables $x$ and $y$. We view $r(x,x)$ as a unary
predicate. We denote by $\overline{\eta}(x,y)$ the “reverse” of $\eta(x,y)$,
i.e., the binary type obtained by swapping the variables $x$ and $y$. The
binary type that contains only the negations of atomic predicates from
$\Sigma$ is called the _null_ type, denoted by $\eta_{\text{null}}$.
Otherwise, it is called a _non-null_ type.

Note that both unary and binary types can be viewed as quantifier-free
formulae that are the conjunction of their elements. We will use the symbols
$\pi$ and $\eta$ (possibly indexed) to denote unary and binary type,
respectively. When viewed as formula, we write $\pi(x)$ and $\eta(x,y)$,
respectively. We write $\pi(y)$ to denote formula $\pi(x)$ with $x$ being
substituted with $y$. Let $\Pi$ denote the set of all unary types over
$\Sigma$ and let $\mathcal{K}$ be the set of all non-null binary types over
$\Sigma$.

For a structure $\mathcal{A}$ (over $\Sigma$), the _type of an element_ $a\in
A$ is the unique unary type $\pi$ that $a$ satisfies in $\mathcal{A}$.
Similarly, the type of a pair $(a,b)\in A\times A$, where $a\neq b$, is the
unique binary type that $(a,b)$ satisfies in $\mathcal{A}$. The configuration
of a pair $(a,b)$ is the tuple $(\pi,\eta,\pi^{\prime})$ where $\pi$ and
$\pi^{\prime}$ are the types of $a$ and $b$, respectively, and $\eta$ is the
type of $(a,b)$. In this case we will also call $(a,b)$ an $\eta$-edge in
$\mathcal{A}$. If $\eta$ is non-null, then we say that $b$ is a neighbour of
$a$. The set of all neighbours of $a$ is called the neighbourhood of $a$.

We say that a unary type $\pi$ is realized in $\mathcal{A}$, if there is an
element whose type is $\pi$. Likewise, a configuration
$(\pi,\eta,\pi^{\prime})$ is realized in $\mathcal{A}$, if there is a pair
$(a,b)$ whose configuration is $(\pi,\eta,\pi^{\prime})$.

#### The graph representation.

In this paper the term graph means finite edge-labelled directed graph
$G=(V,E)$, where $V\subseteq\Pi$ and
$E\subseteq\Pi\times\mathcal{K}\times\Pi$. We can think of an edge
$(\pi,\eta,\pi^{\prime})$ as an edge with label $\eta$ that goes from vertex
$\pi$ to vertex $\pi^{\prime}$. We write $\mathcal{N}_{G}(\pi)$ to denote the
set $\\{(\eta,\pi^{\prime})|(\pi,\eta,\pi^{\prime})\in E\\}$, i.e., the set of
all the edges going out from $\pi$. A graph $H=(V^{\prime},E^{\prime})$ is a
subgraph of $G=(V,E)$ if $V^{\prime}\subseteq V$ and $E^{\prime}\subseteq E$.
We call $H$ a non-empty subgraph of $G$, if $V^{\prime}\neq\emptyset$.

A structure $\mathcal{A}$ conforms to a graph $G$, if the following holds.

  * •

If a type $\pi$ is realized in $\mathcal{A}$, then $\pi$ is a vertex in $G$.

  * •

If a configuration $(\pi,\eta,\pi^{\prime})$ is realized in $\mathcal{A}$,
where $\eta$ is not the null type, then $(\pi,\eta,\pi^{\prime})$ is an edge
in $G$.

Next, we show how the sentence $\Psi$ can be represented as a graph. Recall
that $\Psi$ is a $\textsf{GP}^{2}$ sentence in the normal form (1). We need
the following two definitions.

A unary type $\pi$ is compatible with $\Psi$, if $\pi(x)\models\gamma(x)$.

A configuration $(\pi,\eta,\pi^{\prime})$ is compatible with $\Psi$, if the
following holds.

  * •

Both $\pi$ and $\pi^{\prime}$ are compatible with $\Psi$.

  * •

For each $1\leqslant i\leqslant k$:

$\displaystyle\pi(x)\wedge\eta(x,y)\wedge\pi^{\prime}(y)$
$\displaystyle\models\alpha_{i}(x,y)$
$\displaystyle\pi(y)\wedge\overline{\eta}(x,y)\wedge\pi^{\prime}(x)$
$\displaystyle\models\alpha_{i}(x,y)$

Note that the sentence $\Psi$ defines a directed graph $G_{\Psi}$, where the
vertices are the unary types that are compatible with $\Psi$ and the edges are
$(\pi,\eta,\pi^{\prime})$, for every $(\pi,\eta,\pi^{\prime})$ compatible with
$\Psi$. Moreover, the graph $G_{\Psi}$ is “symmetric” in the sense that
$(\pi,\eta,\pi^{\prime})$ is an edge if and only if
$(\pi^{\prime},\overline{\eta},\pi)$ is an edge.

Intuitively, the vertices and the edges in the graph $G_{\Psi}$ are the
unary/binary types and configurations that do not violate the conjunct
$\forall x\ \gamma(x)$ and $\forall x\forall y\ \alpha_{i}(x,y)$. If there is
a model $\mathcal{A}\models\Psi$, then it is necessary that $\mathcal{A}$
conforms to the graph $G_{\Psi}$. In the next section, we will show how to
analyse the graph $G_{\Psi}$ to infer whether the conjunct
$\bigwedge_{i=1}^{\ell}\forall x\ q_{i}(x)\to\mathcal{P}_{i}(x)$ can also be
satisfied.

###  3.2. The characterization for the satisfiability of $\Psi$

Recall that $\Psi$ is a sentence in normal form (1). For each $1\leqslant
i\leqslant\ell$, let the LP quantifier $\mathcal{P}_{i}(x)$ be:

$\mathcal{P}_{i}(x)\ :=\ \sum_{j=1}^{t_{i}}\
\lambda_{i,j}\cdot\\#_{y}^{R_{i,j}(x,y)}[x\neq
y]\quad\circledast_{i}\quad\delta_{i}$

For a graph $G$, a vertex $\pi$ in $G$ and $1\leqslant i\leqslant\ell$, we
define the linear constraint $\mathcal{Q}_{i}^{G,\pi}$:

$\mathcal{Q}_{i}^{G,\pi}:=\sum_{j=1}^{t_{i}}\ \lambda_{i,j}\ \cdot\
\Bigg{(}\sum_{\begin{subarray}{c}\tiny(\eta^{\prime},\pi^{\prime})\in\mathcal{N}_{G}(\pi)\\\
\text{and}\ R_{i,j}(x,y)\in\eta^{\prime}\end{subarray}}\
z_{\eta^{\prime},\pi^{\prime}}\Bigg{)}\ \circledast_{i}\ \delta_{i}$

The variables in $\mathcal{Q}_{i}^{G,\pi}$ are
$z_{\eta^{\prime},\pi^{\prime}}$, for every
$(\eta^{\prime},\pi^{\prime})\in\mathcal{K}\times\Pi$. Intuitively, each
$z_{\eta^{\prime},\pi^{\prime}}$ represents the number of
$\eta^{\prime}$-edges that goes out from an element with type $\pi$ to another
element with type $\pi^{\prime}$. Note that every element/pair of elements has
a unique unary/binary types. Thus, we can partition the neighbourhood of each
element according to the unary and binary types. This is the reason each
$\\#_{y}^{R_{i,j}(x,y)}[x\neq y]$ is replaced with the sum:

$\sum_{\begin{subarray}{c}\tiny(\eta^{\prime},\pi^{\prime})\ \in\
\mathcal{N}_{G}(\pi)\\\ \text{and}\ \ R_{i,j}(x,y)\ \in\
\eta^{\prime}\end{subarray}}\ z_{\eta^{\prime},\pi^{\prime}}$

We formalize this intuition as Lemma 3.

######  Lemma 3.

Let $G$ be a graph and $\mathcal{A}$ be a structure that conforms to $G$.
Suppose there is an element $a$ in $\mathcal{A}$ whose type is $\pi$ and that
$\mathcal{A},x/a\models\mathcal{P}_{i}(x)$. Then, $\mathcal{Q}_{i}^{G,\pi}$
admits a solution in $\mathbb{N}$.

######  Proof 3.1.

Let $G$, $\mathcal{A}$, $a$ and $\pi$ be as in the hypothesis of the lemma.
For every $(\eta^{\prime},\pi^{\prime})\in\mathcal{N}_{G}(\pi)$, let
$K_{\eta^{\prime},\pi^{\prime}}$ be the number of elements $c$ such that the
configuration of $(a,c)$ is $(\pi,\eta^{\prime},\pi^{\prime})$. Formally:

$K_{\eta^{\prime},\pi^{\prime}}\ =\ \big{|}\\{c\ :\ \text{the configuration
of}\ (a,c)\ \text{is}\ (\pi,\eta^{\prime},\pi^{\prime})\\}\big{|}$

Note that for every neighbour $b$ of $a$, there is exactly one
$(\eta^{\prime},\pi^{\prime})\in\mathcal{N}_{G}(\pi)$ where $b\in
K_{\eta^{\prime},\pi^{\prime}}$, i.e. the sets
$K_{\eta^{\prime},\pi^{\prime}}$’s partitions the neighbourhood of $a$. Since
$\mathcal{A},x/a\models\mathcal{P}_{i}(x)$, it is clear that
$z_{\eta^{\prime},\pi^{\prime}}=K_{\eta^{\prime},\pi}$ is a solution to the
constraint $\mathcal{Q}_{i}^{G,\pi}$.

Next, we define a system of linear constraints that captures whether a certain
configuration can be realized. For an edge $(\pi_{1},\eta,\pi_{2})$ in a graph
$G$, let $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ be the following system of
linear constraints:

$z_{\eta,\pi_{2}}\geqslant 1\ \wedge\bigwedge_{i\ \text{s.t.}\
q_{i}(x)\in\pi_{1}}\mathcal{Q}_{i}^{G,\pi_{1}}$

Similar to $\mathcal{Q}_{i}^{G,\pi}$, the variables in this system are
$z_{\eta^{\prime},\pi^{\prime}}$, for every
$(\eta^{\prime},\pi^{\prime})\in\mathcal{K}\times\Pi$.

The intuitive meaning of the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$
is as follows. If it does not admit a solution in $\mathbb{N}$, then the
configuration $(\pi_{1},\eta,\pi_{2})$ is not realized in any model of $\Psi$.
This is because either $z_{\eta,\pi_{2}}$ must be zero, or one of
$\mathcal{Q}_{i}^{G,\pi_{1}}$ is violated for some $i$ where
$q_{i}(x)\in\pi_{1}$. Its formalization is stated as Lemma 4.

######  Lemma 4.

Let $G$ be a graph and $\mathcal{A}$ be a structure that conforms to $G$.
Suppose there is a pair $(a,b)$ in $\mathcal{A}$ whose configuration is
$(\pi_{1},\eta,\pi_{2})$ and that
$\mathcal{A},x/a\models\bigwedge_{i=1}^{\ell}(q_{i}(x)\to\mathcal{P}_{i}(x))$.
Then, the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ has a solution in
$\mathbb{N}$.

######  Proof 3.2.

The proof is similar to Lemma 3. Let $G$, $\mathcal{A}$, $a$, $b$ and
$(\pi_{1},\eta,\pi_{2})$ be as in the hypothesis. For every
$(\eta^{\prime},\pi^{\prime})\in\mathcal{K}\times\Pi$, let
$K_{\eta^{\prime},\pi^{\prime}}$ denote the number of elements $c$ such that
the configuration of $(a,c)$ is $(\pi_{1},\eta^{\prime},\pi^{\prime})$. Since
the configuration of $(a,b)$ is $(\pi_{1},\eta,\pi_{2})$, we have
$K_{\eta,\pi_{2}}\geqslant 1$. Since
$\mathcal{A},x/a\models\bigwedge_{i=1}^{\ell}q_{i}(x)\to\mathcal{P}_{i}(x)$,
the assignment $z_{\eta^{\prime},\pi^{\prime}}=K_{\eta^{\prime},\pi^{\prime}}$
is a solution to the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$.

To infer the satisfiability of $\Psi$ from the graph $G_{\Psi}$, we will need
a few more terminology.

An edge $(\pi_{1},\eta,\pi_{2})$ is a bad edge in a graph $G$ (w.r.t. the
sentence $\Psi$), if the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ does
not admit a solution in $\mathbb{N}$.

Note that by Lemma 4, if $(\pi_{1},\eta,\pi_{2})$ is a bad edge in $G$, then
there is no model $\mathcal{A}$ that conforms to $G$ such that the
configuration $(\pi_{1},\eta,\pi_{2})$ is realized in $\mathcal{A}$ and that
$\mathcal{A}\models\forall x\ (q_{i}(x)\to\mathcal{P}_{i}(x))$ for every
$1\leqslant i\leqslant\ell$.

Next, we present a similar notion for vertices in $G$.

A vertex $\pi$ is a bad vertex in $G$ (w.r.t. the sentence $\Psi$), if the
following holds.

  * •

It does not have any outgoing edge in $G$.

  * •

There is $1\leqslant i\leqslant\ell$ such that $\pi$ contains $q_{i}(x)$, but
the constraint $\mathcal{Q}_{i}^{G,\pi}$ does not admit a zero solution, i.e.,
the solution where all the variables are assigned with zero.

The intuitive meaning of bad vertex is as follows. Suppose $\mathcal{A}$ is a
structure that conforms to a graph $G$ and that $\pi$ has no outgoing edge in
$G$. This means that for every element $a$ with type $\pi$ the value
$|R_{i,j}(x,y)\wedge x\neq y|^{x/a}_{\mathcal{A}}$ is zero. So, for every
$1\leqslant i\leqslant\ell$, if $\pi$ contains $q_{i}(x)$ and if
$\mathcal{A},x/a\models\mathcal{P}_{i}(x)$, then the following must hold.

$\sum_{j=1}^{t_{i}}\ \lambda_{i,j}\cdot|R_{i,j}(x,y)\wedge x\neq
y|^{x/a}_{\mathcal{A}}=0$

That $\pi$ is a bad vertex means that $\delta_{i}\circledast_{i}0$ does not
hold for some $1\leqslant i\leqslant\ell$, where $\pi$ contains $q_{i}(x)$.

We are now ready for the final terminology which will be crucial when deciding
the satisfiability of $\Psi$.

Let $G$ be a graph and $H$ be a non-empty subgraph of $G$. We say that $H$ is
a good subgraph of $G$, if the following holds.

  * •

There is no bad vertex and bad edge in $H$ (w.r.t. the sentence $\Psi$).

  * •

It is symmetric in the sense that $(\pi,\eta,\pi^{\prime})$ is an edge in $H$
if and only if $(\pi^{\prime},\overline{\eta},\pi)$ is an edge in $H$.

Theorem 5 states that the satisfiability of $\Psi$ is equivalent to the
existence of a good subgraph in $G_{\Psi}$.

######  Theorem 5.

Let $\Psi$ be a $\textsf{GP}^{2}$ sentence in normal form (1). Then, $\Psi$ is
satisfiable if and only if there is a good subgraph in $G_{\Psi}$.

######  Proof 3.3.

(only if) Let $\mathcal{A}\models\Psi$. Let $H$ be the graph where the
vertices are the unary types realized in $\mathcal{A}$ and the edges are the
configurations realized in $\mathcal{A}$. Obviously, $H$ is symmetric and a
non-empty subgraph of $G_{\Psi}$ and that $\mathcal{A}$ conforms to $H$. It
remains to show that there is no bad edge and bad vertex in $H$.

Let $(\pi_{1},\eta,\pi_{2})$ be an edge in $H$. By definition, there is a pair
$(a,b)$ in $\mathcal{A}$ whose configuration is $(\pi_{1},\eta,\pi_{2})$.
Since $\mathcal{A}\models\Psi$, we have
$\mathcal{A},x/a\models\bigwedge_{i=1}^{\ell}q_{i}(x)\to\mathcal{P}_{i}(x)$.
By Lemma 4, the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{H}$ admits a
solution in $\mathbb{N}$, and hence, by definition, $(\pi_{1},\eta,\pi_{2})$
is not a bad edge in $H$.

Now, we prove that $H$ does not contain any bad vertex. Let $\pi$ be a vertex
in $H$ without any outgoing edge. By definition, there is an element $a$ in
$\mathcal{A}$ whose type is $\pi$. Since $\mathcal{A}$ conforms to $H$, for
every relation $R_{i,j}(x,y)$, we have:

$\big{|}R_{i,j}(x,y)\wedge x\neq y\big{|}^{x/a}_{\mathcal{A}}=0$

Since $\mathcal{A},x/a\models q_{i}(x)\to\mathcal{P}_{i}(x)$, for every
$1\leqslant i\leqslant\ell$, if $\pi$ contains $q_{i}(x)$, the constraint
$\mathcal{Q}_{i}^{H,\pi}$ admits the zero solution. Hence, $\pi$ is not a bad
vertex in $H$.

(if) Let $H=(V,E)$ be a good subgraph of $G_{\Psi}$. We will show how to
construct a model $\mathcal{A}\models\Psi$ that conforms to $H$. For each type
$\pi\in V$, we pick a set $A_{\pi}$ of infinitely many elements where for
every different $\pi,\pi^{\prime}\in V$, the sets $A_{\pi}$ and
$A_{\pi^{\prime}}$ are disjoint.

The domain of $\mathcal{A}$ is the set $A=\bigcup_{\pi\in V}A_{\pi}$. We will
define the interpretation of each relation symbol by setting the types of each
element $a\in A$ and each pair $(a,b)\in A\times A$. For unary types, we set
the type of each element in $A_{\pi}$ to be $\pi$ itself. The type of every
pair $(a,b)\in A\times A$ is defined such that the configuration of $(a,b)$ is
an edge in $H$, i.e., to ensure that $\mathcal{A}$ conforms to $H$. Note also
that a binary type $\eta$ uniquely determine its “reverse” $\overline{\eta}$.
So, when we define a binary type of $(a,b)$, we also define the type of
$(b,a)$.

$a_{1}$$\cdots\cdots\cdots\cdots\cdots\cdots\cdots$$a_{j-1}$$a_{j}$$\cdots\cdots\cdots\cdots\cdots\cdots\cdots$$a_{p_{j}}$$a_{p_{j}+1}$$a_{p_{j}+2}$$\cdots\cdots\cdots\cdots$The
binary types between elementsof these two sets are already defined to be the
null typeThe binary types betweenelements of these two setsare not yet
definedThe binary types between elementsof these two sets are already
definedand can be non-null type Figure 1. The relation between the sets
$\\{a_{1},\ldots,a_{j-1}\\}$, $\\{a_{j},\ldots,a_{p_{j}}\\}$ and
$\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$ before the $j^{\text{th}}$ iteration
starts. The finite sets $T_{\eta^{\prime},\pi^{\prime}}$’s used to define the
type of pairs involving $a_{j}$ are all subsets
$\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$.

We first enumerate all the elements in $A$ as $a_{1},a_{2},\ldots$. The
assignment of the binary types is done by iterating the following process
starting from $j=1$ to $j\to\infty$. Each index $j$ is associated with an
integer $p_{j}>j$ such that before the $j^{\text{th}}$ iteration starts, the
following invariant is satisfied:

  1. (1)

The binary types of pairs in
$\\{a_{1},\ldots,a_{j-1}\\}\times\\{a_{j},\ldots,a_{p_{j}}\\}$ are already
defined.

  2. (2)

The binary types of pairs in
$\\{a_{1},\ldots,a_{j-1}\\}\times\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$ are
already defined to be the null type.

  3. (3)

The binary types of pairs in
$\\{a_{j},\ldots,a_{p_{j}}\\}\times\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$ are
not defined yet.

  4. (4)

For every $a\in\\{a_{j},\ldots,a_{p_{j}}\\}$, there is at most one
$b\in\\{a_{1},\ldots,a_{j-1}\\}$ such that the binary type of $(a,b)$ is not
the null type.

  5. (5)

For every $a\in\\{a_{1},\ldots,a_{j-1}\\}$, the following already holds.

$\mathcal{A},x/a\models\bigwedge_{i=1}^{\ell}\ \big{(}q_{i}(x)\ \to\
\mathcal{P}_{i}(x)\big{)}$

Note that (e) makes sense since the binary type of every pair involving the
elements in $\\{a_{1},\ldots,a_{j-1}\\}$ is already defined. Figure 1
illustrates the relation between the sets $\\{a_{1},\ldots,a_{j-1}\\}$,
$\\{a_{j},\ldots,a_{p_{j}}\\}$ and $\\{a_{p_{j}+1},\ldots\\}$.

In the $j^{\text{th}}$ iteration, we set the binary types of each pair
$\\{a_{j}\\}\times\\{a_{j+1},a_{j+2},\ldots\\}$. First, we set the binary type
of each pair in $\\{a_{j}\\}\times\\{a_{j+1},\ldots,a_{p_{j}}\\}$ to be the
null type. Next, we show how to set the binary type of the pairs in
$\\{a_{j}\\}\times\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$. Let $\pi_{1}$ be the
type of $a_{j}$, i.e., $a_{j}\in A_{\pi_{1}}$. There are two cases.

Case 1: There is $h<j$ such that the type $(a_{j},a_{h})$ is defined as a non-
null type.

By (d), there is at most one such $h$. Let $\eta$ be the binary type of
$(a_{j},a_{h})$ and $\pi_{2}$ be the type of $a_{h}$. Since
$(\pi_{1},\eta,\pi_{2})$ is an edge in $H$, it is a good edge, i.e., the
system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{H}$ admits a solution in
$\mathbb{N}$. For every $\eta^{\prime},\pi^{\prime}$, let
$M_{\eta^{\prime},\pi^{\prime}}$ be the solution for the variable
$z_{\eta^{\prime},\pi^{\prime}}$. We fix a set
$T_{\eta^{\prime},\pi^{\prime}}\subseteq
A_{\pi^{\prime}}\cap\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$ such that:

$|T_{\eta^{\prime},\pi^{\prime}}|=\left\\{\begin{array}[]{ll}M_{\eta^{\prime},\pi^{\prime}}&\text{for}\
(\eta^{\prime},\pi^{\prime})\neq(\eta,\pi_{2})\\\
M_{\eta,\pi_{2}}-1&\end{array}\right.$

We also require that the sets $T_{\eta^{\prime},\pi^{\prime}}$’s to be
pairwise disjoint, which is possible since each $A_{\pi^{\prime}}$ is an
infinite set. Note that since $(\pi_{1},\eta,\pi_{2})$ is a good edge, by
definition, $M_{\eta,\pi_{2}}\geqslant 1$.

Now, for every $\eta^{\prime},\pi^{\prime}\in\mathcal{K}\times\Pi$, we set the
type of every pair in $\\{a_{j}\\}\times T_{\eta^{\prime},\pi^{\prime}}$ to be
$\eta^{\prime}$. For every element $c\in\\{a_{p_{j}+1},a_{p_{j}+2},\ldots\\}$,
where $c$ is not in any of $T_{\eta^{\prime},\pi^{\prime}}$, we set the type
of $(a_{j},c)$ to be the null type. Finally, we set $p_{j+1}$ to be the
maximal index of the elements in any of the sets
$T_{\eta^{\prime},\pi^{\prime}}$’s.

It is obvious that invariant (a)–(c) still holds after the $j^{\text{th}}$
iteration. Invariant (d) holds, since the sets
$T_{\eta^{\prime},\pi^{\prime}}$’s are pairwise disjoint. That invariant (e)
holds, i.e.,
$\mathcal{A},x/a_{j}\models\bigwedge_{i=1}^{\ell}(q_{i}(x)\to\mathcal{P}_{i}(x))$,
follows from the fact that
$z_{\eta^{\prime},\pi^{\prime}}=M_{\eta^{\prime},\pi^{\prime}}$ is a solution
for the system $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{H}$.

Case 2: For every $h<j$, the type $(a_{j},a_{h})$ is defined as the null type.

In this case, we pick an arbitrary edge $(\pi_{1},\eta,\pi_{2})$ in $H$. Since
it is a good edge, we consider a solution
$z_{\eta^{\prime},\pi^{\prime}}=M_{\eta^{\prime},\pi^{\prime}}$ for the system
$\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}$. Then, for every
$\eta^{\prime},\pi^{\prime}$, we define the set
$T_{\eta^{\prime},\pi^{\prime}}\subseteq A_{\pi^{\prime}}$ in similar manner
as Case 1, except that
$|T_{\eta^{\prime},\pi^{\prime}}|=M_{\eta^{\prime},\pi^{\prime}}$, for every
$\eta^{\prime},\pi^{\prime}$. Setting the binary types of the pairs involving
the element $a_{j}$ is done exactly as in case 1. That the invariant (a)–(e)
still holds also follows in a straightforward manner. This ends the
construction for case 2.

Coming back to the proof of Theorem 5, as $j\to\infty$, the binary type of
every pair is well defined and due to invariant (e), we have
$\mathcal{A}\models\bigwedge_{i=1}^{\ell}\forall x\ \big{(}q_{i}(x)\ \to\
\mathcal{P}_{i}(x)\big{)}$. Since $\mathcal{A}$ conforms to $H$ and $H$ is a
subgraph of $G_{\Psi}$, it follows that $\mathcal{A}\models\Psi$. This
completes the proof of Theorem 5.

###  3.3. The algorithm

Theorem 5 tells us that to decide if $\Psi$ is satisfiable, it suffices to
find if $G_{\Psi}$ contains a good subgraph. It can be done as follows. First,
construct the graph $G_{\Psi}$. Then, repeatedly delete the bad edges and bad
vertices from the graph $G_{\Psi}$. It stops when there is no more bad
edge/vertex to delete. If the graph ends up not containing any vertices, then
$\Psi$ is not satisfiable. If the graph still contains some vertices, then it
is a good subgraph of $G_{\Psi}$ and $\Psi$ is satisfiable. Its formal
presentation can be found in Algorithm 3.3. It is worth noting that deleting a
bad edge may yield a new bad edge, hence the while-loop.

0: A sentence $\Psi$ in normal form (1).

0: Accept if and only if $\Psi$ is satisfiable.

1: $G:=G_{\Psi}$.

2: while $G$ has a bad edge do

3: Delete the bad edge and its inverse from $G$.

4: Delete all bad vertices (if there is any) from $G$.

5: ACCEPT if and only if $G$ is not an empty graph.

###  3.4. The complexity analysis of Algorithm 3.3

To prove Algorithm 3.3 runs in exponential time in the worst case scenario, we
will need the following two results from [ES06, Pap81].

######  Theorem 6.

[ES06, Theorem 1] Let $A$ be an integer matrix with size $d\times t$ and let
$\bar{b}$ be an integer column vector with size $d$. If the linear system
$A\bar{x}=\bar{b}$ has a solution in $\mathbb{N}$, then it has a solution in
$\mathbb{N}$ in which the number of non-zero entries is bounded by
$2d\log_{2}(4dM)$ where $M$ is the maximal absolute value of the entries in
$A$ and $\bar{b}$.

######  Theorem 7.

[Pap81, Theorem] Let $A$ be an integer matrix with size $d\times t$ and let
$\bar{b}$ be an integer column vector with size $d$. If the linear system
$A\bar{x}=\bar{b}$ has a solution in $\mathbb{N}$, then it has a solution in
$\mathbb{N}$ in which every entry is bounded by $t(dM)^{2d+1}$ where $M$ is
the maximal absolute value of the entries in $A$ and $\bar{b}$.

To proceed with the analysis, we first show that checking whether the system
$\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ admits a solution in $\mathbb{N}$ can
be done in exponential time in the length of the input $\Psi$.

######  Lemma 8.

For every edge $(\pi_{1},\eta,\pi_{2})$ in $G$, checking whether the system
$\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ admits a solution in $\mathbb{N}$
takes exponential time (in the worst case) in the length of the input
sentence.

######  Proof 3.4.

Let $\Psi$ be the input sentence in the normal form (1). Let $n$ and $m$ be
the number of unary and binary relation symbols in $\Psi$. Thus, there are
$2^{n+m}$ unary types and $2^{2m}$ binary types. (Recall that we consider
atomic $R(x,x)$ as a unary predicate.) Note that
$\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ contains at most $\ell+1$ constraints
and $2^{n+3m}$ variables. Moreover, it can be rewritten in matrix form
$A\bar{x}=\bar{b}$ where $A$ has $d=O(\ell)$ rows and $O(2^{n+3m})$ columns.
Let $M$ be the maximal absolute value of the entries in $A$ and $b$.

By Theorem 6, to check if $A\bar{x}=\bar{b}$ has a solution in $\mathbb{N}$,
it suffices to search only for the solutions in which the number of non-zero
entries is at most $2d\log_{2}(4dM)$. Moreover, by Theorem 7, it suffices to
search only for the solutions whose entries are bounded by $t(dM)^{2d+1}$.
This gives us a (deterministic) exponential time upper bound (in the length of
$\Psi$) for checking whether $\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ admits a
solution in $\mathbb{N}$.

Finally, we show that Algorithm 3.3 runs in exponential time, which
establishes that $\text{SAT}(\textsf{GP}^{2})$ is in the class EXP.

######  Theorem 9.

Algorithm 3.3 runs in exponential time in the length of the input sentence.

######  Proof 3.5.

Let $\Psi$ be the input sentence in the normal form (1). Let $n$ and $m$ be
the number of unary and binary relation symbols in $\Psi$. Thus, $G_{\Psi}$
has at most $2^{2n+4m}$ edges which bounds the the number of iterations of the
while-loop in Algorithm 3.3. Checking whether an edge is a bad edge is
equivalent to checking whether the system
$\mathcal{Z}_{\pi_{1},\eta,\pi_{2}}^{G}$ admits a solution in $\mathbb{N}$,
which by Lemma 8, takes exponential time in the length of $\Psi$. Therefore,
Algorithm 3.3 runs in exponential time in the length $\Psi$.

Note that Algorithm 3.3 can be easily implemented using available solvers for
Presburger arithmetic as a black box. See, e.g., [ome23, pri22]. The following
straightforward corollary establishes an upper bound for the number of times
such solvers being called by Algorithm 3.3.

######  Corollary 10.

Algorithm 3.3 can be implemented using a quantifier-free Presburger arithmetic
solver as a black box and the number of calls to such solver is bounded by
$2^{4n+8m}$, where $n$ and $m$ is the number of unary and binary predicates
appearing in the input sentence.

######  Proof 3.6.

In each iteration we check whether each edge is a bad edge. Since the graph
$G_{\Psi}$ has at most $2^{2n+4m}$ edges, there is at most $2^{2n+4m}$ number
of calls to the Presburger arithmetic solver. After each iteration there is at
most one less edge. Therefore, the $2^{4n+8m}$ upper bound follows
immediately.

###  3.5. Local Presburger quantifiers with $\infty$ semantics

In Section 2 we define the the semantics of LP quantifiers in the structure
$\mathbb{N}$. One can easily extend it to the structure
$\mathbb{N}\cup\\{\infty\\}$ in which the operations involving $\infty$ are
defined as follows.

  * •

$\infty+\infty=\infty+a=a+\infty=\infty$, for every $a\in\mathbb{N}$.

  * •

$a\leqslant\infty$, for every $a\in\mathbb{N}$.

  * •

For every $a,b\in\mathbb{N}\cup\\{\infty\\}$, for every $d\in\mathbb{N}$,
$a\equiv_{d}b$ if and only if there is $c\in\mathbb{Z}$ such that $a=b+cd$. In
particular, $\infty\equiv_{d}\infty$, but $\infty\not\equiv_{d}a$, for every
$a\in\mathbb{N}$.

For such semantics to make sense, we need to insist that the LP quantifiers
are of the form:

$\delta\ +\ \sum_{i=1}^{n}\
\lambda_{i}\cdot\\#_{y}^{r_{i}}[\varphi_{i}(x,y)]\qquad\circledast\qquad\sum_{i=1}^{m}\
\kappa_{i}\cdot\\#_{y}^{s_{i}}[\psi_{i}(x,y)]$

where the coefficients $\delta,\lambda_{i},\kappa_{i}$ are all positive
integers or $\infty$.

Note that a set of LP quantifiers of this form can be rewritten into a system
of linear equations of the form:
$A\bar{x}=\bar{b}+A^{\prime}\bar{x}^{\prime}$, where each entry in
$A,A^{\prime}$ and $\bar{b}$ comes from $\mathbb{N}\cup\\{\infty\\}$. Checking
whether it is satisfiable in $\mathbb{N}\cup\\{\infty\\}$ can easily be
reduced to the case in $\mathbb{N}$. Indeed, we can first guess which
variables take the value $\infty$ and check which row must evaluate to
$\infty$. Then, we can check whether the other rows can be satisfied in the
standard $\mathbb{N}$. It is routine to verify that such procedure takes
exponential time in the length of $A,A^{\prime}$ and $\bar{b}$. By Corollary
10, $\text{SAT}(\textsf{GP}^{2})$ is in EXP when the semantics is defined over
$\mathbb{N}\cup\\{\infty\\}$.

###  3.6. Comparison with the approach in [BF22]

An alternating polynomial space algorithm was proposed in [BF22] for deciding
the satisfiability of $\textsf{GP}^{2}$ sentences.333It is well known that the
class of languages decidable by alternating polynomial space Turing machines
is equivalent to the class of languages decidable by deterministic exponential
time Turing machines [CKS81].

Intuitively, it tries to build a tree-like model that satisfies the input
sentence (if satisfiable). It starts by guessing the unary type of of the root
node and all the unary types of its children as well as the binary types of
the edges connecting them. Using Theorems 6 and 7, the number of different
unary types of the children is polynomially bounded (in the length of the
input sentence).444Note that the bound only holds for the number of unary
types of the children, not the number of children itself which can be
exponential. It verifies that the LP quantifiers are satisfied by guessing a
solution that respects the guessed binary types of the edges connecting the
root nodes and the children. The amount of guessing makes it not trivial to
use available Presburger solvers as a black box, compared with our
straightforward Algorithm 3.3.

##  4\. Concluding remarks

In this paper we consider the extension of $\textsf{GF}^{2}$ with the local
Presburger quantifiers which can express rich Presburger constraints while
maintaining deterministic exponential time upper bound. It captures various
natural DL with counting up to $\mathcal{ALCIH}b^{\textsf{self}}$ and
$\mathcal{ALCIHQ}$ without constant symbols. The proof is via a novel, yet
simple and optimal algorithm, which is a reminiscent of type-elimination
approach.

We note that the proof of Theorem 5 relies on the infinity of the model. We
leave a similar characterization for the finite models for future work. It is
worth noting that the finite satisfiability of $\textsf{GP}^{2}$ has been
shown to be decidable in 3-NEXP [BOPT21], though the precise complexity is
still not known.

## Acknowledgment

We thank Bartosz Bednarczyk for his comments on the preliminary drafts of this
work. We acknowledge generous financial support of Taiwan Ministry of Science
and Technology under grant no. 109-2221-E-002-143-MY3.

## References

  * [ANvB98] H. Andréka, I. Németi, and J. van Benthem.  Modal languages and bounded fragments of predicate logic.  J. Philos. Log., 27(3):217–274, 1998.
  * [Baa17] F. Baader.  A new description logic with set constraints and cardinality constraints on role successors.  In FroCoS, 2017.
  * [BBR20] F. Baader, B. Bednarczyk, and S. Rudolph.  Satisfiability and query answering in description logics with global and local cardinality constraints.  In ECAI, 2020.
  * [BCM+03] F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. Patel-Schneider, editors.  The Description Logic Handbook: Theory, Implementation, and Applications.  Cambridge University Press, 2003.
  * [Bed20] B. Bednarczyk.  One-variable logic meets presburger arithmetic.  Theor. Comput. Sci., 802:141–146, 2020.
  * [BF22] B. Bednarczyk and O. Fiuk.  Presburger büchi tree automata with applications to logics with expressive counting.  In WoLLIC, 2022.
  * [BHLS17] F. Baader, I. Horrocks, C. Lutz, and U. Sattler.  An Introduction to Description Logic.  Cambridge University Press, 2017.
  * [BKT20] M. Benedikt, E. Kostylev, and T. Tan.  Two variable logic with ultimately periodic counting.  In ICALP, 2020.
  * [BOPT21] B. Bednarczyk, M. Orlowska, A. Pacanowska, and T. Tan.  On classical decidable logics extended with percentage quantifiers and arithmetics.  In FSTTCS, 2021.
  * [CKS81] A. Chandra, D. Kozen, and L. Stockmeyer.  Alternation.  J. ACM, 28(1):114–133, 1981.
  * [DL10] S. Demri and D. Lugiez.  Complexity of modal logics with presburger constraints.  J. Appl. Log., 2010.
  * [ES06] F. Eisenbrand and G. Shmonin.  Carathéodory bounds for integer cones.  Oper. Res. Lett., 34(5):564–568, 2006.
  * [GKV97] E. Grädel, P. Kolaitis, and M. Vardi.  On the decision problem for two-variable first-order logic.  Bull. Symbolic Logic, 3(1):53–69, 03 1997.
  * [Grä98] E. Grädel.  Description logics and guarded fragments of first order logic.  In DL, 1998.
  * [Grä99] E. Grädel.  On the restraining power of guards.  J. Symb. Log., 64(4):1719–1742, 1999.
  * [Kaz04] Y. Kazakov.  A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment.  In JELIA, 2004.
  * [KP10] C. Kupke and D. Pattinson.  On modal logics of linear inequalities.  In AiML, 2010.
  * [KT15] E. Kopczynski and T. Tan.  Regular graphs and the spectra of two-variable logic with counting.  SIAM J. Comput., 44(3):786–818, 2015.
  * [LLT21] T. Lin, C. Lu, and T. Tan.  Towards a more efficient approach for the satisfiability of two-variable logic.  In LICS, 2021.
  * [ome23] Omega: a solver for quantifier-free problems in Presburger Arithmetic, 2023\.  URL: https://coq.github.io/doc/v8.9/refman/addendum/omega.html.
  * [Pap81] C. Papadimitriou.  On the complexity of integer programming.  J. ACM, 28(4):765–768, 1981.
  * [Pra79] V. R. Pratt.  Models of program logics.  In FOCS, 1979.
  * [Pra05] I. Pratt-Hartmann.  Complexity of the two-variable fragment with counting quantifiers.  Journal of Logic, Language and Information, 14(3):369–395, 2005\.
  * [Pra07] I. Pratt-Hartmann.  Complexity of the guarded two-variable fragment with counting quantifiers.  J. Log. Comput., 17(1):133–155, 2007.
  * [pri22] Princess – The Scala Theorem Prover, 2022.  URL: http://www.philipp.ruemmer.org/princess.shtml.
  * [Tob01] S. Tobies.  Complexity results and practical algorithms for logics in knowledge representation.  PhD thesis, RWTH Aachen University, Germany, 2001.
  * [Var96] M. Vardi.  Why is modal logic so robustly decidable?  In DIMACS Workshop, 1996.