ASNP: A Tame Fragment of Existential SecondOrder Logic
 37 Downloads
Abstract
Amalgamation SNP (ASNP) is a fragment of existential secondorder logic that strictly contains binary connected MMSNP of Feder and Vardi and binary connected guarded monotone SNP of Bienvenu, ten Cate, Lutz, and Wolter; it is a promising candidate for an expressive subclass of NP that exhibits a complexity dichotomy. We show that ASNP has a complexity dichotomy if and only if the infinitedomain dichotomy conjecture holds for constraint satisfaction problems for firstorder reducts of binary finitely bounded homogeneous structures. For such CSPs, powerful universalalgebraic hardness conditions are known that are conjectured to describe the border between NPhard and polynomialtime tractable CSPs. The connection to CSPs also implies that every ASNP sentence can be evaluated in polynomial time on classes of finite structures of bounded treewidth. We show that the syntax of ASNP is decidable. The proof relies on the fact that for classes of finite binary structures given by finitely many forbidden substructures, the amalgamation property is decidable.
1 Introduction
Feder and Vardi in their groundbreaking work [15] formulated the famous dichotomy conjecture for finitedomain constraint satisfaction problems, which has recently been resolved [11, 26]. Their motivation to study finitedomain CSPs was the question which fragments of existential secondorder logic might exhibit a complexity dichotomy in the sense that every problem that can be expressed in the fragment is either in P or NPcomplete. Existential secondorder logic without any restriction is known to capture NP [14] and hence does not have a complexity dichotomy by an old result of Ladner [24]. Feder and Vardi proved that even the fragments of monadic SNP and monotone SNP do not have a complexity dichotomy since every problem in NP is polynomialtime equivalent to a problem that can be expressed in these fragments. However, the dichotomy for finitedomain CSPs implies that monotone monadic SNP (MMSNP) has a dichotomy, too [15, 23].
MMSNP is also known to have a tight connection to a certain class of infinitedomain CSPs [7]: an MMSNP sentence is equivalent to a connected MMSNP sentence if and only if it describes an infinitedomain CSP. Moreover, every problem in MMSNP is equivalent to a finite disjunction of connected MMSNP sentences. The infinite structures that appear in this connection are tame from a modeltheoretic perspective: they are reducts of finitely bounded homogeneous structures (see Sect. 4.1). CSPs for such structures are believed to have a complexity dichotomy, too; there is even a known hardness condition such that all other CSPs in the class are conjectured to be in P [8]. The hardness condition can be expressed in several equivalent forms [1, 2].
In this paper we investigate another candidate for an expressive logic that has a complexity dichotomy. Our minimum requirement for what constitutes a logic is relatively liberal: we require that the syntax of the logic should be decidable. The same requirement has been made for the question whether there exists a logic that captures the class of polynomialtime solvable decision problems (see, e.g., [19, 20]). The idea of our logic is to modify monotone SNP so that only CSPs for modeltheoretically tame structures can be expressed in the logic; the challenge is to come up with a definition of such a logic which has a decidable syntax. We would like to require that the (universal) firstorder part of a monotone SNP sentence describes an amalgamation class. We mention that the Joint Embedding Property (JEP), which follows from the Amalgamation Property (AP), has recently been shown to be undecidable [10]. In contrast, we use the fact that the AP for binary signatures is decidable (Sect. 5). We call our new logic Amalgamation SNP (ASNP). This logic contains binary connected MMSNP; it also contains the more expressive logic of binary connected guarded monotone SNP. Guarded monotone SNP (GMSNP) has been introduced in the context of knowledge representation [3] (see Sect. 6). We show that ASNP has a complexity dichotomy if and only if the infinitedomain dichotomy conjecture holds for constraint satisfaction problems for firstorder reducts of binary finitely bounded homogeneous structures. In particular, every problem that can be expressed in ASNP is a CSP for some countably infinite \(\omega \)categorical structure \(\mathfrak {B}\). In Sect. 7 we present an example application of this fact: every problem that can be expressed in one of these logics can be solved in polynomial time on instances of bounded treewidth.
2 Constraint Satisfaction Problems
Let \(\mathfrak {A},\mathfrak {B}\) be structures with a finite relational signature \(\tau \); each symbol \(R \in \tau \) is equipped with an arity \({{\,\mathrm{ar}\,}}(R) \in {\mathbb N}\). A function \(h :A \rightarrow B\) is called a homomorphism from \(\mathfrak {A}\) to \(\mathfrak {B}\) if for every \(R \in \tau \) and \((a_1,\dots ,a_{{{\,\mathrm{ar}\,}}(R)}) \in R^{\mathfrak {A}}\) we have \((h(a_1),\dots ,h(a_{{{\,\mathrm{ar}\,}}(R)})) \in R^{\mathfrak {B}}\); in this case we write \(\mathfrak {A}\rightarrow \mathfrak {B}\). We write \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) for the class of all finite \(\tau \)structures \(\mathfrak {A}\) such that \(\mathfrak {A}\rightarrow \mathfrak {B}\).
Example 1
If \(\mathfrak {B}= K_3\) is the 3clique, i.e., the complete undirected graph with three vertices, then \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) is the graph 3colouring problem, which is NPcomplete [18].
Example 2
If \(\mathfrak {B}= ({\mathbb Q};<)\) then \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) is the digraph acyclicity problem, which is in P.
Example 3
If \(\mathfrak {B}= ({\mathbb Q};{{\,\mathrm{Betw}\,}})\) for \({{\,\mathrm{Betw}\,}}:= \{(x,y,z) \mid x< y< z \vee z< y < x \}\) then \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) is the Betweenness problem, which is NPcomplete [18].
A homomorphism h from \(\mathfrak {A}\) to \(\mathfrak {B}\) is called an embedding of \(\mathfrak {A}\) into \(\mathfrak {B}\) if h is injective and for every \(R \in \tau \) and \(a_1,\dots ,a_{{{\,\mathrm{ar}\,}}(R)} \in A\) we have \((a_1,\dots ,a_{{{\,\mathrm{ar}\,}}(R)}) \in R^{\mathfrak {A}}\) if and only if \((h(a_1),\dots ,h(a_{{{\,\mathrm{ar}\,}}(R)})) \in R^{\mathfrak {B}}\); in this case we write \(\mathfrak {A}\hookrightarrow \mathfrak {B}\). The union of two \(\tau \)structures \(\mathfrak {A},\mathfrak {B}\) is the \(\tau \)structure \(\mathfrak {A}\cup \mathfrak {B}\) with domain \(A \cup B\) and the relation \(R^{\mathfrak {A}\cup \mathfrak {B}} := R^{\mathfrak {A}}\cup R^{\mathfrak {B}}\) for every \(R\in \tau \). The intersection \(\mathfrak {A}\cap \mathfrak {B}\) is defined analogously. A disjoint union of \(\mathfrak {A}\) and \(\mathfrak {B}\) is the union of isomorphic copies of \(\mathfrak {A}\) and \(\mathfrak {B}\) with disjoint domains. As disjoint unions are unique up to isomorphism, we usually speak of the disjoint union of \(\mathfrak {A}\) and \(\mathfrak {B}\), and denote it by \(\mathfrak {A}\uplus \mathfrak {B}\). A structure is connected if it cannot be written as a disjoint union of at least two structures with nonempty domain. A class of structures \(\mathcal C\) is closed under inverse homomorphisms if whenever \(\mathfrak {B}\in {\mathcal C}\) and \(\mathfrak {A}\) homomorphically maps to \(\mathfrak {B}\) we have \(\mathfrak {A}\in {\mathcal C}\). If \(\tau \) is a finite relational signature, then it is wellknown and easy to see [5] that \({\mathcal C} = {{\,\mathrm{CSP}\,}}(\mathfrak {B})\) for a countably infinite \(\tau \)structure \(\mathfrak {B}\) if and only if \(\mathcal C\) is closed under inverse homomorphisms and disjoint unions.
3 Monotone SNP
Example 4
A class \(\mathcal C\) of finite \(\tau \)structures is said to be in SNP if there exists an SNP \(\tau \)sentence \(\varPhi \) such that \([\![\varPhi ]\!]= {\mathcal C}\); we use analogous definitions for all logics considered in this paper. We may assume that the quantifierfree part of SNP sentences is written in conjunctive normal form, and then use the usual terminology (clauses, literals, etc).
Definition 1
monotone if each literal of \(\phi \) with a symbol from \(\tau \) is negative, i.e., of the form \(\lnot R(\bar{x})\) for \(R \in \tau \).
monadic if all the existentially quantified relations are unary.
connected if each clause of \(\phi \) is connected, i.e., the following \(\tau \cup \sigma \)structure \(\mathfrak {C}\) is connected: the domain of \(\mathfrak {C}\) is the set of variables of the clause, and \(t \in R^{\mathfrak {C}}\) if and only if \(\lnot R(t)\) is a disjunct of the clause.
The SNP sentence from Example 4 is monotone, but not monadic, and it can be shown that there does not exist an equivalent MMSNP sentence [4].
Theorem 1
([5]). Every sentence in connected monotone SNP describes a problem of the form \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) for some relational structure \(\mathfrak {B}\). Conversely, for every structure \(\mathfrak {B}\), if \({{\,\mathrm{CSP}\,}}(\mathfrak {B})\) is in SNP then it is also in connected monotone SNP.
4 Amalgamation SNP
In this section we define the new logic Amalgamation SNP (ASNP). We first revisit some basic concepts from model theory.
4.1 The Amalgamation Property
the Joint Embedding Property (JEP) if for all structures \(\mathfrak {B}_1,\mathfrak {B}_2 \in {\mathcal C}\) there exists a structure \(\mathfrak {C}\in {\mathcal C}\) that embeds both \(\mathfrak {B}_1\) and \(\mathfrak {B}_2\).
the Amalgamation Property (AP) if for any two structures \(\mathfrak {B}_1,\mathfrak {B}_2 \in {\mathcal C}\) such that \(B_1 \cap B_2\) induce the same substructure in \(\mathfrak {B}_1\) and in \(\mathfrak {B}_2\) (a socalled amalgamation diagram) there exists a structure \(\mathfrak {C}\in {\mathcal C}\) and embeddings \(e_1 :\mathfrak {B}_1 \hookrightarrow \mathfrak {C}\) and \(e_2 :\mathfrak {B}_2 \hookrightarrow \mathfrak {C}\) such that \(e_1(a) = e_2(a)\) for all \(a \in B_1 \cap B_2\).
Note that since \(\tau \) is relational, the AP implies the JEP. A class of finite \(\tau \)structures which has the AP and is closed under induced substructures and isomorphisms is called an amalgamation class.
The age of \(\mathfrak {B}\) is the class of all finite \(\tau \)structures that embed into \(\mathfrak {B}\). We say that \(\mathfrak {B}\) is finitely bounded if \({{\,\mathrm{Age}\,}}(\mathfrak {B})\) is finitely bounded. A relational \(\tau \)structure \(\mathfrak {B}\) is called homogeneous if every isomorphism between finite substructures of \(\mathfrak {B}\) can be extended to an automorphism of \(\mathfrak {B}\). Fraïssé’s theorem implies that for every amalgamation class \(\mathcal C\) there exists a countable homogeneous \(\tau \)structure \(\mathfrak {B}\) with \({{\,\mathrm{Age}\,}}(\mathfrak {B}) = {\mathcal C}\); the structure \(\mathfrak {B}\) is unique up to isomorphism, also called the Fraïssélimit of \(\mathcal C\). Conversely, it is easy to see that the age of a homogeneous \(\tau \)structure is an amalgamation class. A structure \(\mathfrak {A}\) is called a reduct of a structure \(\mathfrak {B}\) if \(\mathfrak {A}\) is obtained from \(\mathfrak {B}\) by restricting the signature. It is called a firstorder reduct of \(\mathfrak {B}\) if \(\mathfrak {A}\) is obtained from \(\mathfrak {B}\) by first expanding by all firstorder definable relations, and then restricting the signature. An example of a firstorder reduct of \(({\mathbb Q};<)\) is the structure \(({\mathbb Q};{{\,\mathrm{Betw}\,}})\) from Example 3.
4.2 Defining Amalgamation SNP
As we have mentioned in the introduction, the idea of our logic is to require that a certain class of finite structures associated to the firstorder part of an SNP sentence is an amalgamation class. We then use the fact that for binary signatures, the amalgamation property is decidable (Sect. 5).
Definition 2
\(R_1,\dots ,R_k\) are binary;
\(\phi \) is a conjunction of \(\{R_1,\dots ,R_k\}\)formulas and of conjuncts of the form \(S(x_1,\dots ,x_k) \Rightarrow \psi (x_1,\dots ,x_k)\) where \(S \in \tau \) and \(\psi \) is a \(\{R_1,\dots ,R_k\}\)formula;
the class of \(\{R_1,\dots ,R_k\}\)reducts of the finite models of \(\phi \) is an amalgamation class.
Note that ASNP inherits from SNP the restriction that equality symbols are not allowed. Also note that Amalgamation SNP sentences are necessarily monotone. This implies in particular that the class of \(\{R_1,\dots ,R_k\}\)reducts of the finite models of \(\phi \) is precisely the class of finite \(\{R_1,\dots ,R_k\}\)structures that satisfy the conjuncts of \(\phi \) that are \(\{R_1,\dots ,R_k\}\)formulas (i.e., that do not contain any symbol from \(\tau \)).
Example 5
Then the class of finite models of the firstorder part of \(\varPhi \) has the JEP, and since equality is not allowed in SNP the class is even closed under disjoint unions; it follows that also \(\varPhi \) is closed under disjoint unions. It can be shown as in the proof of Theorem 1 that every Amalgamation SNP sentence can be rewritten into an equivalent connected Amalgamation SNP sentence.
4.3 ASNP and CSPs
We present the link between ASNP and infinitedomain CSPs.
Theorem 2
For every ASNP \(\tau \)sentence \(\varPhi \) there exists a firstorder reduct \(\mathfrak {C}\) of a binary finitely bounded homogeneous structure such that \({{\,\mathrm{CSP}\,}}(\mathfrak {C}) = [\![\varPhi ]\!]\).
Proof
Let \(\rho \) be the set of existentially quantified relation symbols of \(\varPhi \). Let \(\phi = \forall x_1,\dots ,x_n :\psi \), for a quantifierfree formula \(\psi \) in conjunctive normal form, be the firstorder part of \(\varPhi \). Let \(\mathcal C\) be the class of \(\rho \)reducts of the finite models of \(\phi \); by assumption, \(\mathcal C\) is an amalgamation class. Moreover, \(\mathcal C\) is finitely bounded because it is the class of models of a universal \(\rho \)sentence. Let \(\mathfrak {B}\) be the Fraïssélimit of \(\mathcal C\); then \(\mathfrak {B}\) is a finitely bounded homogeneous structure. Let \(\mathfrak {C}\) be the \(\tau \)structure which is the firstorder reduct of the structure \(\mathfrak {B}\) where the relation \(S^{\mathfrak {C}}\) for \(S \in \tau \) is defined as follows: if \(\phi _1,\dots ,\phi _s\) are all the \(\rho \)formulas such that \(\psi \) contains the conjunct \(S(x_1,\dots ,x_k) \Rightarrow \phi _i(x_1,\dots ,x_k)\) for all \(i \in \{1,\dots ,s\}\), then the firstorder definition of S is given by \(S(x_1,\dots ,x_k) \Leftrightarrow (\phi _1 \wedge \dots \wedge \phi _s)\).
Claim 1
If \(\mathfrak {A}\) is a finite \(\tau \)structure such that \(\mathfrak {A}\rightarrow \mathfrak {C}\), then \(\mathfrak {A}\models \varPhi \).
Let \(h :\mathfrak {A}\rightarrow \mathfrak {C}\) be a homomorphism. Let \(\mathfrak {A}'\) be the \((\tau \cup \rho )\)expansion of \(\mathfrak {A}\) where \(R \in \rho \) of arity l denotes \(\{(a_1,\dots ,a_l) \mid (h(a_1),\dots ,h(a_l)) \in R^{\mathfrak {B}} \}\). Then \(\mathfrak {A}'\) satisfies \(\phi \): to see this, let \(a_1,\dots ,a_n \in A\) and let \(\psi '\) be a conjunct of \(\psi \). Since \(\mathfrak {C}\models \forall x_1,\dots ,x_n :\psi \) we have in particular that \(\mathfrak {C}\models \psi '(h(a_1),\dots ,h(a_n))\) and so there must be a disjunct \(\psi ''\) of \(\psi '\) such that \(\mathfrak {C}\models \psi ''(h(a_1),\dots ,h(a_n))\). Then one of the following cases applies.

\(\psi ''\) is a \(\tau \)literal and hence must be negative since \(\varPhi \) is a monotone SNP sentence. In this case \(\mathfrak {C}\models \psi ''(h(a_1),\dots ,h(a_n))\) implies \(\mathfrak {A}' \models \psi ''(a_1,\dots ,a_n)\) since h is a homomorphism.

\(\psi ''\) is a \(\rho \)literal. Then by the definition of \(\mathfrak {A}'\) we have that \(\mathfrak {A}' \models \psi ''(a_1,\dots ,a_n)\) if and only if \(\mathfrak {C}\models \psi ''(h(a_1),\dots ,h(a_n))\).
Hence, \(\mathfrak {A}' \models \psi '(a_1,\dots ,a_n)\). Since the conjunct \(\psi '\) of \(\psi \) and \(a_1,\dots ,a_n \in A\) were arbitrarily chosen, we have that \(\mathfrak {A}' \models \forall x_1,\dots ,x_n :\psi \). Hence, \(\mathfrak {A}\) satisfies \(\varPhi \).
Claim 2
If \(\mathfrak {A}\) is a finite \(\tau \)structure such that \(\mathfrak {A}\models \varPhi \), then \(\mathfrak {A}\rightarrow \mathfrak {C}\).
If \(\mathfrak {A}\) has a \((\tau \cup \rho )\)expansion \(\mathfrak {A}'\) that satisfies \(\phi \), then there exists an embedding from the \(\rho \)reduct \(\mathfrak {A}''\) of \(\mathfrak {A}'\) into \(\mathfrak {B}\) by the definition of \(\mathfrak {B}\). This embedding is in particular a homomorphism from \(\mathfrak {A}\) to \(\mathfrak {C}\). \(\square \)
Theorem 3
Let \(\mathfrak {C}\) be a firstorder reduct of a binary finitely bounded homogeneous structure \(\mathfrak {B}\). Then \({{\,\mathrm{CSP}\,}}(\mathfrak {C})\) can be expressed in ASNP.
Proof
replacing each occurrence of the equality symbol by the symbol \(E \in \sigma \);
joining conjuncts that imply that E denotes an equivalence relation;
 joining for every \(R \in \sigma \) of arity n the conjunct(implementing indiscernibility of identicals for the relation E).$$\forall x_1,\dots ,x_n,y_1,\dots ,y_n \big (R(x_1,\dots ,x_n) \vee \lnot R(y_1,\dots ,y_n) \vee \bigvee _{i \le n} \lnot E(x_i,y_i) \big )$$
We claim that \({{\,\mathrm{Age}\,}}(\mathfrak {B}^*) = [\![\phi ^* ]\!]\). To see this, let \(\mathfrak {A}^*\) be a finite \(\sigma \)structure. If \(\mathfrak {A}^*\) satisfies \(\phi ^*\), then every induced substructure \(\mathfrak {A}\) of \(\mathfrak {A}^*\) with the property that \((x,y) \in E^{\mathfrak {A}}\) implies that at most one of x and y is an element of A, satisfies \(\phi \), and hence is a substructure of \(\mathfrak {B}\). This in turn means that \(\mathfrak {A}^*\) is in \({{\,\mathrm{Age}\,}}(\mathfrak {B}^*)\). The implications in this statement can be reversed which shows the claim.
Corollary 1
ASNP has a complexity dichotomy if and only if the infinitedomain dichotomy conjecture is true for firstorder reducts of binary finitely bounded homogeneous structures.
5 Deciding Amalgamation
In this section we show how to algorithmically decide whether a given existential secondorder sentence is in ASNP. The following is a known fact in the model theory of homogeneous structures (the first author has learned the fact from Gregory Cherlin), but we are not aware of any published proof in the literature.
Theorem 4
Let \({\mathcal F}\) be a finite set of finite binary relational \(\tau \)structures. There is an algorithm that decides whether \({{\,\mathrm{Forb}\,}}({\mathcal F})\) has the amalgamation property.
Proof
Let m be the maximal size of a structure in \(\mathcal F\), and let \(\ell \) be the number of isomorphism types of twoelement structures in \({\mathcal C} := {{\,\mathrm{Forb}\,}}({\mathcal F})\). It is wellknown and easy to prove that \({\mathcal C}\) has the amalgamation property if and only if it has the socalled 1point amalgamation property, i.e., the amalgamation property restricted to diagrams \((\mathfrak {B}_1,\mathfrak {B}_2)\) where \(B_1 = B_2 = B_1 \cap B_2 +1\). Suppose that \((\mathfrak {B}_1,\mathfrak {B}_2)\) is such an amalgamation diagram without amalgam. Let \(B_0 := B_1 \cap B_2\). Let \(B_1 \setminus B_0 = \{p\}\) and \(B_2 \setminus B_0 = \{q\}\). Let \(\mathfrak {D}\) be a \(\tau \)structure \(\mathfrak {D}\) with domain \(B_1 \cup B_2\) such that \(\mathfrak {B}_1\) and \(\mathfrak {B}_2\) are substructures of \(\mathfrak {D}\). Since \(\mathfrak {D}\) by assumption is not an amalgam for \((\mathfrak {B}_1,\mathfrak {B}_2)\), there must exist \(A = \{a_1,\dots ,a_{m2}\} \in B_0\) such that the substructure of \(\mathfrak {D}\) induced by \(\{a_1,\dots ,a_{m2},p,q\}\) embeds a structure from \(\mathcal F\).
Note that the number of such \(\tau \)structures \(\mathfrak {D}\) is bounded by \(\ell \) since they only differ by the substructure induced by p and q. So let \(A_1,\dots ,A_{\ell } \subseteq B_0\) be a list of sets witnessing that all of these structures \(\mathfrak {D}\) embed a structure from \(\mathcal F\). Let \(\mathfrak {C}_1\) be the substructure of \(\mathfrak {B}_1\) induced by \(\{p\} \cup A_1 \cup \cdots \cup A_{\ell }\) and \(\mathfrak {C}_2\) be the substructure of \(\mathfrak {B}_2\) induced by \(\{q\} \cup A_1 \cup \dots \cup A_{\ell }\). Suppose for contradiction that \((\mathfrak {C}_1,\mathfrak {C}_2)\) has an amalgam \(\mathfrak {C}\); we may assume that this amalgam is of size at most \((m2) \cdot \ell \). Depending on the twoelement structure induced by \(\{p,q\}\) in \(\mathfrak {C}\), there exists an \(i \le \ell \) such that the structure induced by \(\{p,q\} \cup A_i\) in \(\mathfrak {C}\) embeds a structure from \(\mathcal F\), a contradiction. \(\square \)
Corollary 2
There is an algorithm that decides for a given existential secondorder sentence \(\varPhi \) whether it is in ASNP.
Proof
Let k be the maximal number of variables per clause in the firstorder part \(\phi \) of \(\varPhi \), and let \(\mathcal F\) be the set of all structures at most the elements \(\{1,\dots ,k\}\) that do not satisfy \(\phi \). Then \({{\,\mathrm{Forb}\,}}({\mathcal F}) = [\![\phi ]\!]\) and the result follows from Theorem 2. \(\square \)
6 Guarded Monotone SNP
In this section we revisit an expressive generalisation of MMSNP introduced by Bienvenu, ten Cate, Lutz, and Wolter [3] in the context of ontologybased data access, called guarded monotone SNP (GMSNP). It is equally expressive as the logic MMSNP\(_2\) introduced by Madelaine [25]^{1}. We will see that every GMSNP sentence is equivalent to a finite disjunction of connected GMSNP sentences (Proposition 1), each of which lies in ASNP if the signature is binary (Theorem 5).
Definition 3
\(\alpha _1,\dots ,\alpha _n\) are atomic \((\tau \cup \rho )\)formulas, called body atoms,
\(\beta _1,\dots ,\beta _m\) are atomic \(\rho \)formulas, called head atoms,
for every head atom \(\beta _i\) there is a body atom \(\alpha _j\) such that \(\alpha _j\) contains all variables from \(\beta _i\) (such clauses are called guarded).
We do allow the case that \(m=0\), i.e., the case where the head consists of the empty disjunction, which is equivalent to \(\perp \) (false).
The next proposition extends a wellknown fact for MMSNP to guarded SNP.
Proposition 1
Every GMSNP sentence \(\varPhi \) is equivalent to a finite disjunction \(\varPhi _1 \vee \cdots \vee \varPhi _k\) of connected GMSNP sentences.
Proof
We prove Proposition 1. Let \(\varPhi \) be a guarded SNP sentence. Suppose that the quantifierfree part of \(\varPhi \) has a disconnected clause \(\psi \) (Definition 1). By definition the variable set can be partitioned into nonempty variable sets \(X_1\) and \(X_2\) such that for every negative literal \(\lnot R(x_1,\dots ,x_r)\) of the clause either \(\{x_1,\dots ,x_r\} \subseteq X_1\) or \(\{x_1,\dots ,x_r\} \subseteq X_2\). The same is true for every positive literal, since otherwise the definition of guarded clauses would imply a negative literal on a set that contains \(\{x_1,\dots ,x_r\}\), contradicting the property above. Hence, \(\psi \) can be written as \(\psi _1(\bar{x}) \vee \psi _2(\bar{y})\) for nonempty disjoint tuples of variables \(\bar{x}\) and \(\bar{y}\). Let \(\phi _1\) be the formula obtained from \(\phi \) by replacing \(\psi \) by \(\psi _1\), and let \(\phi _2\) be the formula obtained from \(\phi \) by replacing \(\psi \) by \(\psi _2\).
Let \(P_1,\dots ,P_k\) be the existential predicates in \(\varPhi \), and let \(\tau \) be the input signature of \(\varPhi \). It suffices to show that for every \((\tau \cup \{P_1,\dots ,P_k\})\)expansion \(\mathfrak {A}'\) of \(\mathfrak {A}\) we have that \(\mathfrak {A}'\) satisfies \(\phi \) if and only if \(\mathfrak {A}'\) satisfies \(\phi _1\) or \(\phi _2\). If \(\mathfrak {A}'\) falsifies a clause of \(\phi \), there is nothing to show since then \(\mathfrak {A}'\) satisfies neither \(\phi _1\) nor \(\phi _2\). If \(\mathfrak {A}'\) satisfies all clauses of \(\phi \), it in particular satisfies a literal from \(\psi \); depending on whether this literal lies in \(\psi _1\) or in \(\psi _2\), we obtain that \(\mathfrak {A}'\) satisfies \(\psi _1\) or \(\psi _2\), and hence \(\phi _1\) or \(\phi _2\). Iterating this process for each disconnected clause of \(\phi \), we eventually arrive at a finite disjunction of connected guarded SNP sentences. \(\square \)
It is wellknown and easy to see [17] that each of \(\varPhi _1,\dots ,\varPhi _k\) can be reduced to \(\varPhi \) in polynomial time. Conversely, if each of \(\varPhi _1,\dots ,\varPhi _k\) is in P, then \(\varPhi \) is in P, too. It follows in particular that if connected GMSNP has a complexity dichotomy into P and NPcomplete, then so has GMSNP.
Theorem 5
For every sentence \(\varPhi \) in connected GMSNP there exists a reduct \(\mathfrak {C}\) of a finitely bounded homogeneous structures such that \([\![\varPhi ]\!]= {{\,\mathrm{CSP}\,}}(\mathfrak {C})\). If all existentially quantified relation symbols in \(\varPhi \) are binary then it is equivalent to an ASNP sentence.
In the proof of Theorem 5 we use a result of Cherlin, Shelah, and Shi [12] in a strengthened form due to Hubička and Nešetřil [22], namely that for every finite set \(\mathcal F\) of finite \(\sigma \)structures, for some finite relational signature \(\sigma \), there exists a finitely bounded homogeneous \((\sigma \cup \rho )\)structure \(\mathfrak {B}\) such that a finite \(\sigma \)structure \(\mathfrak {A}\) homomorphically maps to \(\mathfrak {B}\) if none of the structures in \(\mathcal F\) homomorphically maps to \(\mathfrak {B}\). We now prove Theorem 5.
Proof
\(R'\) denotes \(R^{\mathfrak {A}'}\) for each \(R \in \tau \);
\(R^+\) denotes \(R^{\mathfrak {A}'}\) for each \(R \in \{E_1,\dots ,E_k\}\);
\(R^{}\) denotes \(\lnot R^{\mathfrak {A}'}\) for each \(R \in \{E_1,\dots ,E_k\}\).
Then \(\mathfrak {A}''\) satisfies \(\phi '\), and hence embeds into \(\mathfrak {B}\). This embedding is a homomorphism from \(\mathfrak {A}\) to \(\mathfrak {C}\) since the image of the embedding is correctly labelled by the construction of \(\mathfrak {A}''\).
Conversely, suppose that \(\mathfrak {A}\) has a homomorphism h to \(\mathfrak {C}\). Let \(\mathfrak {A}'\) be the \(\tau \cup \{E_1,\dots ,E_k\}\)expansion of \(\mathfrak {A}\) by defining \((a_1,\dots ,a_n) \in R^\mathfrak {A}\) if and only if \((h(a_1),\dots ,h(a_n)) \in R^{\mathfrak {B}'}\), for every nary \(R \in \{E_1,\dots ,E_k\}\). Then each clause of \(\phi \) is satisfied, because each clause of \(\phi \) is guarded: let \(x_1,\dots ,x_m\) be the variables of some clause of \(\phi \). If \(a_1,\dots ,a_m \in A\) satisfy the body of this clause, and \(\psi (a_{i_1},\dots ,a_{i_l})\) is a head atom of such a clause, then the set \(\{h(a_{i_1}),\dots , h(a_{i_l})\}\) is correctly labelled. This implies that some of the head atoms of the clause must be true in \(\mathfrak {A}'\) because \(\mathfrak {B}'\) satisfies \(\phi '\). The second statement follows from Theorem 3. \(\square \)
The following example shows that GMSNP does not contain ASNP.
Example 6
\({{\,\mathrm{CSP}\,}}({\mathbb Q};<)\) is in ASNP (see Example 5) but not in GMSNP. Indeed, suppose that \(\varPhi \) is a GMSNP sentence which is true on all finite directed paths. We assume that the quantifierfree part \(\phi \) of \(\varPhi \) is in conjunctive normal form. Let \(\rho \) be the existentially quantified relation symbols of \(\varPhi \), let \(k := \rho \), and let l be the number of variables in \(\varPhi \). Every directed path, viewed as a \(\{<\}\)structure, satisfies \(\varPhi \), and therefore has an \(\{<\} \cup \rho \)expansion \(\mathfrak {A}\) that satisfies \(\phi \). Note that there are finitely many different \(\{<\} \cup \rho \)expansions of a path of length \(l \in {\mathbb N}\); let \(p \in {\mathbb N}\) be this number. Hence, for a path of length \(L := (p+1) l\), there must be \(i,j \in \{0,\dots , p\}\) with \(i<j\) such that the substructures of \(\mathfrak {A}\) induced by \(i l +1,i l+2,\dots ,i l +l\) and by \(j l + 1,j l+2,\dots ,j l+l\) are isomorphic. We then claim that the directed cycle \((i+1) l + 1,(i+1) l + 2,\dots , j l + 1,\dots , jl + l, (i+1) l + 1\) satisfies \(\varPhi \): this is witnessed by the \(\{<\} \cup \rho \)expansion inherited from \(\mathfrak {A}\) which satisfies \(\phi \) since each clause in \(\phi \) is guarded. Hence, \(\varPhi \) does not express digraph acyclicity.
7 Application: Instances of Bounded Treewidth
If a computational problem can be formulated in ASNP or in GMSNP, then this has remarkable consequences besides a potential complexity dichotomy. In this section we show that every problem that can be formulated in ASNP or in GMSNP is in P when restricted to instances of bounded treewidth. The corresponding result for Monadic SecondOrder Logic (MSO) instead of ASNP is a famous theorem of Courcelle [13]. We strongly believe that ASNP is not contained in MSO (consider for instance the Betweenness Problem from Example 3), so our result appears to be incomparable to Courcelle’s.
In the proof of our result, we need the following concepts from model theory. A firstorder theory T is called \(\omega \)categorical if all countable models of T are isomorphic [21]. A structure \(\mathfrak {B}\) is called \(\omega \)categorical if its firstorder theory (i.e., the set of firstorder sentences that hold in \(\mathfrak {B}\)) is \(\omega \)categorical. Note that with this definition, finite structures are \(\omega \)categorical. Another classic example is the structure \(({\mathbb Q};<)\). The definition of treewidth can be treated as a black box in our proof, and we refer the reader to [6].
Theorem 6
Let \(\varPhi \) be an ASNP or a connected GMSNP \(\tau \)sentence and let \(k \in \mathbb N\). Then the problem to decide whether a given finite \(\tau \)structure \(\mathfrak {A}\) of treewidth at most k satisfies \(\varPhi \) can be decided in polynomial time with a Datalog program (of width k).
Proof
Since structures that are homogeneous in a finite relational language are \(\omega \)categorical [21] and firstorder reducts of \(\omega \)categorical structures are \(\omega \)categorical [21], Theorem 2 and Theorem 5 imply that the problem to decide whether a finite \(\tau \)structure satisfies \(\phi \) can be formulated as CSP\((\mathfrak {B})\) for an \(\omega \)categorical structure \(\mathfrak {B}\). Then the statement follows from Corollary 1 in [6]. \(\square \)
Remark 1
In Theorem 6 it actually suffices to assume that the core of \(\mathfrak {A}\) has treewidth at most k.
Corollary 3
Let \(\varPhi \) be a GMSNP \(\tau \)sentence and let \(k \in {\mathbb N}\). Then there is a polynomialtime algorithm that decides whether a given \(\tau \)structure of treewidth at most k satisfies \(\varPhi \).
8 Conclusion and Open Problems
We presented an application of ASNP concerning the evaluation of computational problems on classes of structures of bounded treewidth. We also proved that the syntax of ASNP is algorithmically decidable. The following problems concerning ASNP are open.
 1.
Is the Amalgamation Property decidable for (not necessarily binary) classes given by finitely many forbidden substructures?
 2.
Is every binary CSP in Monadic SecondOrder Logic (MSO) also in ASNP?
 3.
Is every problem in NP polynomialtime equivalent to a problem in Amalgamation SNP if we drop the monotonicity assumption?
 4.
Is there a natural logic (which in particular has an effective syntax) that contains both ASNP and connected GMSNP and which describes CSPs for reducts of finitely bounded homogeneous structures?
Footnotes
References
 1.Barto, L., Kompatscher, M., Olšák, M., Pham, T.V., Pinsker, M.: Equations in oligomorphic clones and the constraint satisfaction problem for \(\omega \)categorical structures. J. Math. Logic, 19(2), #1950010 (2019). An extended abstract appeared at the Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science  LICS’17Google Scholar
 2.Barto, L., Pinsker, M.: The algebraic dichotomy conjecture for infinite domain constraint satisfaction problems. In: Proceedings of the 31th Annual IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 615–622 (2016). Preprint arXiv:1602.04353
 3.Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontologybased data access: a study through disjunctive datalog, CSP, and MMSNP. ACM Trans. Database Syst. 39(4), 33 (2014)MathSciNetCrossRefGoogle Scholar
 4.Bodirsky, M.: Constraint satisfaction with infinite domains. Dissertation, HumboldtUniversität zu Berlin (2004)Google Scholar
 5.Bodirsky, M.: Complexity classification in infinitedomain constraint satisfaction. Mémoire d’habilitation à diriger des recherches, Université Diderot  Paris 7. arXiv:1201.0856 (2012)
 6.Bodirsky, M., Dalmau, V.: Datalog and constraint satisfaction with infinite templates. J. Comput. Syst. Sci. 79, 79–100 (2013). A preliminary version appeared in the proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS’05)MathSciNetCrossRefGoogle Scholar
 7.Bodirsky, M., Madelaine, F., Mottet, A.: A universalalgebraic proof of the complexity dichotomy for Monotone Monadic SNP. In: Proceedings of the Symposium on Logic in Computer Science (LICS), pp. 105–114 (2018). Preprint available under arXiv:1802.03255
 8.Bodirsky, M., Pinsker, M., Pongrácz, A.: Projective clone homomorphisms. J. Symb. Logic (2014). Preprint arXiv:1409.4601
 9.Bodirsky, M., Rydval, J.: Temporal constraint satisfaction problems in fixed point logic (2019). PreprintGoogle Scholar
 10.Braunfeld, S.: Towards the undecidability of atomicity for permutation classes via the undecidability of joint embedding for hereditary graph classes (2019). Preprint available at arXiv:1903.11932
 11.Bulatov, A.A.: A dichotomy theorem for nonuniform CSPs. In: 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, 15–17 October 2017, pp. 319–330 (2017)Google Scholar
 12.Cherlin, G., Shelah, S., Shi, N.: Universal graphs with forbidden subgraphs and algebraic closure. Adv. Appl. Math. 22, 454–491 (1999)MathSciNetCrossRefGoogle Scholar
 13.Courcelle, B., Engelfriet, J.: Graph Structure and Monadic SecondOrder Logic: A LanguageTheoretic Approach. Cambridge University Press, New York (2012)CrossRefGoogle Scholar
 14.Fagin, R.: Generalized firstorder spectra and polynomialtime recognizable sets. Complex. Comput. 7, 43–73 (1974)MathSciNetzbMATHGoogle Scholar
 15.Feder, T., Vardi, M.Y.: The computational structure of monotone monadic SNP and constraint satisfaction: a study through Datalog and group theory. SIAM J. Comput. 28, 57–104 (1999)MathSciNetCrossRefGoogle Scholar
 16.Feder, T., Vardi, M.Y.: Homomorphism closed vs. existential positive. In: Proceedings of the Symposium on Logic in Computer Science (LICS), pp. 311–320 (2003)Google Scholar
 17.Foniok, J., Nešetřil, J.: Generalised dualities and maximal finite antichains in the homomorphism order of relational structures. Eur. J. Combin. 29(4), 881–899 (2008)MathSciNetCrossRefGoogle Scholar
 18.Garey, M., Johnson, D.: A Guide to NPCompleteness. CSLI Press, Stanford (1978)Google Scholar
 19.Grohe, M.: The quest for a logic capturing PTIME. In: Proceedings of ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 267–271 (2008)Google Scholar
 20.Gurevich, Y.: Toward logic tailored for computational complexity. In: Börger, E., Oberschelp, W., Richter, M.M., Schinzel, B., Thomas, W. (eds.) Computation and Proof Theory. LNM, vol. 1104, pp. 175–216. Springer, Heidelberg (1984). https://doi.org/10.1007/BFb0099486CrossRefGoogle Scholar
 21.Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)CrossRefGoogle Scholar
 22.Hubička, J., Nešetřil, J.: Homomorphism and embedding universal structures for restricted classes. MultipleValued Logic Soft Comput. 27(2–3), 229–253 (2016). arXiv:0909.4939MathSciNetzbMATHGoogle Scholar
 23.Kun, G.: Constraints, MMSNP, and expander relational structures. Combinatorica 33(3), 335–347 (2013). https://doi.org/10.1007/s0049301324054MathSciNetCrossRefzbMATHGoogle Scholar
 24.Ladner, R.E.: On the structure of polynomial time reducibility. J. ACM 22(1), 155–171 (1975)MathSciNetCrossRefGoogle Scholar
 25.Madelaine, F.: Universal structures and the logic of forbidden patterns. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 471–485. Springer, Heidelberg (2006). https://doi.org/10.1007/11874683_31CrossRefzbMATHGoogle Scholar
 26.Zhuk, D.: A proof of CSP dichotomy conjecture. In: 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, 15–17 October 2017, pp. 331–342 (2017). https://arxiv.org/abs/1704.01914