On guarded extensions of MMSNP
This work was supported by ANR project DIFFERENCE (<https://anr.fr/Projet-ANR-20-CE48-0002>).

Alexey Barsukov1,20000-0001-7627-4823
Florent R. Madelaine10000-0002-8528-7105

A. Barsukov and F. Madelaine

Université Paris-Est Créteil, France
Charles University, Czech Republic

We investigate logics and classes of problems below Fagin's existential second-order logic ($\ESO$) and above Feder and Vardi's logic for constraint satisfaction problems ($\CSP$), the so called monotone monadic $\SNP$ without inequality ($\MMSNP$).
It is known that $\MMSNP$ has a dichotomy between $\P$
and $\NPc$ but that the removal of any of these three restrictions
imposed on $\SNP$ yields a logic that is $\P$time equivalent to
$\ESO$: so by Ladner's theorem we have three stronger sibling logics that are nondichotomic above $\MMSNP$.
In this paper, we explore the area between these four logics, mostly
by considering guarded extensions of $\MMSNP$, with the ultimate goal
being to obtain logics above $\MMSNP$ that exhibit such a dichotomy.

§ INTRODUCTION

A consequence of Ladner's theorem <cit.> is that if $\P\not=\NP$, then $\NP$ does not have a $\P\text{vs}\NPc$ dichotomy.
Feder and Vardi proved in <cit.> that $\MMSNP$ captures
$\CSP$ up to $\P$time equivalence and that its three stronger siblings
do not have a dichotomy, and conjectured the dichotomy of $\CSP$; a conjecture
proved independently by Bulatov and Zhuk in <cit.>.
The classes studied in this paper are depicted on <Ref>, where
an arrow from a class $\family{C}_1$ to a class $\family{C}_2$ indicates that any problem from
$\family{C}_1$ is $\P$time equivalent to a problem from $\family{C}_2$. This means that if $\family{C}_2$ has
a dichotomy, then so does $\family{C}_1$.
In <cit.>, Bienvenu introduced $\GMSNP$ a guarded
extension of $\MMSNP$ that relaxes the constraint of monadicity, and showed
that it is logically equivalent to $\MMSNPtwo$ <cit.> an
extension of $\MMSNP$ which colors edges in the spirit of Courcelle's $\mathsf{MSO}_2$.

Regarding the constraint of monotonicity, there is no logic in the literature that sits between $\MMSNP$ and monadic $\SNP$ without $\neq$.
There is, however, an extension of $\CSP$ on graphs, the so called Matrix Partition problems <cit.>, studied on relational structures in <cit.>.

Classes at the bottom exhibit a $\P$vs$\NPc$ dichotomy, while
those at the  top do not, and it remains open for classes in the

Main contributions.
In <Ref>, we introduce the guarded extension of $\MMSNP$ with $\neq$
($\GMMSNPineq$) and prove that it exhibits a dichotomy. In this paper, $\Sat(\Phi)$ denotes the set of finite structures that satisfy a sentence $\Phi$.

For any sentence $\Phi$ in $\GMMSNPineq$ there exists a sentence $\Phi'$ in $\MMSNP$ such that the problems $\Sat(\Phi)$ and $\Sat(\Phi')$ are $\P$time equivalent.

While we are not able to do the same for $\GMSNP$, we establish that
it would suffice to prove a dichotomy for a signature with a single
input relation in <Ref>.

For any finite relational signature $\tau$ there exists a signature $\tau_1$ consisting of a single relational symbol such that, for any $\GMSNP$ $\tau$-sentence $\Phi$ there exists a $\GMSNP$ $\tau_1$-sentence $\Phi^1$ such that $\Sat(\Phi)$ and $\Sat(\Phi^1)$ are $\P$time equivalent.

We recall Hell's Matrix Partition <cit.>, a graph problem
which we recast as a problem on arbitrary relational structure, for
which we propose a logic in <Ref>.

Finally, in <Ref>, we provide a complete proof of one crucial step of Feder
and Vardi's argument to establish that the three stronger siblings of
$\MMSNP$ can not have a dichotomy unless $\P$ equals $\NP$. The
original argument provides key ideas, in particular using oblivious
Turing machines, but to the best of our knowledge, nobody in the
community has reconstructed a complete proof from their argument,
which motivates us to do it here.

For each problem $\Omega$ in $\NP$ there is a sentence $\Phi$ in $\MMSNPineq$ such that $\Omega$ and $\Sat(\Phi)$ are $\P$time equivalent.

The interested reader may consult <cit.> for extensive
proofs regarding the two other logics.

Full proofs for statements marked with $\star$ can be found in the appendix.

§ PRELIMINARIES

Denote by $\tau$ a relational signature.
A $\tau$-sentence is in strict $\NP$ ($\SNP$) if it is of the form

\begin{equation*}
\exists  \rel{X}_1,\ldots,  \rel{X}_s \; \forall x_1,\ldots,x_n \; \phi(x_1,\ldots,x_n),
\end{equation*}
where $\phi(x_1,\ldots,x_n)$ is a quantifier-free first-order formula.

Denote the set of existentially quantified second-order variables $\{ \rel{X}_1,\ldots,  \rel{X}_s\}$ by $\sigma$.
Relation symbols of $\tau$ are called input and relation symbols of $\sigma$ are called existential. Also, tuples of first-order variables or elements are denoted with bold lower-case letters: $\tuple{x},\tuple{a},\dots$

Any $\tau$-sentence $\Phi$ in $\SNP$ can be rewritten in the following form:

\begin{equation}\label{eq:negated_cnf}
\exists \rel{X}_1,\ldots,  \rel{X}_s\;\forall\tuple{x} \; \bigwedge_i \neg (\alpha_i\wedge\beta_i\wedge \epsilon_i),
\end{equation}

where $\alpha_i$ is a conjunction of atomic or negated atomic $\tau$-formulas, $\beta_i$ is a conjunction of atomic or negated atomic $\sigma$-formulas, and $\epsilon_i$ is a conjunction of inequalities $x_i\not=x_j$, for some $x_i,x_j\in\tuple{x}$.
We frequently write “atom” instead of “atomic formula”.
Every subformula $\neg (\alpha_i\wedge\beta_i\wedge\epsilon_i)$ is
called a negated conjunct.

An $\SNP$-sentence $\Phi$ is called monadic if all existential relation symbols have arity $1$.
It is called monotone if every $\alpha_i$ omits negated $\tau$-atoms.
Alternatively, one can think of this property as of being closed under
inverse homomorphisms, thanks to the following theorem.

For a sentence $\Phi$ in $\SNP$, the class $\Sat(\Phi)$ is closed under inverse homomorphisms iff $\Phi$ is logically equivalent to a monotone sentence.

Denote by $\MMSNP$ the fragment of $\SNP$ consisting of sentences that are monotone, monadic, and without inequality, , every $\epsilon_i$ is empty.

A sentence $\Phi$ is in guarded monotone strict NP($\GMSNP$) if it is written in the form of <ref>, where:

* each $\alpha_i$ is a conjunction of nonnegated $\tau$-atoms,

* each $\beta_i$ is a conjunction of $\sigma$-atoms or negated $\sigma$-atoms, and

* each $\epsilon_i$ is empty.

Also, for every negated $\sigma$-atom $\neg \rel{X}(\tuple{x}_1)$ from every $\beta_i$ there exists either

* a $\tau$-atom $\rel{R}(\tuple{x}_2)$ from $\alpha_i$, or

* a nonnegated $\sigma$-atom $\rel{X}'(\tuple{x}_2)$ from $\beta_i$

such that $\tuple{x}_1\subseteq\tuple{x}_2$.
In this case, we say that $\rel{R}(\tuple{x}_2)$ (or $\rel{X}'(\tuple{x}_2)$) guards $\rel{X}(\tuple{x}_1)$.

The logic $\MMSNP$ with guarded $\neq$, denoted by $\GMMSNPineq$, is the class of sentences of the form as in <ref>, where

* each $\alpha_i$ is a conjunction of nonnegated $\tau$-atoms,

* each $\beta_i$ is a conjunction of unary $\sigma$-atoms or negated unary $\sigma$-atoms, and

* for every inequality $x_j\not=x_j'$ of each $\epsilon_i$ there exists a $\tau$-atom in $\alpha_i$ that contains both $x_j$ and $x_j'$.

For any sentence that we consider, we assume that it is not trivial, , it has some YES and some  NO input instances.

For further notions that remain undefined please refer to <cit.>.

§ MMSNP WITH GUARDED INEQUALITY

In this section, we prove <Ref>, for the sake
of simplicity in the case of $\tau = \{\rel{R}\}$, where $\rel{R}$ has
arity $n$. In the case of many relations, one should apply the same procedure for each relation independently.

The construction has two main steps.
At first, we enrich every negated conjunct of $\Phi$ with inequalities and keep the resulting sentence logically equivalent to the initial one.
This transformation is the same as the one used in Lemma 4 in <cit.>.

After that, we construct an equivalent $\MMSNP$ sentence $\Phi'$ by changing the input relational signature.
Each new relation symbol is associated with an equivalence relation on an $n$-element set, where $n$ is the arity of $\rel{R}$.

Enriching the sentence with inequalities. For every negated conjunct $\neg\phi$ of  $\Phi$ and for every two variables $x,y$ that appear in the same $\rel{R}$-atom of $\neg\phi$,  replace this negated conjunct with two negated conjuncts: the first one is obtained from $\neg\phi$ by adding the inequality $x\not=y$ to the conjunction, the second one is obtained from $\neg\phi$ by replacing every occurrence of the variable $y$ with the variable $x$.

If $\Phi$ contains a negated conjunct $\neg\bigl(\rel{R}(x,y)\wedge\rel{X}_1(x)\wedge\rel{X}_2(y)\bigr)$, then it is replaced by the two following negated conjuncts:

\begin{equation*}
\neg\bigl(\rel{R}(x,y)\wedge\rel{X}_1(x)\wedge\rel{X}_2(y)\wedge x\not=y\bigr)\wedge \neg\bigl(\rel{R}(x,x)\wedge\rel{X}_1(x)\wedge\rel{X}_2(x)\bigr).
\end{equation*}

The following lemma is a direct implication from the construction.

Any $\GMMSNPineq$ sentence $\Phi$ is logically equivalent to a $\GMMSNPineq$ sentence $\Psi$ such that, for any negated conjunct $\neg\psi_i$ of $\Psi$ and for any two different variables $x,y$ that appear within some $\rel{R}$-atom of $\psi_i$, this conjunct contains the inequality $x\not=y$.

Let $\Phi$ and $\Psi$ be as in the paragraph above <Ref>, and  $\structure{A}$ be a $\tau$-structure.
Suppose that $\structure{A}\not\models\Phi$; then for any $\sigma$-expansion there exists a negated conjunct $\neg\phi_i$ of $\Phi$ that is false for some assignment of elements of $A$ to the conjunct variables.
Among the negated conjuncts of $\Psi$ that are obtained from $\phi_i$ we choose the one that is associated with this assignment: if two variables $x,y$ of $\phi$ have the same element $a$ in $ A$ assigned to them, then $x$ and $y$ must be identified in the corresponding conjunct of $\Psi$; if two different elements $a,a'$ in $ A$ are assigned to $x$ and $y$, then the corresponding conjunct of $\Psi$ must contain the inequality $x\not=y$.
By the construction of $\Psi$, such a conjunct exists.
If $\structure{A}\not\models\Psi$, then for any $\sigma$-expansion there is a negated conjunct of $\Psi$ that is false for some assignment.
It is associated with some negated conjunct $\neg\phi_i$ of $\Phi$, and, by construction, $\phi_i$ is also false for the same assignment.
We conclude that $\structure{A}\models\Phi\longleftrightarrow\structure{A}\models\Psi$, for any $\tau$-structure $\structure{A}$.

Now, by <Ref>, we assume that for any two variables $x,y$ that appear within the same $\rel{R}$-atom in some negated conjunct of $\Phi$, this negated conjunct contains $x\not=y$.

We need to introduce some necessary notations. For $n$ in $\mathbb{N}$, denote by $B_n$ the number of equivalence relations on a set of $n$ elements: $\sim_1,\ldots,\sim_{B_n}$. For each $\sim_k$, denote by $n_k:=\bigl|\{1,\ldots,n\}/\sim_k\bigr|$ the number of equivalence classes of this relation.
Every $n$-tuple $(x_1,\ldots,x_n)$ is associated with exactly one $\sim_k$ such that $x_i=x_j$ iff $i\sim_k j$.
If $\sim_k$ is associated with $\tuple{x}$, then we say that $\tuple{x}$ has equivalence type $k$.
For every equivalence class $\{x_{c_1},\ldots, x_{c_l}\}$ of $\sim_k$, denote it by $[c]_{\sim_k}$, where $c = \min\{c_1,\ldots,c_l\}$ – the smallest number of this set.
Then, introduce a linear ordering $\prec_k$ on the set $\{1,\ldots,n\}/\sim_k$ by setting $[i]_{\sim_k}\prec_k [j]_{\sim_k}$ if $i<j$.

For a set $X$, define a function $\func{p}\colon \biguplus_{n=1}^\infty X^n \to \biguplus_{n=1}^\infty X^n$ as follows.
Let $\tuple{x}=(x_1,\ldots,x_n)$ in $ X^n$ be an $n$-tuple of equivalence type $k$.
Let $[s_1]_{\sim_k},\ldots,[s_{n_k}]_{\sim_k}$ be the $\sim_k$-equivalence classes such that $[s_i]_{\sim_k}\prec_k[s_j]_{\sim_k}$ iff $i<j$.
Then, put $\func{p}(\tuple{x}):= \bigl(x_{s_1},\ldots,x_{s_{n_k}}\bigr)$.

Informally, the function $\func{p}$ removes an element from a tuple if it is not its first occurrence.
Consider a $3$-tuple $\tuple{t} = (y,x,x)$, it is associated with the equivalence relation $\sim_4$ from <Ref>, the equivalence classes of $\sim_4$ on the set $\{1,2,3\}$ are $[1]_{\sim_4}=\{1\}$ and $[2]_{\sim_4} = \{2,3\}$.
Then, $\func{p}(\tuple{t})=(y,x)$ because $y$ is on the first coordinate of $\tuple{t}$, $x$ is on the second, and $[1]_{\sim_4}\prec_4[2]_{\sim_4}$.

All the 5 equivalence relations on a $3$-element set.

Constructing the $\MMSNP$ sentence.
The $\MMSNP$ sentence $\Phi'$ has the same existential signature $\sigma$ as $\Phi$, however the input signature $\tau'$ is not the same.
$\tau'$ has $B_n$ relation symbols $\rel{R}_1,\ldots,\rel{R}_{B_n}$.
Each $\rel{R}_i$ is associated with one of the $B_n$ equivalence relations $\sim_k$ on the set $\{1,\ldots,n\}$, the arity of $\rel{R}_k$ equals to the number $n_k$ of equivalence classes of $\sim_k$. For example, if $n=3$, then $\tau'$ contains $B_3=5$ relation symbols $\rel{R}_1(\cdot,\cdot,\cdot), \rel{R}_2(\cdot,\cdot), \rel{R}_3(\cdot,\cdot), \rel{R}_4(\cdot,\cdot), \rel{R}_5(\cdot)$, see <Ref>.
We now describe how to construct the $\MMSNP$ sentence $\Phi'$ from $\Phi$.

* Firstly, remove all inequalities from $\Phi$.

* Then, replace every $\tau$-atom $\rel{R}(\tuple{x})$ with $\rel{R}_k\bigl(\func{p}(\tuple{x})\bigr)$, where $k$ is the equivalence type of $\tuple{x}$.

* Finally, in order to mimic the inequalities that we have removed, we forbid the same variable to appear within $\tau'$-atoms more than once. For every $\rel{R}_k$ in $\tau'$ and for every $i<j$ in $[n_k]$, add to $\Phi'$ the following:

\begin{equation}\label{eq:negated_conjunct_rigid}
\neg\rel{R}_k(x_1,\ldots,x_{i-1},x,x_{i+1},\ldots,x_{j-1},x,x_{j+1},\ldots,x_{n_k}).
\end{equation}

Let $\Phi'$ be obtained from $\Phi$ as above.
Let $\structure{A}$ be a $\tau$-structure.
The corresponding $\tau'$-structure $\structure{A}'$ has the same domain $A'=A$.
And, for every $\rel{R}_k$ in $\tau'$ and for every tuple $\tuple{a} = (a_1,\ldots,a_n)$ of equivalence type $k$:

\begin{equation}\label{eq:construction_of_adash}
\rel{R}_k^{\structure{A}'}\bigl(\func{p}(\tuple{a})\bigr) \longleftrightarrow \rel{R}^\structure{A}(\tuple{a}).
\end{equation}

For an arbitrary $\tau'$-structure there exists a $\tau$-structure $\structure{A}$ satisfying <ref> iff all conditions of the type from <ref> hold.
Otherwise, such a structure does not satisfy $\Phi'$, and we can output a fixed NO instance of $\Phi$.

By construction, $\structure{A}'$ satisfies every negated conjunct from <ref>.
Let $\structure{A}^\sigma$ and $\structure{A}'^\sigma$ be $\sigma$-expansions such that, for any $\rel{X}$ in $\sigma$ and $a$ in $ A$,  $\rel{X}^{\structure{A}^\sigma}=\rel{X}^{\structure{A}'^\sigma}$.

Suppose $\structure{A}^\sigma$ does not satisfy the first-order part of $\Phi$; then, for some negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and some elements $\tuple{a}_i$ of $A$, $\structure{A}^\sigma\models\phi_i(\tuple{a}_i)$. For any $\sigma$-atom $\rel{X}(a)$ of $\phi_i(\tuple{a}_i)$, $\structure{A}^\sigma\models\rel{X}(a)$, but then $\structure{A}'^\sigma\models\rel{X}(a)$. For any $\tau$-atom $\rel{R}(\tuple{a})$ of $\phi_i(\tuple{a}_i)$, $\structure{A}^\sigma\models\rel{R}(\tuple{a})$, but then $\structure{A}'^\sigma\models\rel{R}_k\bigl(\func{p}(\tuple{a})\bigr)$, by <ref>.
Thus, $\structure{A}'^\sigma\models\phi_i'(\tuple{a}_i)$.
The other direction is similar.

§ GUARDED MONOTONE SNP

In this section, we prove <Ref> in several stages.
In the first one, we check if $\Phi$ holds in a structure consisting of a
single $\rel{R}$-tuple, for $\rel{R}$ in $\tau$. If not, then we get
rid of this relation symbol because we need every relation of an input
structure to be allowed to be nonempty.
In the second one, we enrich every negated conjunct with $\tau$-atoms so that every relation symbol of $\tau$ is present in every conjunct.
In the last stage, we construct a suitable sentence over a single relation symbol.

An $\SNP$ $\tau$-sentence $\Phi$ of the form as in <ref> is called connected if no negated conjunct $\neg \phi(\tuple{x})$ of $\Phi$ can be written as $\neg\bigl(\psi_1(\tuple{x}_1)\wedge\psi_2(\tuple{x}_2)\bigr)$, where $\tuple{x}_1$ and $\tuple{x}_2$ share no variables.
By <Ref>, we can consider only connected $\tau$-sentences $\Phi$ in $\GMSNP$ and, by <Ref>, $\Sat(\Phi)$ is closed under disjoint unions.

The following statements are equivalent.

* For any $\tau$-sentence $\Phi$ in $\GMSNP$, $\Sat(\Phi)$ is in $\P\cup\NPc$.

* For any connected $\tau$-sentence $\Phi$ in $\GMSNP$, $\Sat(\Phi)$ is in $\P\cup\NPc$.

Let $\Phi$ be an $\SNP$ sentence.
Then, $\Sat(\Phi)$ is closed under disjoint unions iff $\Phi$ is logically equivalent to a connected $\SNP$ sentence.

First stage: removing unnecessary relation symbols.
For a $k$-ary $\rel{R}$ in $\tau$, let $\structure{B}_\rel{R}$ be a $\tau$-structure that consists of one $\rel{R}$-tuple $\tuple{b}_\rel{R} = (b_{\rel{R},1},\ldots,b_{\rel{R},k})$. That is, (a) $\structure{B}_\rel{R}$ has the domain $B_\rel{R}=\{b_{\rel{R},1},\ldots,b_{\rel{R},k}\}$, (b) $\rel{R}^{\structure{B}_\rel{R}}=\{\tuple{b}_\rel{R}\}$, and (c) for any other $\rel{S}\in\tau$, $\rel{S}^{\structure{B}_\rel{R}}=\varnothing$.

If, for some $\rel{R}$ in $\tau$, a connected $\GMSNP$ $\tau$-sentence $\Phi$ does not satisfy $\structure{B}_\rel{R}$, then $\Sat(\Phi)$ is $\P$time equivalent to $\Sat(\Phi^{\cancel{\rel{R}}})$, where $\Phi^{\cancel{\rel{R}}}$ is a connected $(\tau\setminus\{\rel{R}\})$-sentence that is obtained from $\Phi$ by removing all negated conjuncts that contain an $\rel{R}$-atom.

Suppose that $\structure{B}_\rel{R}\not\models\Phi$.
Let a $\tau$-structure $\structure{A}$ be an input instance of $\Sat(\Phi)$.
If $\rel{R}^\structure{A}\not=\varnothing$, then $\structure{B}_\rel{R}\to\structure{A}$, so, by <Ref>, $\structure{A}\not\models\Phi$, and we reduce it to some NO instance of $\Sat(\Phi^{\cancel{\rel{R}}})$.
Suppose that $\rel{R}^\structure{A}=\varnothing$; then we reduce $\structure{A}$ to its $(\tau\setminus\{\rel{R}\})$-reduct $\structure{A}^{\cancel{\rel{R}}}$. For any $\sigma$-expansion of $\structure{A}$, any negated conjunct with an $\rel{R}$-atom is always satisfied, as $\rel{R}^\structure{A}=\varnothing$.
Thus, $\structure{A}\models\Phi$ iff $\structure{A}^{\cancel{\rel{R}}}\models\Phi^{\cancel{\rel{R}}}$. For $\tau$-structures $\structure{A}$ such that $\rel{R}^\structure{A}=\varnothing$, the correspondence $\structure{A}\longleftrightarrow\structure{A}^{\cancel{\rel{R}}}$ is one-to-one.
This means that the two problems are $\P$time equivalent.

Second stage: enriching negated conjuncts with $\tau$-atoms.

Call a $\GMSNP$ sentence enriched if, for any of its negated conjuncts $\neg\phi_i$ and any $\rel{R}\in\tau$, $\neg\phi_i$ contains at least one $\rel{R}$-atom.
We now show, for any connected $\Phi$, how to obtain an enriched sentence $\Phi'$ such that  the corresponding problems are $\P$time equivalent.
Take any negated conjunct $\neg \phi_i$ of $\Phi$ and replace it with $\neg\phi_i' := \neg\left(\phi_i\wedge \bigwedge_{\rel{R}\in\tau}\rel{R}(\tuple{x}_\rel{R})\right)$, where each $\tuple{x}_\rel{R}$ is a tuple of new variables.
Observe that $\Phi'$ is not connected anymore.
However, $\Phi$ is more restrictive than $\Phi'$, as we enrich negated conjuncts of $\Phi$ with $\tau$-atoms.
That is, for any $\tau$-structure $\structure{A}$, $\structure{A}\models\Phi$ implies $\structure{A}\models\Phi'$.
Below, we check the $\P$time equivalence of $\Sat(\Phi)$ and $\Sat(\Phi')$.

Above, one can see the transformation of each negated conjunct of $\Phi$ to a negated conjunct of $\Phi'$.
Below, it is shown how the structure $\structure{A}'$ is constructed from $\structure{A}$.

$\Sat(\Phi)$ is $\P$time reducible to $\Sat(\Phi')$.

For a $\tau$-structure $\structure{A}$, put $\structure{A}' := \structure{A} \uplus \left(\biguplus_{\rel{R}\in\tau}\structure{B}_\rel{R}\right)$.
Suppose that $\structure{A}\models\Phi$.
By <Ref>, we assume that, for $\rel{R}$ in $\tau$, $\structure{B}_\rel{R}\models\Phi$.
Then, by <Ref>, $\structure{A}'\models\Phi$, as $\structure{A}'$ is the disjoint union of structures satisfying $\Phi$.
But then, as $\Phi'$ is less restrictive than $\Phi$, we have $\structure{A}'\models\Phi'$.

Suppose that $\structure{A}'\models\Phi'$; then, for some $\sigma$-expansion $\structure{A}'^\sigma$, the first-order part $\phi'$ of $\Phi'$ is satisfied.
Choose a $\sigma$-expansion $\structure{A}^\sigma$ of $\structure{A}$ to be equal to $\structure{A}'^\sigma[A]$, the substructure of $\structure{A}'^\sigma$ induced on $A$.
Suppose that, for some negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$, there exists an assignment that makes it false in $\structure{A}^\sigma$.
But then we can take the corresponding negated conjunct $\neg\left(\phi_i\wedge \bigwedge_{\rel{R}\in\tau}\rel{R}(\tuple{x}_\rel{R})\right)$ of $\Phi'$, and assign $\tuple{b}_\rel{R}$ to each new tuple of variables $\tuple{x}_\rel{R}$.
Under this assignment the conjunct is false in $\structure{A}'^\sigma$, this is a contradiction.

$\Sat(\Phi')$ is $\P$time reducible to $\Sat(\Phi)$.

Consider a $\tau$-structure $\structure{A}$ that is an input instance of $\Sat(\Phi')$.
Suppose that, for some $\rel{R}$ in $\tau$, $\rel{R}^\structure{A}=\varnothing$.
Then, $\structure{A}\models\Phi'$ because $\Phi'$ is enriched.
We reduce it to some fixed YES instance of $\Sat(\Phi)$.

Suppose that, for all $\rel{R}$ in $\tau$, $\rel{R}^\structure{A}\not=\varnothing$. Firstly, $\structure{A}\models\Phi$ implies $\structure{A}\models\Phi'$ because $\Phi$ is more restrictive than $\Phi'$.
Suppose that $\structure{A}\not\models\Phi$; then, for any $\sigma$-expansion $\structure{A}^\sigma$ of $\structure{A}$ there exists a negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and a tuple $\tuple{a}_i$ of elements of $\structure{A}$ such that $\structure{A}^\sigma\models\phi_i(\tuple{a}_i)$.
But then, take the negated conjunct $\neg\left(\phi_i(\tuple{x}_i)\wedge\bigwedge_{\rel{R}\in\tau}\rel{R}(\tuple{x}_\rel{R})\right)$, assign $\tuple{a}_i$ to $\tuple{x}_i$ and assign $\tuple{a}_\rel{R}$ to $\tuple{x}_\rel{R}$ such that, for any $\rel{R}$ in $\tau$, $\tuple{a}_\rel{R}\in\rel{R}^\structure{A}$.
At least one such $\tuple{a}_\rel{R}$ exists as $\rel{R}^\structure{A}\not=\varnothing$.
But then $\structure{A}^\sigma\models\left(\phi_i(\tuple{a}_i)\wedge\bigwedge_{\rel{R}\in\tau}\rel{R}(\tuple{a}_\rel{R})\right)$.
This implies that $\structure{A}\not\models\Phi'$.

Last stage: concatenation. In this part, we construct a $\tau_1$-sentence $\Phi^1$ that is $\P$time equivalent to $\Phi$.
By <Ref>, we can assume that $\Phi$ is already enriched.
Set $\tau_1 := \{\rel{P}\}$, where $\mathrm{arity}(\rel{P}) = \sum_{\rel{R}\in\tau}\mathrm{arity}(\rel{R})$. For two tuples $\tuple{x}=(x_1,\ldots,x_n),\tuple{y}=(y_1,\ldots,y_m)$, set $(\tuple{x},\tuple{y}):=(x_1,\ldots,x_n,y_1,\ldots,y_m)$.
The notation $(\tuple{x}_1,\ldots,\tuple{x}_t)$ is defined similarly.

Recall that $\tau=\{\rel{R}_1,\ldots,\rel{R}_t\}$. For a negated conjunct $\neg\phi_i$ of $\Phi$, we construct the corresponding negated conjunct $\neg\phi_i^1$ of $\Phi^1$ as follows.
The $\sigma$-atoms of $\phi_i^1$ are the same as in $\phi_i$. For every $\tau$-atom $\rel{R}_j(\tuple{x})$ of $\phi_i$, add to $\phi_i^1$ a $\tau_1$-atom $\rel{P}(\tuple{y}_1,\ldots,\tuple{y}_t)$, where $\tuple{y}_j=\tuple{x}$ and all other variables of this atomic formula are new and they are used only there.
In the rest, we check the equivalence of the corresponding problems. Together, <Ref> imply <Ref>.

On the left, there is the $\tau$-part of some negated conjunct of $\Phi$.
On the right, there is the $\tau_1$-part of the corresponding negated conjunct of $\Phi^1$.

$\Sat(\Phi)$ is $\P$time reducible to $\Sat(\Phi^1)$.

For a $\tau$-structure $\structure{A}$, we construct the corresponding $\tau_1$-structure $\structure{A}_1$.
The structures have the same domain: $A_1=A$.
The relation $\rel{P}^{\structure{A}_1}$ is defined by the relations of $\tau$ as follows:

\begin{equation}\label{eq:construction_P_from_R}
\rel{P}^{\structure{A}_1}(\tuple{a}_1,\ldots,\tuple{a}_t)\longleftrightarrow\rel{R}_1^\structure{A}(\tuple{a}_1)\wedge\dots\wedge\rel{R}_t^\structure{A}(\tuple{a}_t).
\end{equation}

Suppose that $\rel{R}^\structure{A}=\varnothing$, for some $\rel{R}$ in $\tau$; then $\rel{P}^{\structure{A}_1}=\varnothing$ and $\structure{A}_1\models\Phi^1$.
But also $\structure{A}\models\Phi$, as $\Phi$ is enriched.
So, we can now assume that $\rel{R}^\structure{A}\not=\varnothing$, for any $\rel{R}$ in $\tau$.

The original $\tau$-structure $\structure{A}$ is on the left.
The corresponding $\tau_1$-structure $\structure{A}_1$ is on the right.

Let $\structure{A}^\sigma$ and $\structure{A}_1^\sigma$ be two $\sigma$-expansions of $\structure{A}$ and $\structure{A}_1$ such that, for any $\rel{X}$ in $\sigma$, $\rel{X}^{\structure{A}^\sigma}=\rel{X}^{\structure{A}_1^\sigma}$.
It suffices to show that $\structure{A}^\sigma\models\forall\tuple{x}\;\phi(\tuple{x})$ iff $\structure{A}_1^\sigma\models\forall\tuple{x},\tuple{y}\;\phi^1(\tuple{x},\tuple{y})$, where $\tuple{y}$ represents variables that are added during the construction of $\Phi^1$.
Suppose that $\structure{A}^\sigma\not\models\forall\tuple{x}\;\phi(\tuple{x})$; then, for some negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and for some tuple $\tuple{a}_i$, we have  $\structure{A}^\sigma\models\phi_i(\tuple{a}_i)$.
Consider the $i$th negated conjunct $\neg\phi_i^1(\tuple{x}_i,\tuple{y}_i)$ of $\Phi^1$.
To the tuple of variables $\tuple{x}_i$ that are used in $\phi_i$ as well, we assign the same tuple $\tuple{a}_i$.
Let $\rel{P}(\tuple{y}_1,\ldots,\tuple{y}_t)$ be a $\tau_1$-atom that is contained in $\phi_i^1$.
Pick a tuple $\tuple{y}_j$ of variables of this atom such that nothing is assigned to them yet.
We know that, for the $j$th relation symbol $\rel{R}_j$ in $\tau$, $\phi_i$ contains at least one $\tau$-atom $\rel{R}_j (\tuple{z}_j)$, thus each variable of $\tuple{z}_j$ is contained in $\tuple{x}_i$.
As $\tuple{a}_i$ is assigned to $\tuple{x}_i$, some tuple $\tuple{b}_j$ of elements of $A$ is already assigned to $\tuple{z}_j$.
Hence, we assign $\tuple{b}_j$ to $\tuple{y}_j$.
Repeat this procedure for all unassigned variables of $\rel{P}(\tuple{y}_1,\ldots,\tuple{y}_t)$.
By <ref>, we have $\structure{A}^\sigma_1\models\rel{P} (\tuple{b}_1,\ldots,\tuple{b}_t)$.
This is true for any $\tau$-atom of $\phi_i^1$.
Thus, $\structure{A}_1^\sigma\not\models\forall\tuple{x},\tuple{y}\;\phi(\tuple{x},\tuple{y})$.

For the other direction, suppose that $\structure{A}_1^\sigma\not\models\forall\tuple{x},\tuple{y}\;\phi(\tuple{x},\tuple{y})$; then there is a negated conjunct $\neg\phi_i^1(\tuple{x}_i,\tuple{y}_i)$ and tuples $\tuple{a}_i,\tuple{b}_i$ of elements of $A$ such that $\structure{A}_1^\sigma\models\phi_i^1(\tuple{a}_i,\tuple{b}_i)$.
Take the corresponding negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and assign $\tuple{a}_i$ to $\tuple{x}_i$.
We have $\structure{A}^\sigma\models\phi_i (\tuple{a}_i)$, by <ref>.

$\Sat(\Phi^1)$ is $\P$time reducible to $\Sat(\Phi)$.

For an arbitrary $\tau_1$-structure $\structure{B}_1$, we construct a $\tau$-structure $\structure{B}$.
They have the same domain $B$, and every $\tau$-relation $\rel{R}_j^\structure{B}$ is defined as follows:

\begin{equation}\label{eq:construction_R_from_P}
\rel{R}_j^\structure{B}(\tuple{x}_j)\longleftrightarrow\exists\tuple{x}_1,\ldots,\tuple{x}_{j-1},\tuple{x}_{j+1},\ldots,\tuple{x}_t\;\rel{P}^{\structure{B}_1}(\tuple{x}_1,\ldots,\tuple{x}_t).
\end{equation}

Similarly as above, we consider two $\sigma$-expansions $\structure{B}^\sigma$ and $\structure{B}_1^\sigma$ such that, for all $\rel{X}$ in $\sigma$, $\rel{X}^{\structure{B}^\sigma}=\rel{X}^{\structure{B}_1^\sigma}$.
Suppose that $\structure{B}_1^\sigma\not\models\forall\tuple{x},\tuple{y}\;\phi^1(\tuple{x},\tuple{y})$; then there exists a negated conjunct $\neg\phi_i^1(\tuple{x}_i,\tuple{y}_i)$ and assignments $\tuple{a}_i,\tuple{b}_i$ to $\tuple{x}_i,\tuple{y}_i$ such that $\structure{B}_1^\sigma\models\phi_i^1(\tuple{a}_i,\tuple{b}_i)$.
Take the $i$th negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and assign $\tuple{a}_i$ to $\tuple{x}_i$.
As $\phi_i$ and $\phi_i^1$ have the same $\sigma$-part, $\structure{B}^\sigma$ satisfies every $\sigma$-atom and negated $\sigma$-atom of $\phi_i$.
Any $\tau$-atom of $\phi_i$ is satisfied, by <ref>.
So $\structure{B}^\sigma\models\phi_i(\tuple{a}_i)$.

For the other direction, suppose that $\structure{B}^\sigma\models\phi_i (\tuple{a}_i)$, for some negated conjunct $\neg\phi_i(\tuple{x}_i)$ of $\Phi$ and for some assignment $\tuple{a}_i$ of elements of $B$ to the variables $\tuple{x}_i$ of $\phi_i$. For any $\tau$-atom $\rel{R}_j(\tuple{z})$ of $\phi_i$, $\phi_i^1$ contains a $\tau_1$-atom $\rel{P}(\tuple{y}_1,\ldots,\tuple{y}_t)$, where $\tuple{y}_j=\tuple{z}$.
We know that some tuple $\tuple{c}$ is assigned to $\tuple{z}$ such that $\structure{B}^\sigma\models\rel{R}_j(\tuple{c})$.
By <ref>, there exist $\tuple{b}_1,\ldots,\tuple{b}_{j-1},\tuple{b}_{j+1},\ldots,\tuple{b}_t$ such that $\rel{P}^{\structure{B}_1^\sigma}(\tuple{b}_1,\ldots,\tuple{b}_t)$, where $\tuple{b}_j=\tuple{c}$.
So, for all $\tuple{y}_1,\ldots,\tuple{y}_t$ except for $\tuple{y}_j=\tuple{z}$, we assign $\tuple{b}_1,\ldots,\tuple{b}_t$ to them.
Then, $\structure{B}_1^\sigma\models\rel{P}(\tuple{b}_1,\ldots,\tuple{b}_t)$, this is true for any $\tau$-atom of $\phi_i^1$.
Any $\sigma$-atom and negated $\sigma$-atom of $\phi_i$ is also satisfied by the choice of $\sigma$-expansions.
This implies that $\structure{B}_1^\sigma\not\models\forall\tuple{x},\tuple{y}\;\phi^1(\tuple{x},\tuple{y})$ and we are done.

§ MATRIX PARTITION

We are not aware of any logic above $\MMSNP$ that is still monadic but the “monotone” condition is changed to something less strict.
However, there is a well-known class of matrix partition problems <cit.> that extends graph homomorphisms in this direction.
It is not known if this class enjoys a $\P$vs$\NPc$ dichotomy.
In this section, we define corresponding logical classes and discuss
what can be an analogue of the “guarded” property for them.

Let $\matrice{M}$ be an $(s\times s)$-matrix with entries from $\{0,1,\star\}$.
A loopless graph  $\structure{G}$ admits $\matrice{M}$-partition if its domain $G$ can be split into $s$ classes $X_1,\ldots,X_s$ such that, for any two distinct $x,y$ from any $X_i,X_j$,

* if $m_{i,j}=0$, then $(x,y)\not\in E^\structure{G}$,

* if $m_{i,j}=1$, then $(x,y)\in E^\structure{G}$,

* if $m_{i,j}=\star$, then there is no restriction for $(x,y)$.

Any matrix partition problem can be expressed in the form of <ref> as follows, this gives rise to a fragment of $\SNP$ introduced further in <Ref>.

\begin{align*}
&\exists \rel{X}_1,\ldots,  \rel{X}_s\;\forall x,y \; \neg\bigl(\neg\rel{X}_1(x)\wedge\dots\wedge\neg\rel{X}_s(x)\bigr)\wedge\bigwedge_{i,j\in[s],i\not=j}\bigl(\rel{X}_i(x)\wedge\rel{X}_j(x)\bigr)\wedge\\ \bigwedge_{m_{i,j}=0} &\neg\bigl(\rel{E}(x,y)\wedge\rel{X}_i(x)\wedge\rel{X}_j(y)\wedge x\not=y\bigr)\wedge\bigwedge_{m_{i,j}=1} \neg\bigl(\neg\rel{E}(x,y)\wedge\rel{X}_i(x)\wedge\rel{X}_j  (y)\wedge x\not=y\bigr).
\end{align*}

A $\tau$-sentence $\Phi$ written in the form of <ref> belongs to the class $\mathsf{GMPART}_{\not=}$ if:

* each $\alpha_i$ is either a conjunction only of nonnegated $\tau$-atoms or a conjunction only of negated $\tau$-atoms,

* each $\beta_i$ is a conjunction of unary $\sigma$-atoms or negated unary $\sigma$-atoms, and

* for every inequality $x_j\not=x_j'$ of each $\epsilon_i$ there exists a $\tau$-atom in $\alpha_i$ that contains both $x_j$ and $x_j'$.

The class $\mathsf{GMPART}_{\not=}$ contains both matrix partition problems and $\GMMSNPineq$ from <Ref> but it is not contained in monadic $\SNP$ without $\not=$. Denote by $\mathsf{MPART}$ the fragment of $\mathsf{GMPART}_{\not=}$, where each $\epsilon_i$ is empty. This class (strictly) extends $\MMSNP$ and belongs to monadic $\SNP$ without $\not=$ at the same time.

There is a sentence $\Phi$ in $\mathsf{MPART}$ such that, for any $\Psi$ in $\MMSNP$, $\Phi$ is not logically equivalent to $\Psi$.

Let $\Phi$ be a sentence that accepts only complete directed graphs with loops: $\forall x,y\;\neg\bigl(\neg\rel{E}(x,y)\bigr)$.
As $\Sat(\Phi)$ is not closed under inverse homomorphisms, it can not be expressed by an $\MMSNP$ sentence, by <Ref>.

Although $\mathsf{GMPART}_{\not=}$ is related to $\mathsf{MPART}$ in the same way as $\GMMSNPineq$ is related to $\MMSNP$, the methods from the proof of <Ref> do not spread to them because now negated conjuncts may contain negated $\tau$-atoms. This means that these two classes might differ having a dichotomy.

Is it true that for every $\Phi$ in $\mathsf{GMPART}_{\not=}$ there is $\Phi'$ in $\mathsf{MPART}$ such that $\Sat(\Phi)$ is $\P$time equivalent to $\Sat(\Phi')$?

§ NP IS PTIME EQUIVALENT TO MMSNP WITH INEQUALITY

We prove <Ref> and consider a problem $\Omega$
in $\NP$: we may assume that $\Omega$ is decided
by an oblivious Turing Machine $M_o$, for which the head
movement depends only on the size of the input string.
We build a sentence $\Phi$ in $\MMSNPineq$ that shall operate on an input $\structure{A}$ which ought to describe the space-time diagram of an input string $\tuple{x}$ of $M_o$.
We use two binary input predicates $\rel{succ}$ and $\rel{next}$ for space and time respectively, together with additional predicates to obtain a grid like structure.

Obliviousness allows us to check the computation with monadic predicates only, and it is not hard to prove the following.

There exists a $\P$time reduction $\func{r}_1$ from $\Omega$ to $\Sat(\Phi)$.

The actual subtlety of the proof concerns the converse reduction, and to deal appropriately with structures $\structure{A}$ that are degenerate in the sense that they are not in the image of $\func{r}_1$.
It is precisely this part of the proof that is fully absent
in <cit.>. For this part, we need a very uniform
oblivious Turing machine for which we can predict the movement of the head.
Our construction of $\Phi$ ensures that:

* if $\structure{A}$ is over-complete, then $\structure{A}\not\models\Phi$ (checking that the degree of $\rel{succ}$ or $\rel{next}$ is 2 or  more is possible in $\MMSNPineq$),

* if $\structure{A}$ is not complete enough either locally – it is like a grid with holes – or globally – too small to simulate a complete run of $M_o$, then $\structure{A}\models\Phi$ (this is achieved by a monadic marking scheme of $\structure{A}$ by the sentence $\Phi$ and a relativization of the verification of $M_o$'s computation to the marked part),

* if $\structure{A}$ is in an appropriate form and can simulate a run of $M_o$, then $\structure{A}\models\Phi$ iff $M_o$ accepts.

We use space-time diagrams as input instances of the $\MMSNPineq$ sentence.
In order to ensure that an input instance $\structure{A}$ can simulate the whole execution of $M_o$, we need to know the position of its head at any moment of time and the precise time when the machine will halt.
An arbitrary Turing machine can not provide this information, so we need to consider only oblivious ones.
Denote by $\family{O}$ a family of Turing machines $M_o$ that satisfy the following.

* $M_o$ has a one-way infinite tape.

* The head of $M_o$ is at the first element of the tape at the start.

* For an input string of length $n$, the head first moves to the $n$th cell, then returns to the left end, then moves to the $(n+1)$th cell, then returns to the left end, and so on.
At each next round-trip, the tape length increases by one cell.
In the end of the run, the head returns to the left end and halts.

* For some $k\in\mathbb{N}$ there is $\func{f}(n)\in O(n^k)$ such that, for any input string of length $n$, the head makes precisely $\func{f}(n)+1$ round-trips as above before it halts.
This means that the head makes precisely $\func{g}(n) :=\frac{1}{2}\bigl(\func{f}(n)+1\bigr)\bigl(2n-2+\func{f}(n)\bigr)$ movements during the run.

It is well-known that an oblivious machine can simulate any other one <cit.>.
However, as $\family{O}$ has some additional constraints, we need the following lemma, its proof can be found in <Ref>.

For any nondeterministic Turing machine $M$ there is a $\P$time equivalent Turing machine $M_o$ in $\family{O}$.

At first, we find an equivalent machine $M'$ whose running time depends only on the size of the input.
Then, we construct $M_o$ from $M'$ by using a method similar to the one used in <cit.>.

Construction of the space-time diagram.
Let $M_o$ have the alphabet $\Sigma_o$, and let $\tuple{x}\in(\Sigma_o\setminus\{\sqcup\})^n$ be an input string.
$\structure{A}:=\func{r}_1(\tuple{x})$ has a form of a space-time diagram, where the horizontal axis represents “space”, and the vertical axis represents “time”.
It consists of $\func{g}(n)+1$ rows, each row represents the tape at a moment of time from $0$ to $\func{g}(n)$.
The first row has length $n+1$, and the length increases by $1$ each time when the head is at the rightmost element, the $n$th row has length $n+1$ but the $(n+1)$th row has length $n+2$.

$\structure{A}$ has a relational signature:

\begin{equation*}
\tau = \bigl\{\rel{s}(\cdot)\mid s\in\Sigma\setminus\{\sqcup\}\bigr\}\uplus\bigl\{\rel{start}(\cdot), \rel{succ}(\cdot,\cdot), \rel{next}(\cdot,\cdot),\rel{row}(\cdot,\cdot,\cdot)\bigr\},\;\text{where}
\end{equation*}

* relations $\rel{s}(\cdot)$ represent the alphabet $\Sigma_o$: the $(i+1)$th element of the first row belongs to $\rel{s}^\structure{A}$ iff the $i$th cell $x_i$ of the string $\tuple{x}$ contains $s\in\Sigma_o$;

* $\rel{start}(\cdot)$ represents the point of reference of the diagram, there is a unique element in $\rel{start}^\structure{A}$ – the first element of the first row;

* $\rel{succ}(\cdot,\cdot)$ is a horizontal arc: it links two neighbors of the same row and also it connects the last element of a row to the first element of the next row;

* $\rel{next}(\cdot,\cdot)$ is a vertical arc: for each $i$, it connects the $i$th element of a row to the $i$th element of the next row;

* $\rel{row}(x,y,z)$ represents the membership of $y$ within the row that starts in $x$ while the next row starts in $z$.

An example of $\structure{A}$, for the case $n=3$ and $\func{f}(3)=1$, is displayed on <Ref>.

The structure $\structure{A}=\func{r}_1(x_1x_2x_3)$, and the positions of the head $\rel{H}$.

Construction of $\Phi$.
The existential relations of $\Phi$ are:

\begin{equation*}
\sigma = \bigl\{\rel{S}(\cdot)\mid s\in\Sigma_o\bigr\}\uplus\bigl\{\rel{Mark}(\cdot), \rel{Init}(\cdot),\rel{H}(\cdot)\bigr\}\uplus \bigl\{\rel{Q}(\cdot)\mid q\in\family{Q}\bigr\},\;\text{where}
\end{equation*}

* relations $\rel{S}$ describe the string symbols at any moment of time;

* $\rel{Mark}$ determines the region, where the head movement is mandatory;

* $\rel{Init}$ contains the elements of the first row, it is used in order to generate all $\rel{Mark}$ elements and to assign the initial symbols: $\rel{s}(x)\to\rel{S}(x)$;

* $\rel{H}$ contains all the positions of $M_o$'s head at every moment of time;

* relations $\rel{Q}$ represent the current state of the machine.

The two most important relations are $\rel{Init}$ and $\rel{Mark}$, as other simply imitate the execution of $M_o$.
The relation $\rel{Init}$ is initiated by the $\rel{succ}$-neighbor of the $\rel{start}$ and it must spread either until the end of the first row or until an element that is not contained in a relation $\rel{s}$, for $s\in\Sigma_o$.
The existential relation $\rel{S}$ is assigned to an $\rel{Init}$ element $x$ if $\rel{s}(x)$ holds.
The relation $\rel{Mark}$ is initiated by the $\rel{Init}$ elements and then it must spread along the vertical $\rel{next}$-arcs from top to bottom.
The $\rel{next}$-neighbor (red circle) must be in $\rel{Mark}$ only if its predecessor (black circle) is in $\rel{Mark}$ and if the neighborhood looks like a two-dimensional grid, see <Ref>.
The head $\rel{H}$ is forced to move only if it is in $\rel{Mark}$.
If the head is in a rejecting state, then the sentence is false.

End, no head.

End, head.

All the four cases when $\rel{Mark}$ is forced to spread to the bottom.

The expressiveness of $\MMSNPineq$ permits $\Phi$ to have the following first-order properties:

* there is at most one $\rel{start}$ element,

* the in- and out- degrees of $\rel{succ}$ and $\rel{next}$ are at most 1,

* an element $y$ can not be in different triples $\rel{row}(x,y,z)$ and $\rel{row}(x',y,z')$,

* loops $\rel{succ}(x,x),\rel{next}(x,x)$ are forbidden as well as $\rel{row}(x,y,x)$, and

* there can not be 2 symbol relations $\rel{s}(x),\rel{s}'(x)$ for the same element.

<Ref> follows from the constructions of $\Phi$ and $\structure{A}$.
For more details on $\Phi$ and for the proof of <Ref>, see <Ref>.

The difficult direction.
It remains to show the following lemma, for a full proof see <Ref>.

For any $\tau$-structure $\structure{B}$ there exists an input string $\tuple{x}\in(\Sigma_o\setminus\{\sqcup\})^\ast$ such that $\tuple{x}$ is computed in Ptime in $|B|$ and $\structure{B}\models\Phi$ iff $M_o$ accepts $\tuple{x}$.

An incomplete structure.

Computing $\rel{Init},\rel{Mark}$, and $\rel{H}$.

The cases 2 and 3.

As the input structure $\structure{B}$ is arbitrary, there are $3$ cases to consider. The first two are easy to deal with.

* $\structure{B}$ violates one of first-order properties imposed by $\Phi$, the $\rel{start}$ element is not unique, or the degree of $\rel{succ}$ or $\rel{next}$ is 2 or greater, etc.
These properties are checked in $\P$time, if this is the case, then we reduce $\structure{B}$ to a fixed NO instance of $M_o$.

* The set of elements of $\structure{B}$ that are forced to be in $\rel{Mark}$ is not sufficient to simulate the entire run of the machine. For example, if the $\rel{start}$ element does not exist, then no element is forced to be in $\rel{Mark}$, so the head $\rel{H}$ will never be in a rejecting state. Or, if the first row contains $n$ elements, and the total number of rows is lesser than $\func{g}(n)$. In any of these situations, $\structure{B}\models\Phi$, so we can reduce it to a fixed YES instance of $M_o$.
See <Ref>.

* $\structure{B}$ allows to simulate $M_o$'s run.
In order to check if $\structure{B}$ falls into this case, we find in $\P$time all the elements of $\structure{B}$ that are forced to be in $\rel{Init}$, in $\rel{Mark}$, and in $\rel{H}$.
The $\rel{Init}$ elements are the $\rel{succ}$-essors of the $\rel{start}$.
Then, we find all the elements that are forced to be in $\rel{Mark}$, there is the minimal by inclusion set of them.
Then, we find all the positions of the head $\rel{H}$, it is also done in $\P$time because the head movement is deterministic.
If, during the first round-trip, the head passes $n$ elements and if the $\bigl(\func{g}(n)+1\bigr)$th row has an element from $\rel{H}$, then, by obliviousness, we are sure that the execution halts there.
Otherwise, we are in case 2.
In case 3, we reduce $\structure{B}$ to the string consisting of symbols that are present on the first row of $\structure{B}$.
See <Ref>.

§ PROOF OF <REF>

For any nondeterministic Turing machine $M$ there is a $\P$time equivalent Turing machine $M_o$ from $\family{O}$.

We show that for any nondeterministic Turing machine there exists a $\P$time equivalent $\MMSNPineq$ sentence.

Feder and Vardi in <cit.> consider only oblivious Turing machines.
An oblivious Turing machine is defined by the following property: for any two input instances of the same size, the head movements during the machine executions are the same.
That is, the head movement does not depend on the symbols written on the tape, it depends only on the size of the input.
More formally, a (possibly nondeterministic) Turing machine $M_o$ is called oblivious if there exists a function $\func{f}\colon\mathbb{N}\to\mathbb{N}$ such that, for any input $\tuple{x}$ of size $\card{\tuple{x}}=n$, $M_o$ decides $\tuple{x}$ in precisely $\func{g}(n)$ steps.
And that, for every two inputs $\tuple{x}_1,\tuple{x}_2$ such that $\card{\tuple{x}_1}=\card{\tuple{x}_2}$, and, for any moment $t$, for $0\leq t\leq \func{g}(n)$ of each execution, the positions of the head are the same.
The concept of oblivious Turing machines is introduced by Pippenger and Fischer in <cit.>.

The proof of <Ref> is only vaguely sketched in <cit.>.
We provide a complete proof in this section.
This proof relies on a specific choice of the way in which we expect an oblivious Turing machine to work.
That is, we do not know how to provide a proof of <Ref> that would use <cit.> as a black box reduction from nondeterministic Turing machines to oblivious ones.

Before explaining how $\NP$ can be embedded into $\MMSNPineq$, we argue that one can consider only oblivious Turing machines with a one-way infinite tape.
Then, for any oblivious Turing machine, we construct an $\MMSNPineq$ sentence $\Phi$ and then show that the corresponding problems are $\P$time equivalent.

In the reduction, an input instance of a Turing machine is associated with a structure that looks like a two-dimensional grid, which represents the set of tape configurations at any moment of the execution.
That is, the structure shall be used to represent a canvas for the space-time diagram of the oblivious Turing machine.
A row consists of cells that are either occupied by the input or visited by the head by this time.
When the head reaches the rightmost cell of the tape it does one more step to the right and, thus, increases the row size by 1, as a new cell is visited.
The first row is associated with the initial configuration of the tape ($t=0$): the head is at the leftmost cell, the string of symbols is the initial input string.
The next row is associated with the next moment of time ($t=1$), the head has done one step to the right.
The movements of the head are independent of the input contents.
So it shall be possible to check that the grid is in the correct shape in $\MMSNPineq$.

We assume that a Turing machine that we consider is nontrivial, , it neither accepts all input instances nor rejects all of them.

For a Turing machine $M$, we say that the running time of $M$ depends only on the size of the input if there is a function $\func{f}\colon \mathbb{N}\to\mathbb{N}$ such that, for any input $\tuple{x}$ of size $\card{\tuple{x}}=n$, $M$ decides $\tuple{x}$ in precisely $\func{f}(n)$ steps. The following lemma allows us to consider without loss of generality only Turing machines whose running time depends only on the size of the input.

Let $M$ be a nondeterministic Turing machine. Let $\func{f}\colon\mathbb{N}\to\mathbb{N}$ be a function such that $M$ operates within time $\func{f}(n)$. Then there is a nondeterministic Turing machine $M'$ that is $\P$time equivalent to $M$ and whose running time depends only on the size of the input.

We know that, for some $c,k$ in $\mathbb{N}$, $\func{f}(n)\leq cn^k$. We construct a Turing machine $M'$ that decides an input of $M$ of size $n$ precisely in time $\func{f}'(n)$, for some other function $\func{f}'\colon\mathbb{N}\to\mathbb{N}$. The machine $M'$ has two tapes. The alphabet of the first tape is the same as the alphabet of $M$. The alphabet of the second tape has $m$ symbols, where $m = 2^k + c'$ such that $m^{\log_2 n} > cn^k$. Such $m$ exists and it is fixed and does not depend on $n$. Suppose without loss of generality that it consists of the symbols $1,\ldots,m$. Then every execution of $M'$ is as follows:

* The head of the first tape of $M'$ scans it and writes on the second tape the sequence of $1$s of length $\lceil\log_2 n\rceil$. This procedure takes the same amount of time for any input on the tape 1 of size $n$.

* Then, $M'$ does the same things as $M$ for this input. And, for the tape 2, $M'$ acts as a deterministic Turing machine. It consequently writes all the $\lceil\log_2n\rceil$-sequences consisting of numbers from $1$ to $m$. For $m$ large enough, the execution for the tape 2 always stops after the execution for the tape 1. At the end, it is always in the accepting state.

The machine $M'$ accepts the input if it both tapes answer YES. Otherwise it rejects the input. By construction, it is equivalent to $M$. And it is well-known, see <cit.>, that a machine with two tapes can be simulated by a machine with one tape. Thus, it is possible to construct an equivalent machine such that its running time depends only on the size of the input.

The next lemma states that without loss of generality we can assume that the movement of the head of the machine is the same for any two input instances of the same size. For a Turing machine $M$, we construct an oblivious Turing machine $M_o$. The movement of head of $M_o$ is always the same: for every iteration of $M$, the head of $M_o$  walks to the right end of the tape, increases the tape size by 1, and then walks to the left end of the tape, see <Ref> on fig:oblivious_scheme.

The trajectory of the head movement of $M_o$.

If $M$ halts in precisely $\func{f}(n)$ steps, for an input of size $n$, then $M_o$ halts, for any input of size $n$, in $\func{g}(n)$ steps, where:

\begin{equation*}
\func{g}(n) := 2(n-1) + 2n + \ldots + 2(n+\func{f}(n)-1) = \frac{1}{2}\bigl(\func{f}(n)+1\bigr)\bigl(2n-2+\func{f}(n)\bigr).
\end{equation*}

For any nondeterministic Turing machine $M$ with a one-way infinite tape whose running time depends only on the size of the input, there exists a $\P$time equivalent oblivious nondeterministic Turing machine $M_o$ with a one-way infinite tape.

Let $M$ have the alphabet $\Sigma = \{s_1,\ldots,s_k,\triangleright,\sqcup\}$, where $\triangleright$ is the first symbol and $\sqcup$ is the blank symbol; and the states $\family{Q}=\{q_0,\ldots,q_m\}$, where $q_0$ is the starting state. Firstly, we describe the alphabet $\Sigma_o$ and the set of states $\family{Q}_o$ of $M_o$.

* For $s$ in $\Sigma\setminus\{\triangleright,\sqcup\}$, add to $\Sigma_o$ two symbols: $s,s^h$. The $h$-superscript helps to remember the position of the head of $M$. Instead of one blank symbol in $\Sigma$, $\Sigma_o$ has three symbols: $\sqcup, \sqcup',\sqcup^{\prime h}$. $\sqcup$ is written in cells that are not visited by the head of $M_o$. $\sqcup'$ is written in those cells that are blank but the head of the machine $M$ potentially could have already visited them. $\sqcup^{\prime h}$, similarly as $s^h$, informs the head of $M_o$ that the head of $M$ is at the same cell. At last, add the first symbol $\triangleright$ to $\Sigma_o$.

* Any state $q_i$ in $\family{Q}$ is replaced by two states: $q_i^L,q_i^R$ in $\family{Q}_o$ – they highlight the head movement direction (Left or Right).  Then, for every pair of states $q_i,q_j$ of $\family{Q}$, we add four states to $\family{Q}_o$: $q_{i\to j}^L$ and $q_{i\to j}^R$ and $q_{i\to j(write)}^R,q_{i\to j(write)}$ – they are used when $M_o$ simulates the transition of $M$. And also we add to $\family{Q}_o$ states $q_{start},q_{search},q_{return}$ that are used at the start of the execution in order to check if the input of $M_o$ is associated with the input of $M$; $q_{start}$ is the starting state. And, finally, for every newly added state, we add a copy of it that is labeled with the word “error”, for $q_i^R$ we add $q_{i}^{R,error}$. For every state of the type $q$, the corresponding state of the type $error$ does the same function but, in this case, at the end of the execution, the machine always answers YES.

We explain how $M_o$ works. Our informal explanation is followed by an explicit description of $M_o$.

We assume that for every input tape there is $N$ in $\mathbb{N}$ such that the first cell contains $\triangleright$, next $N$ cells contain symbols of $\Sigma_o\setminus\{\triangleright,\sqcup\}$, and every other cell contains the blank symbol $\sqcup$. We also assume that the head of $M_o$ is in the first cell of the tape and in the state $q_{start}$ when the execution starts.

Informal description of $M_o$.
We want to check if the input of the machine $M_o$ is associated with an input of the machine $M$. It must have the following form: the first cell must contain the first symbol $\triangleright$, the next $n$ cells must contain an element of $\Sigma\setminus\{\triangleright,\sqcup\}$, and all other cells must contain $\sqcup$.

Check if the input of $M_o$ is exactly like an input of $M$.
At the start of any execution, the head turns into the state $q_{search}$ and moves to the right end of the input in this state. When it reads the blank symbol $\sqcup$, it turns into the state $q_{return}$ and moves  back to the initial position in this state. During the left-to-right walk, the head scans every cell and changes the state to $q_{search}^{error}$ if the cell contains an element not from $\Sigma\setminus\{\triangleright,\sqcup\}$. The head edits the bad cell by writing in it a symbol from $\Sigma\setminus\{\triangleright,\sqcup\}$. Thus, when the head returns back to the initial position, the input of the machine is of the right form. But the machine already knows that there is an error, and it shall accept this input at the end of the execution anyway.

Simulate one move of $M$ by two walks: left to right, then right to left.
After this scanning and editing procedure, the machine $M_o$ starts the simulation of the execution of $M$. Every move of the head of $M$ is associated with the walk of the head of $M_o$ towards the right end of the tape and its return to the left end. The head of $M_o$ moves to the right, until it scans the first cell with the blank symbol $\sqcup$. It rewrites $\sqcup$ to $\sqcup'$ in order to mark that during the next walk it does not have to stop at the same cell and can make one more step to the right. Then it returns to the left end of the input string.

If the head is at a cell with a symbol $s$ without the $h$-superscript, then the head of $M_o$ does not rewrite the symbol and keeps walking in the same direction.

Any cell, except for the first and the last ones, is visited by the head of $M_o$ exactly two times: when it goes left-to-right and right-to-left. Suppose that the head of $M_o$ scans a cell that contains $s^h$ and that the original Turing machine $M$ is in the state $q_i$ now. As it is non-deterministic, there is more than one possible transition from this configuration. For every transition when $M$ decides to move to the right, $M_o$ simulates this transition during the left-to-right walk, and for every transition when $M$ decides to move to the left, $M_o$ does this when the head is returning to the left end. Suppose that the head of $M_o$ is moving towards the right end now, that it is in the state $q_i^R$, and that it reads $s^h$ from the current cell; then the machine $M_o$ can do one of the following things.

$\bf{right:}$ $M_o$ decides to simulate one of the possible transitions of $M$ for the configuration $(q_i,s)$ when, during the transition, the head of $M$ moves to the right, $(q_i,s)\to (q_j,s',\rightarrow)$. In this case, $M_o$ changes its state to $q_{i\to j(write)}^R$, writes $s'$, and moves one cell to the right. Then it changes to the state $q_{i\to j}^R$ and, for the symbol $s_1$ of this new cell, writes $s_1^h$ and keeps walking to the right end. Then it changes to the state $q_{i\to j}^L$ and walks towards the left end. And, at the left end, it changes to the state $q_j^R$ and repeats the walk. See <Ref> on fig:oblivious_simulation.

$\bf{left:}$ The machine $M_o$ decides to simulate one of the transitions when the head of $M$ walks to the left. In this case, $M_o$ does not change its state $q_i^R$ until it is at the right end of the tape. Then it turns to the state $q_i^L$, arrives to the cell with $s^h$ during the right-to-left walk and does the steps similar to those from the previous case.

A move of the head of a machine $M$ is simulated by a walk of the head of the corresponding oblivious machine $M_o$.

If the head of $M$ is at the first cell, then it always moves to the right. This means that $M_o$ must simulate this movement when it is going to the right from the first cell.

Any state of the type $error$ is similar to the corresponding one of the type $q$. The only difference is that at the end of the execution the machine in an $error$-type state  always answers YES.

Explicit description of $M_o$

We give below the transitions of $M_o$. For the sake of brevity, we do not write the transition rules for the states of the type $error$ as they just repeat the transition rules of the usual states, and, once $M_o$ is in an $error$ state, it will always be in an $error$ state.

Transitions checking the input.
If the cell, where the head of $M_o$ is before the run, contains something different from $\triangleright$, then the machine turns to the $q_{search}^{error}$ state, writes $\triangleright$ in the first cell, and starts walking to the right. If the first cell contains $\triangleright$, then the machine writes nothing and just walks to the right while being in the state $q_{search}$.

\begin{equation*}
\forall s\not=\triangleright \; \bigl((q_{start}, s)\to (q_{search}^{error}, \triangleright,\rightarrow)\bigr),
\end{equation*}

\begin{equation*}
\end{equation*}

When the head of $M_o$ walks to the right: either it meets a symbol not from $\Sigma$, edits it to a symbol from $\Sigma$, changes the state to $q_{search}^{error}$, and keeps moving to the right; or it edits nothing and keeps moving to the right.

\begin{equation*}
\forall s\not\in\Sigma \; \bigl((q_{search},s)\to (q_{search}^{error}, s_1,\rightarrow)\bigr), \text{ for some arbitrary } s_1\in\Sigma,
\end{equation*}

\begin{equation*}
\forall s\in\Sigma\setminus\{\triangleright,\sqcup\} \; \bigl((q_{search},s)\to(q_{search},s,\rightarrow)\bigr).
\end{equation*}

Now we describe what the head does when it reaches the right end. Observe that, when the machine is at the right end and in the state $q_{search}$, the tape already has a good form, so we do not need to edit it anymore.

\begin{equation*}
(q_{search},\sqcup)\to(q_{return}, \sqcup',\leftarrow),\; \forall s\in\Sigma_o\setminus\{\triangleright\}\; \bigl((q_{return},s)\to (q_{return},s,\leftarrow)\bigr).
\end{equation*}

When the head of $M_o$ returns to the first cell, it simulates the first move of $M$. Suppose that $M$ has the following transition rule:

\begin{equation*}
\end{equation*}

then $M_o$ has the following transition rule:

\begin{equation*}
(q_{search},\triangleright)\to\bigl\{(q_{0\to i_1(write)}^R,\triangleright,\rightarrow),\ldots,(q_{0\to i_k(write)}^R,\triangleright,\rightarrow)\bigr\}.
\end{equation*}

For $q_i,q_j$ in $\family{Q}$, the states $q_{i\to j(write)}^L,q_{i\to j(write)}^R$ are used when the head of $M_o$ simulates the change of the head position of the initial machine $M$. The head of $M_o$ adds the $h$-superscript to the symbol of the next cell. Thus, $M_o$ must have the following rules for any symbol of $\Sigma_o\setminus\{\sqcup,\triangleright\}$ without the $h$-superscript:

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup,\triangleright\} \; \bigl((q_{i\to j(write)}^R,s)\to (q_{i\to j}^R,s^h,\rightarrow)\bigr),
\end{equation*}

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup,\triangleright\} \; \bigl((q_{i\to j(write)}^L,s)\to (q_{i\to j}^L,s^h,\leftarrow)\bigr).
\end{equation*}

Note that by  construction, the head of $M_o$ can not be simultaneously in the state of the type $q_{i\to j(write)}$ and scan the symbol $\sqcup$. The head can not be in the first cell (that contains $\triangleright$) in a state of the types $q_{i\to j}^R, q_{i\to j(write)}^R$, as there is no cell to the left from the first cell. However, it can be at the first cell in a state of the type $q_{i\to j(write)}^L$. We will describe this case  later.

If the head of $M_o$, being in a state not of the type $q_{i\to j(write)}$, reads a symbol without the $h$-superscript, then it does not change the symbol and keeps moving further:

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup\} \; \bigl((q_i^R, s)\to(q_i^R, s,\rightarrow)\bigr),
\end{equation*}

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup\} \; \bigl((q_{i\to j}^R, s)\to(q_{i\to j}^R, s,\rightarrow)\bigr),
\end{equation*}

and similarly for the right-to-left direction:

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup\} \; \bigl((q_i^L, s)\to(q_i^L, s,\leftarrow)\bigr),
\end{equation*}

\begin{equation*}
\forall q_i,q_j\in\family{Q},s\in\bigl(\Sigma\cup\{\sqcup'\}\bigr)\setminus\{\sqcup\} \; \bigl((q_{i\to j}^L, s)\to(q_{i\to j}^L, s,\leftarrow)\bigr),
\end{equation*}

If the head of $M$ is not at the first cell, then, for a rule

\begin{equation*}
\end{equation*}

of $M$, we write a rule

\begin{equation*}
(q_i^R,s^h)\to(q_{i\to j_k(write)}^R, s_{j_k},\rightarrow)
\end{equation*}

for any $k$ in $\{1,\ldots,m\}$ such that $D_k = \rightarrow$; and if $D_k = \leftarrow$, then we write a rule

\begin{equation*}
(q_i^L,s^h)\to(q_{i\to j_k(write)}^L, s_{j_k},\leftarrow),
\end{equation*}

and we also want to let the head of $M_o$ pass $s^h$ when it moves left-to-right:

\begin{equation*}
(q_i^R,s^h)\to (q_i^R, s^h,\rightarrow).
\end{equation*}

If the head of $M_o$ is in a state of the type $q_{i\to j}$, then it has simulated the current transition of $M$ and is returning now to the first cell in order to change its state to $q_j^R$.

\begin{equation*}
\forall s\in\Sigma_o\setminus\{\triangleright,\sqcup\} \; \bigl((q_{i\to j}^R, s)\to(q_{i\to j}^R, s,\rightarrow)\bigr),
\end{equation*}

\begin{equation*}
\forall s\in\Sigma_o\setminus\{\triangleright,\sqcup\} \; \bigl((q_{i\to j}^L,s)\to (q_{i\to j},s,\leftarrow)\bigr).
\end{equation*}

By construction, $M_o$ reaches the right end in one of the states of the type: $q_i^R, q_{i\to j}^R$, for some $i,j$. In this case, it pushes the right end one cell to the right by changing $\sqcup$ to $\sqcup'$ and starts moving to the left:

\begin{equation*}
(q_i^R,\sqcup)\to(q_i^L,\sqcup',\leftarrow),\; (q_{i\to j}^R, \sqcup)\to (q_{i\to j}^L, \sqcup',\leftarrow).
\end{equation*}

When it returns to the first cell, it turns into the state $q_j^R$ and moves to the right:

\begin{equation*}
(q_{i\to j}^L, \triangleright)\to (q_j^R, \triangleright,\rightarrow).
\end{equation*}

It remains to explain what $M_o$ does when the head of $M$ moves to the first cell. Consider the following situation, it is displayed on <Ref> on fig:oblivious_simulation1. The head of $M$ is in the second cell with a symbol $s$, being in the state $q_i$. Then it rewrites $s$ to $s'$, moves one cell to the left and arrives to the first cell being in the state $q_j$. And then it moves one cell to the right and turns into the state $q_k$. In total, there are two moves of the head of $M$. As each move of $M$ is associated with a walk of $M_o$ left-to-right and back, the head of $M_o$ must simulate these two moves with two walks. It starts the first walk at the first cell and turns into the state $q_i^R$. Then it passes the second cell from left to right and does nothing. Then it reaches the end of the tape and turns into the state $q_i^L$. When it visits the second cell again, it turns into the state $q_{i\to j(write)}^L$, rewrites $s^h$ to $s'$, and moves to the first cell. Then it acts according to the following rule:

\begin{equation*}
(q_{i\to j(write)}^L,\triangleright)\to (q_{j\to k(write)}^R,\triangleright,\rightarrow).
\end{equation*}

As it arrives to the second cell again, being in the state $q_{j\to k(write)}^R$, it has to rewrite $s'$ to $s^{\prime h}$, turn into the state $q_{j\to k}^R$ and continue walking to the right. When it arrives to the end of the tape, it turns into the state $q_{j\to k}^L$ and walks left. Eventually, it arrives to the first cell and turns into the state $q_k^R$. With this setting, one move of $M$ is associated with one left-right-left walk, thus, $M_o$ does not violate the obliviousness property.

Description of the $M_o$ simulation when the head of $M$ is at the first cell.

We have explained how $M_o$ executes. Every execution for the input of size $n$ will take the same amount of time $\func{g}(n)$ as the running time of the machine $M$ depends only on the size of the input. The movement of the head of $M_o$ is also the same for all input instances of the same size. We conclude that $M_o$ is oblivious. Moreover, $M_o$ is $\P$time equivalent to $M$, because if the input of $M_o$ is not of the form that fits $M$, then we reduce to a fixed YES instance of $M$, and if it is of the good form, then we reduce to the same input tape of $M$. The reduction from $M$ to $M_o$ is the identity.

<Ref> together imply <Ref>.

§ CONSTRUCTIONS AND PROOF OF <REF>

Let an oblivious Turing machine $M_o$ be the same as in the proof of <Ref>.

* $M_o$ has the alphabet $\Sigma_o:=\Sigma\uplus\{s^h\mid s\in\Sigma\setminus\{\triangleright,\sqcup\}\}\uplus\{\sqcup',\sqcup^{\prime h}\}$.

* It has the states $\family{Q}_o$: $q_{start},q_{search},q_{return}$ in $\family{Q}_o$;
* for every $q_i$ in $\family{Q}$, $q_i^L,q_i^R$ in $\family{Q}_o$;
* for every two distinct $q_i,q_j$ in $\family{Q}$, $q_{i\to j}^L,q_{i\to j}^R,q_{i\to j(write)}^L,q_{i\to j(write)}^R\in\family{Q}_o$;
* $\family{Q}_o$ contains all the $error$-copies of each of these states.

The input $\structure{A}$ of the $\MMSNPineq$ sentence $\Phi$ to be constructed shall be a canvas for a space-time diagram of a run of $M_o$.
The expressing power of the inequality allows us to forbid the structure $\structure{A}$ to be over-complete, that is, to have more than one tuple of the same relation that are incident to the same element. For example, by using of the inequality, we can require that all the out- and in-degrees of digraph elements are at most one.

However, we can not forbid the structure $\structure{A}$ to be incomplete, that is, not to have tuples where they ought to be.
This is because any $\MMSNPineq$ formula is monotone $\tau$-relations. For example, we can not require that all the out- and in-degrees are precisely one.

The main difficulty of the proof is to come up with an encoding that can be dealt with using the expressiveness of $\MMSNPineq$ when $\structure{A}$ is not of the correct form.

We are planning to construct $\Phi$ in $\MMSNPineq$ such that, for any input structure $\structure{A}$:

* if $\structure{A}$ is over-complete, then $\structure{A}\not\models\Phi$,

* if $\structure{A}$ is not complete enough to simulate a run of $M_o$, then $\structure{A}\models\Phi$,

* if $\structure{A}$ is in an appropriate form and can simulate a run of $M_o$ that returns YES, then $\structure{A}\models\Phi$,

* if $\structure{A}$ is in an appropriate form and can simulate a run of $M_o$ that returns NO, then $\structure{A}\not\models\Phi$.

By an appropriate form we mean the form of a two-dimensional(space-time) grid.
It is formed by horizontal $\rel{succ}$-arcs directed from left to right and by vertical $\rel{next}$-arcs directed from top to bottom.
Every row of this grid represents the tape at some moment of time $t$.
The row below is the tape at the next moment $t+1$, and the row above stands for the moment $t-1$.
Every element of a row is connected to the first and the last member of the row with a ternary relation $\rel{row}$, this will allow us to require some properties precisely from all the elements of the tape at some fixed moment of time.
The contents of the tape – the symbols, the states, the positions of the head – are encoded with both input and existential relations.

The input relations are represented by a signature $\tau$:

\begin{equation*}
\tau = \{\rel{s}(\cdot)\mid s\in\Sigma\}\uplus\{\rel{start}(\cdot), \rel{succ}(\cdot,\cdot), \rel{next}(\cdot,\cdot),\rel{row}(\cdot,\cdot,\cdot)\},
\end{equation*}

* $\rel{start}(x)$ represents a constant that highlights the grid element that is associated with the leftmost element of the tape, where the head must be at the start of the execution;

* $\rel{succ}(x,y)$ – a horizontal arc, it means that the cell corresponding to $y$ is the right neighbor of the cell corresponding to $x$ on the tape;

* $\rel{next}(x,x')$ – a vertical arc, it means that $x'$ represents some cell of the tape at the time $t$, and $x$ represents the same cell at the time $t+1$;

* $\rel{s}(x)$, for each $s$ in $\Sigma$, means that the symbol $s$ is written in the cell corresponding to an element $x$; these relations matter only in the first row, where they set the initial values for the corresponding existential relations;

* $\rel{row}(x,y,z)$ means that $y$ represents an element of a tape that starts at $x$ and ends at $z$.

The existential relations are represented by a signature $\sigma$.
All of them must be unary.
In order to distinguish $\tau$-relations from $\sigma$-relations, we write the name of each $\sigma$-relation with an initial upper case letter while every $\tau$-relation starts with a lower case letter.
This is convenient because there are both input and existential relations that describe symbols on the tape and that are named identically up to the letter case.

\begin{equation*}
\sigma = \{\rel{S}(\cdot)\mid s\in\Sigma_o\}\uplus\{\rel{Mark}(\cdot),\rel{H}(\cdot)\}\uplus \{\rel{Q}(\cdot)\mid q\in\family{Q}\},
\end{equation*}

* $\rel{S}(x)$, for $s$ in $\Sigma_o$, means that the cell corresponding to $x$ contains a symbol $s$;

* $\rel{Mark}(x)$ marks the elements that need to be considered;

* $\rel{Init}(x)$ highlights the elements corresponding to the initial configuration of the tape, it is used in order to generate all $\rel{Mark}$ elements;

* $\rel{H}(x)$ means that the head of $M_o$ is at the cell corresponding to $x$;

* $\rel{Q}(x)$ means that the cell corresponding to $x$ belongs to the tape at the moment of time when the machine is in the state $q$.

Below, we provide the conditions that force an element to be in $\rel{Mark}$.
We require that the elements of the first row are $\rel{Init}$, where the first row consists of all $x$ such that $\rel{row} (a,x,a')\wedge\rel{start}(a)$.
We demand every $\rel{Init}$ element to be in $\rel{Mark}$.
And then we force $\rel{Mark}$ relation to spread from an element to its bottom $\rel{next}$-neighbor if the structure contains all the necessary tuples around this point.

Simultaneously, we set the values for existential relations that are associated with alphabetical symbols as we do not want to have an $\rel{Init}$ element that is associated with a cell with no symbol. For any $s$ in $\Sigma$, we add the following conjuncts to $\Phi$:

\begin{multline*}
\rel{start}(a)\wedge\rel{succ}(a,x)\wedge\rel{next}(a,a')\wedge\rel{row}(a,x,a')\wedge\rel{s}(x)\to\\
\rel{Init}(x)\wedge\rel{S}(x)\wedge\rel{H}(x)\wedge\rel{Q}_{start}(x),
\end{multline*}

\begin{multline*}
\rel{start}(a)\wedge\rel{Init}(x)\wedge\rel{succ}(x,y)\wedge\rel{row}(a,y,a')\wedge\rel{next}(a,a')\wedge\rel{s}(y)\to\\
\rel{Init}(y)\wedge\rel{S}(y),
\end{multline*}

we require that every element of the row highlighted with $\rel{start}$ must be $\rel{Init}$, except for the $\rel{start}$ itself.
We also want the structure to be complete $\rel{row}$ and $\rel{next}$, , an element does not need to be $\rel{Init}$ if any such tuple is missing.
In the same rule we assign the existential symbol relations $\rel{S}(\cdot)$ depending on the input symbol relations $\rel{s}(\cdot)$, and also demand that the $\rel{H}$ is in the leftmost cell (the right $\rel{succ}$-neighbor of the $\rel{start}$ element) in the state $\rel{Q}_{start}$.
See <Ref> for a graphical representation.

A graphical representation of formulas that set the $\rel{Init}$ relation on the first row of the grid.
Arcs with black heads are $\rel{succ}$, arcs with white heads are $\rel{next}$, dashed closed curves are $\rel{row}$-triples, red squares are $\rel{start}$ elements, small white circles are $\rel{Init}$ elements, large white circles are $\rel{H}$ elements.
Relations $\rel{s}$ and $\rel{S}$ are implicit.

$\rel{Init}$ elements generate all the $\rel{Mark}$ elements. Firstly, we require that all the elements of the first row are $\rel{Mark}$: $\rel{Init}(x)\to\rel{Mark}(x)$.
Secondly, we force the relation $\rel{Mark}$ to spread from top to bottom via $\rel{next}$-arcs.
If the neighborhood of an element $y'$ has one of the four appropriate patterns from <Ref> and if its $\rel{next}$-predecessor $y$ is $\rel{Mark}$, then $y'$ must also be in $\rel{Mark}$.
It will be more convenient to display them as graphs, see <Ref>.
As the corresponding formulas are rather difficult to read.
We explicitly write only the rule corresponding to <Ref>.
It goes as follows.

\begin{equation*}
\left(
\begin{aligned}
& \rel{succ}(a,y)\wedge\rel{succ}(y,z)\wedge\rel{succ}(a',y')\wedge\rel{succ}   (y',z')\wedge\\
& \rel{next}(a,a')\wedge\rel{next}(y,y')\wedge\rel{next}(z,z')\wedge\rel{next}   (a',a'')\wedge\\
& \rel{row}(a,y,a')\wedge\rel{row}(a,z,a')\wedge\rel{row}   (a',y',a'')\wedge\\
& \rel{row}(a',z',a'')\wedge\rel{Mark}(y)\wedge\rel{Mark}(z)
\end{aligned}
\right)\to\rel{Mark}(y')
\end{equation*}

$y$ is the first element of the tape.
If $y,z$ are $\rel{Mark}$, then $y'$ has to be in $\rel{Mark}$.

The general case, when $y$ is in the middle of the tape.
If $x,y,z$ are $\rel{Mark}$, then $y'$ has to be in $\rel{Mark}$.

$y$ is at the end of the tape.
The head is not at $y$, this is highlighted with a cross.
Then, at the next moment of time, the tape will not be augmented.
If $x,y$ are $\rel{Mark}$, then $y'$ has to be in $\rel{Mark}$.

$y$ is at the end of the tape.
The head is at $y$, this is highlighted with a large circle.
Then the tape will be augmented with $z'$.
Both $y',z'$ have to be in $\rel{Mark}$ and the head has to move upon $x'$.

All the four cases when an element $y'$ is forced to become $\rel{Mark}$.
All the elements are required to be pairwise distinct, using $\not=$.
Black-headed arcs are $\rel{succ}$.
White-headed arcs are $\rel{next}$.
Dashed closed curves are $\rel{row}$.
Small white discs are $\rel{Mark}$ elements.

We want from the relations that represent the states to be a partition:

\begin{equation*}
\neg\left(\bigwedge_{q\in\family{Q}}\neg\rel{Q}(x)\right)\wedge\bigwedge_{q,q'\in\family{Q}}\neg\bigl(\rel{Q}(x)\wedge\rel{Q'}(x)\bigr),
\end{equation*}
and that two points at the same row of the grid(, from the tape at the same moment of time) can not have different states, thus, they are in precisely one state:

\begin{equation*}
\bigwedge_{q,q'\in\family{Q}}\neg\bigl(\rel{row}(a,x,a')\wedge\rel{row}(a,y,a')\wedge\rel{next}(a,a')\wedge\rel{Q}(x)\wedge\rel{Q'}(y)\bigr).
\end{equation*}

The relations $\rel{S}$, for $s$ in $\Sigma_o$, form a partition, as a cell can not contain two different symbols simultaneously:

\begin{equation*}
\neg\left(\bigwedge_{s\in\Sigma_o}\neg\rel{S}(x)\right)\wedge\bigwedge_{s,s'\in\Sigma_o}\neg\bigl(\rel{S}(x)\wedge\rel{S}'(x)\bigr).
\end{equation*}

The symbol predicates $\rel{S}(\cdot)$, for $s$ in $\Sigma_o\setminus\{\sqcup\}$, are propagated from top to bottom  when the predicate $\rel{H}$ is not upon the considered element.
These symbol predicates can change only when $\rel{H}$ is present.
This is because a machine can change the contents of the tape only with its head. For every $s$ in $\Sigma_o\setminus\{\sqcup\}$ and the corresponding relation $\rel{S}$ written in upper-case, we write:

\begin{equation}\label{eq:symbol_propagate}
\rel{Mark}(x)\wedge\neg\rel{H}(x)\wedge\rel{S}(x)\wedge\rel{next}(x,x')\to\rel{S}(x').
\end{equation}

We shall add constraints for  the $\rel{H}$  movement when we provide the formulas that describe the transitions of $M_o$.
There is only one other constraint for the $\rel{H}$ relation.
It states that at any moment of time there can not be two different cells of the tape where the $\rel{H}$ is at:

\begin{equation}\label{eq:head_unique}
\rel{row}(a,x,a')\wedge\rel{row}(a,y,a')\wedge\rel{next}(a,a')\wedge\rel{H}(x)\wedge\rel{H}(y)\to x=y.
\end{equation}

The head of $M_o$ is on the initial cell containing $\triangleright$ at the start.
We have one element to the left of $\triangleright$ in our structure so the conjunct will not be $\rel{start}(x)\to\rel{H}(x)$ but something morally similar.

A graphical representation of the formulas that describe the transition of $M_o$.
Horizontal black-headed arcs are $\rel{succ}$.
Vertical white-headed arcs are $\rel{next}$.
Dashed closed curves are $\rel{row}$-tuples.
Small white circles are $\rel{Mark}$ elements.
Medium white circles are $\rel{H}$ elements.
Large squares are existential symbol relations $\rel{S}$.
If two squares on the same figure have the same color, then they are associated with the same relation.
There is a letter $h$ near the square iff the corresponding symbol has the $h$-superscript.
A square with $\triangleright$ is associated with the first symbol relation $\triangleright(\cdot)$.
Squares with $\sqcup,\sqcup'$ are relations corresponding to the blank symbol that highlights the end of the tape and to the blank symbol that can be written in the middle of the tape.
Large circles stand for the state relations.
If two circles have the same color, then they are associated with the same relation.
A letter $w$ near the circle means that the head is in a state of the type $q_{i\to j(write)}$.
Symbols $\Leftarrow$ and $\Rightarrow$ near circles denote the direction of the walk.
A symbol $\Rightarrow$ between structures means that the left structure represented as the conjunction of all the corresponding atomic formulas implies any atomic formula that is present on the right structure and absent on the left.
Symbols $\vee\dots\vee$ mean that the structure on the left implies one of the structures on the right.

The formulas are displayed on <Ref>.
The figure has 6 lines.
Every line is associated with a class of head transitions.
Every such class is described by an implication between $ (\tau\uplus\sigma)$structures.
The caption of <Ref> explains the meaning of every detail of the figure.
We describe the transitions one by one.
Observe that in the base of every implication the element with the $\rel{H}$ is $\rel{Mark}$.
This means that if the $\rel{H}$ comes into an element that is not in $\rel{Mark}$, then no transition rule has to be used.

* The first line describes the case when the $\rel{H}$ is in the first cell.
The transition of $M_o$ is always deterministic when the first symbol $\triangleright$ is read.
During the transition the $\rel{H}$ writes the same symbol and then moves right.
The new state is uniquely determined by the state in which the machine was before the transition.
The corresponding rule of $M_o$ is of the following form: $(q_{i\to j}^L, \triangleright)\to(q_j^R, \triangleright,\rightarrow)$.
Below, we write the formula that is associated with this rule:

\begin{equation*} \left(
\begin{aligned}
&\rel{row}(a,y,a')\wedge\\ &\rel{succ}(a,y)\wedge\rel{succ}(y,z)\wedge\rel{succ}(a',y')\wedge\rel{succ}(y',z')\wedge\\ &\rel{next}(a,a')\wedge\rel{next}(y,y')\wedge\rel{next}(z,z')\wedge\\ &\rel{Mark}(y)\wedge\rel{H}(y)\wedge\rel{S}_\triangleright(y)\wedge\rel{Q}_{i\to j}^L(y)
\end{aligned} \right)\to\left(
\begin{aligned}
&\rel{S}_\triangleright(y')\wedge\\ &\rel{H}(z')\wedge\rel{Q}_j^R(z')
\end{aligned} \right).
\end{equation*}

For brevity, we write the formula only for one case, as, for other cases, the formulas can be written similarly.

* The second line describes the situation when the $\rel{H}$ is in the last cell.
By the form of the input tape, the last cell is the cell that contains the blank symbol $\sqcup$.
When the $\rel{H}$ of $M_o$ is reads $\sqcup$, then the transition is deterministic. For any possible state of $M_o$, the $\rel{H}$ rewrites $\sqcup$ to $\sqcup'$ and moves to the left.
The new state is uniquely determined by the previous state.
As the length of the grid increases every time when the head reaches its end, we also assign the relation $\sqcup(\cdot)$ to the newly added element.

* The third line contains two rules that are similar to each other.
They describe the case when the $\rel{H}$ reads a symbol in the middle of the tape that does not contain the $h$-superscript.
This means that the transition is deterministic: the $\rel{H}$ does not rewrite the symbol and keeps moving in the same direction.
This line also describes the situation when the $\rel{H}$ has done the transition and now is returning to the first cell in order to start a new tour.

* The fourth line is associated with the case when the $\rel{H}$ is moving towards the right end and reads a symbol with the $h$-superscript.
This means that it can imitate some of the transitions of the original Turing machine $M$, where the $\rel{H}$ moves to the right.
In this case, the $\rel{H}$ of $M_o$ has a choice: either to continue moving further and imitate the transition when it visits this cell for the second time, or to imitate one of the transitions.
If it decides to imitate them now, then it rewrites the symbol according to the transition, and turns into a state of the type $q_{i\to j(write)}$ in order to add the $h$-superscript to the next symbol.

* The fifth line is associated with the case when the $\rel{H}$ is moving towards the left end and reads a symbol with the $h$-superscript.
This case is similar to the fourth line, but now the $\rel{H}$ can not do nothing and keep moving.
It is the last time when it visits this cell, so it has to do the transition now.

* The sixth line contains two similar rules.
Each of them is associated with the case when the $\rel{H}$ is in a state of the type $q_{i\to j(write)}$ and it reads a symbol without the $h$-superscript.
In this case, it adds the $h$-superscript to the symbol highlighting that the head of the original machine $M$ changes its position.
After doing this it keeps moving to the same direction.

We have described how to represent the transition rules of $M_o$ in the language of $\MMSNPineq$.
We know that $M_o$ rejects the input if at the end of the execution it is in a rejecting state.
We are going to reject the structure if, for some point $x$, it has both $\rel{H}$ and $\rel{Q}_{reject}$ at this point (for any $\rel{Q}_{reject}$ that is associated with a rejecting state of $\family{Q}$):

\begin{equation}\label{eq:rejecting_state}
\neg\bigl(\rel{Mark}(x)\wedge\rel{H}(x)\wedge\rel{Q}_{reject}(x)\bigr)
\end{equation}

There exists a $\P$time reduction $\func{r}_1$ from $\Omega$ to $\Sat(\Phi)$.

For a tape of length $n$, we reduce to a grid that consists of $\func{g}(n)+1$ rows, where $\func{g}(n)$ is the running time of $M_o$.
The horizontal arcs are $\rel{succ}$, the vertical are $\rel{next}$, each element of the row is connected by $\rel{row}$ with the start of this row and with the start of the next row.
The start of a row is the $\rel{succ}$-successor of the end of the precedent row.
As every time the the head reaches the right end of the tape, it extends the tape by one cell, we need to augment the length of each row by $1$ every time the head reaches its end.
So, the first $n$ rows of the grid have length $n$, the next $2(n+1)$ rows have length $n+1$, and so on.
The top-left element of the grid has the predicate $\rel{start}$.
And the elements of the first row have predicates from $\{s(\cdot)\mid s\in\Sigma_o\}$ that are associated with symbols in the cells of the tape.
Such a grid is displayed on <Ref>.

An example of the grid that is associated with the tape of $M_o$.
The horizontal arcs are $\rel{succ}$, the red square element is the $\rel{start}$.
All tuples of the relation $\rel{row}$ and the symbol relations $\rel{s}(\cdot)$ are not drawn in order to make the figure look less complex.

By the construction of $\Phi$ and the construction of the grid, every grid element has to be in $\rel{Mark}$ unless it is the leftmost element of a row.
For the predicate $\rel{H}$ there is only one possible interpretation on the set of $\rel{Mark}$ elements.
See <Ref>.

The coloring of the grid from <Ref> with the predicates $\rel{Mark}$(small white circles) and $\rel{H}$(large white circles).

As any element that is associated with a cell of the tape is $\rel{Mark}$ and as the $\rel{H}$ movement coincides with the one of $M_o$, we conclude that this grid is accepted by $\Phi$ iff all the conjuncts from <ref> are satisfied.
That is, iff $M_o$ does not reject its input tape.
This proves the reduction.

§ PROOF OF <REF>

For any $\tau$-structure $\structure{B}$ there exists an input string $\tuple{x}\in(\Sigma_o\setminus\{\sqcup\})^\ast$ such that $\tuple{x}$ is computed in Ptime in $|B|$ and $\structure{B}\models\Phi$ iff $M_o$ accepts $\tuple{x}$.

We need to show the other direction of $\P$time equivalence.
That is, for any relational $\tau$-structure, either we need to solve $\Sat(\Phi)$ in time polynomial in the structure size  or we need to reduce this $\tau$-structure to an equivalent tape of $M_o$.

In order to do this we have to treat all the input that does not look like a grid from <Ref>.
We are going to use $\not=$ to forbid all the inputs that are over-complete.
Informally speaking, $\not=$ helps us to forbid degrees two or more and to forbid two or more appearances of a predicate.

Let us list these conditions, which are displayed on <Ref>:

* there can be at most one point highlighted with $\rel{start}$:

\begin{equation*}
\neg(\rel{start}(x)\wedge\rel{start}(y)\wedge x\not=y),
\end{equation*}

* every element may have at most one in-neighbor and at most one out-neighbor $\rel{succ}$ and $\rel{next}$:

\begin{equation*}
\neg(\rel{succ}(x,y)\wedge\rel{succ} (x,y')\wedge y\not=y'),\;\neg(\rel{succ}(x,y)\wedge\rel{succ} (x',y)\wedge x\not=x'),\;
\end{equation*}

\begin{equation*}
\neg(\rel{next}(x,y)\wedge\rel{next}(x,y')\wedge y\not=y'), \; \neg(\rel{next} (x,y)\wedge\rel{next}(x',y)\wedge x\not=x'),
\end{equation*}

* every element can not belong to several tapes at the same time, that is, it can participate in at most one $\rel{row}$-tuple:

\begin{equation*}
\neg(\rel{row}(x,y,z)\wedge\rel{row} (x',y,z')\wedge x\not=x'),
\end{equation*}

\begin{equation*}
\neg(\rel{row}(x,y,z)\wedge\rel{row}(x',y,z')\wedge z\not=z'),
\end{equation*}

* if an element is on the $1$st or on the $3$rd coordinate in a $\rel{row}$-tuple, then it can not be on the second coordinate of another  $\rel{row}$-tuple:

\begin{equation*}
\neg\bigl(\rel{row}(a,x,b)\wedge\rel{row} (a',a,b')\bigr),\;\neg\bigl(\rel{row}(a,x,b)\wedge\rel{row} (a',b,b')\bigr),
\end{equation*}

* loops of any kind are forbidden:

\begin{equation*}
\neg\rel{succ}(x,x),\;\neg\rel{next} (x,x'),\;\neg\rel{row}(a,x,a),
\end{equation*}

* a point can belong to at most one symbol relation, that is, for each $s,s'$ in $\Sigma_o$, we add $\neg\bigl(\rel{s}(x)\wedge\rel{s}' (x)\bigr).$

A graphical representation of forbidden conjunctions.
Red squares are $\rel{start}$ elements.
Arcs with black heads are $\rel{succ}$-arcs.
Arcs with white heads are $\rel{next}$-arcs.
Closed curves are $\rel{row}$-triples.
Red and blue disks are different input symbol relations $\rel{s},\rel{s}'$.

Observe that grids corresponding to tapes satisfy all these sentences.
Thus, if we add them to $\Phi$, the reduction from $\NP$ to $\MMSNPineq$ still works correctly.

For some input $\tau$-structure $\structure{A}$, we first check if it omits all the forbidden patterns from <Ref>.
If it does, then we can understand which elements must be in $\rel{Mark}$, and at which elements the $\rel{H}$ has to be.
We shall argue that one needs to consider the minimal by inclusion interpretations of the $\rel{Mark}$ and $\rel{H}$ relations. For an oblivious Turing machine, we know exactly how much time we do need to finish the execution.
Thus, we can just  see if the size of the substructure induced on $\rel{Mark}$ elements is large enough to achieve it.
If the size is not large enough, then we are certain that the head never reaches a rejecting state, thus, all the conjuncts of $\Phi$ are satisfied.
In this case, we reduce the structure to some input instance of $M_o$ that is accepted by the machine.
If the substructure induced on $\rel{Mark}$ elements is sufficiently large to finish the execution, then the input instance of $M_o$ is provided by the first row of the grid.

It takes $\P$time to check if the input structure $\structure{A}$ of $\Sat(\Phi)$ satisfies conditions given on <Ref> as they all are first-order formulas.
If it is rejected, then we reduce it to some input instance rejected by $M_o$.
If not, then we use the following claim in order to understand which elements of $\structure{A}$ must be in $\rel{Mark}$ and reconstruct the movement of the $\rel{H}$.

Among all valid interpretations of the relations $\rel{Mark}$ and $\rel{H}$ there exist unique minimal by inclusion interpretations, and, if $\Phi$ holds on $\structure{A}$, then there exists a valid assignment of $\sigma$-relations such that $\rel{Mark}^\structure{A}$ and $\rel{H}^\structure{A}$ are minimal by inclusion.

Denote by $a_0$ an element of $\structure{A}$ such that $\rel{start}(a_0)$; if such element does not exist, then no element is forced to be in $\rel{Mark}$.
Denote by $C_m\subseteq A$ the set of elements that are forced to be in $\rel{Mark}$.
It is defined inductively. Firstly, we add to $C_m$ the right $\rel{succ}$-neighbor of $a_0$; then we put the neighbor of the neighbor and so on, by using the formulas from <Ref>.
Eventually, we add all the elements that are forced to be $\rel{Init}$.
Then, we use the formulas from <Ref> and add every element that is forced to be in $\rel{Mark}$ by one of the rules.
Repeat this until no more element can be added.

We now know that in- and out-degrees of $\rel{succ}$- and $\rel{next}$-arcs of $\structure{A}$ are at most one.
Thus, we can assign to every element of $C_m$ a pair of natural numbers.
Assign $(1,0)$ to the right $\rel{succ}$-neighbor of the $\rel{start}$, assign $(2,0)$ to the neighbor of the neighbor, and so on. For the bottom $\rel{next}$-neighbor of $(i,j)$, we assign $(i,j+1)$.
One can prove by induction that, for any $x,y$ in $ C_m$ with coordinates $(i_x,j_x),(i_y,j_y)$, we have $\rel{succ}^\structure{A} (x,y)$ iff $i_x+1=i_y$ and $j_x=j_y$; also, a similar statement is true for $\rel{next}$-arcs, and for $\rel{row}$-triples as well: $x$ and $y$ are on the same row iff $j_x=j_y$.

We show that any interpretation $\rel{Mark}^\structure{A}$ either contains $C_m$ as a subset or does not satisfy $\Phi$.
If there is $x$ in $ C_m$ such that $x\not\in\rel{Mark}^\structure{A}$, then choose such $x$ that is added to $C_m$ at the earliest possible moment.
Then, as $x$ is not $\rel{Mark}$, it does not satisfy one of the formulas from <Ref>, as all its predecessors are $\rel{Mark}$.

Suppose that $\structure{A}\models\Phi$ and $\rel{Mark}^\structure{A}=B$ is the interpretation of a solution.
We show now that if we set $\rel{Mark}^\structure{A} = C_m$, then this assignment is still valid.
Suppose that it is not valid, thus, some conjunct of $\Phi$ is false.
It can not be a rule from <Ref>, as $C_m$ satisfies them.
And there are no conjuncts with an atomic $\rel{Mark}$ formula that has an even number of negations before it.
This means that all other conjuncts can not be violated because of the $\rel{Mark}$ relation.
All other relations are the same, so we conclude that $\Phi$ is also satisfied when $\rel{Mark}^\structure{A}=C_m$.
We have proved that we can assume that the relation $\rel{Mark}$ is interpreted as the minimal possible one.

Now we proceed similarly for the relation $\rel{H}$.
We define a set $C_h$ as follows. Firstly, add the right $\rel{succ}$-neighbor of $a_0$ to $C_h$ (only if it belongs to $C_m$).
Then, follow the rules that are responsible for the head movement, , those that simulate the transitions of the Turing machine displayed on <Ref>.
Recall that any transition rule is fired only if the current $\rel{H}$ element is $\rel{Mark}$; also recall that the movement of the $\rel{H}$ is unambiguous.
This means that there is at most one $\rel{H}$ element that is not in $C_m$: it is the last element that is added to $C_h$.

Similarly as for $C_m$, for any interpretation $\rel{H}^\structure{A}$, either $C_h\subseteq\rel{H}^\structure{A}$ or a rule of $\Phi$ that describes the transition is not satisfied in $\structure{A}$.

Suppose that there is a valid assignment for the existential relations of $\Phi$, where $\rel{H}^\structure{A} = B\supsetneq C_h$.
We show now that if we set $\rel{H}^\structure{A} = C_h$, then the assignment is still valid.
Suppose that it is not valid when $\rel{H}^\structure{A}=C_h$; then there is a conjunct of $\Phi$ that is not satisfied.
This conjunct contains a $\rel{H}$-atom that is true when $\rel{H}^\structure{A}=B$ and that is false when $\rel{H}^\structure{A} = C_h$.
This means that this atom has an even number of negations before it.
The only conjunct that can be false and that has a $\rel{H}$-atom is <ref>, it means that, if there is no $\rel{H}$ at a cell, then this cell contains the same symbol as before at the next moment of time.
This means that, when $\rel{H}^\structure{A}=B$, it can put the head where it is not supposed to be and change the symbol written on the tape such that the $\rel{H}$ is never in a rejecting state.
But this is not allowed for elements of $C_m$, by <ref>, that forbids the head $\rel{H}$ to appear at two different elements of the same row.
Thus, in the case when $\rel{H}^\structure{A} =B$, changing a symbol on the tape does not change the rejecting state of the machine at the last point of $C_h$.
See <Ref> for a graphical representation of this proof.

The substructure of $\structure{A}$ induced on $C_m$.
The red square is $\rel{start}$, horizontal arcs are $\rel{succ}$, vertical are $\rel{next}$.
White circles with black boundaries are the elements of $C_h$.
White circles with red boundaries are the elements of $B\setminus C_h$.
Thick red line highlights the moment of time when the execution of $M_o$ stops.
There can not be an element of $B\setminus C_h$ above this red line.
The region where they could be is highlighted with grey.

Proof of <Ref>.
We know now that we can interpret $\rel{Mark}$ and $\rel{H}$ as $C_m$ and $C_h$.
We can construct these two sets in time linear of the size of $\structure{A}$.
We know that $M_o$ decides an input of size $n$ in exactly $\func{g}(n)$ steps.
The size of the input is equal to $N=\max\{i\mid(i,0)\in C_m\}$.
Then we see if $C_h\cap C_m$ contains an element with its second coordinate equal to $\func{g}(N)$.
If it does, then we know that the structure is large enough to simulate the execution of $M_o$, and we associate it with a string of symbols written in cells $(1,0),\ldots, (N,0)$.
Otherwise any element of $C_h\cap C_m$ has a too small second coordinate, so no negated conjunct of the following type can be false:

\begin{equation*}
\neg\bigl(\rel{Mark}(x)\wedge\rel{H}(x)\wedge\rel{Q}_{reject}(x)\bigr).
\end{equation*}

This means that $\structure{A}\models\Phi$, and we associate with $\structure{A}$ some YES instance of $M_o$.

Why oblivious Turing machines are necessary?

In this paragraph we explain why the proof of <Ref> works only for oblivious Turing machines.
We use this property in the proof of <Ref>, where we reduce $\MMSNPineq$ back to $\NP$.
Suppose that the Turing machine is not oblivious; then the head movements and the execution time can be arbitrary.
We can make the input to look like a two-dimensional grid.
But we can not manipulate its height (the number of rows) and width (the number of columns).
If the Turing machine is oblivious, then we know the exact head movement and the time of the execution.
Consider two grids that are displayed on <Ref>.
If the head movement is oblivious, then it will perform as we expect, for every grid that is in a good form.
If the grid is too short in terms of height and width, then the execution will not be finished, then the rejecting state will never be reached, this means that such short input will never be rejected.
However, if the movement is not oblivious, then, for some input string, it can be rejected arbitrarily quickly.
This means that we can not predict if a short grid is large enough to imitate the whole execution leading to a rejecting state.
The right two-dimensional grid is an example of a short grid: the red dashed line marks the boundary, everything beyond it is deleted.
The white circles mark the head movement.
The execution time is small enough to reject the input encoded in the first row.

On the left, there is a space-time grid in a good form.
On the right, there is a space-time grid in a bad form.