Symmetric Linear Arc Monadic Datalog and Gadget Reductions

In monadic Datalog, we restrict the arity of the inferred predicates of the Datalog program to one (i.e., all the IDBs are monadic). In arc Datalog we restrict each rule to a single input relation symbol (i.e., the body contains a single EDB; for formal definitions, see Section 2.4).

An important Datalog fragment is arc monadic Datalog, which is still powerful enough to express the famous arc consistency procedure in constraint satisfaction. The arc consistency procedure has already been studied by Feder and Vardi [25], and has many favorable properties: it can be evaluated in linear time and linear space. It is used as an important pre-processing step in the algorithms for both of the mentioned CSP dichotomy proofs, and it is also used in many practical implementations of algorithms in constraint satisfaction. The arc consistency procedure is still extremely powerful, and can for instance solve the P-complete HornSat Problem.

Feder and Vardi characterised the power of the arc consistency procedure in terms of tree duality (see Section 2.6), a natural combinatorial property which has been studied intensively in the graph homomorphism literature in the 90s (see, e.g., [26, 27]). Their characterisation has several remarkable consequences: one is that also the class of CSPs that can be solved by an arc monadic Datalog program is closed under gadget reductions. Another one is a collapse result for Datalog when it comes to finite-domain CSPs, namely that monadic Datalog collapses to arc monadic Datalog: in fact, if a finite-domain CSP can be solved by a monadic Datalog program, then it can already be solved by the arc consistency procedure (i.e., by a program in arc monadic Datalog). This statement is false without the restriction to finite-domain CSPs; in fact, there are infinite-domain CSPs that can be solved by a monadic Datalog program, but not by a program in arc monadic Datalog (Bodirsky and Dalmau [8]).

Besides arc monadic Datalog, there are other natural fragments of Datalog. The most notable one is linear Datalog [29]. Linear Datalog programs can be evaluated in non-deterministic logarithmic space (NL), and hence cannot express P-hard problems (unless P=NL). Dalmau [19] asked whether the converse is true as well, i.e., whether every finite-domain CSP which is in NL can be solved by a linear Datalog program [19]. This is widely treated as a conjecture, to which we refer as the linear Datalog conjecture; it is one of the biggest open problems in finite-domain constraint satisfaction.

There are some sufficient conditions for solvability by linear Datalog (see Bulatov, Kozik, and Willard [3] and Carvalho, Dalmau, and Krokhin [15]) and some necessary conditions (Larose and Tesson [32]) but the results still leave a large gap. For examples of CSPs of orientations of trees that fall into this gap, see Bodirsky, Bulín, Starke, and Wernthaler [7]. Again, linear Datalog is closed under gadget reductions [38]. And indeed, if HornSat has a gadget-reduction in a finite-domain CSP, then the finite-domain CSP cannot be solved by a linear Datalog program [1].

A further restriction is symmetric linear Datalog, introduced by Egri, Larose, and Tesson [23]. Symmetric linear Datalog programs can be evaluated in deterministic logspace (L). Egri, Larose, and Tesson conjecture that every finite-domain CSP which is in L can be be solved by a symmetric linear Datalog program [23]; we refer to this conjecture as the symmetric linear Datalog conjecture.

Symmetric linear Datalog is closed under gadget reductions [38]. Since directed reachability is not in symmetric linear Datalog [24], it follows that every CSP that admits a gadget reduction from directed reachability cannot be solved by a symmetric linear Datalog program. Egri, Larose, and Tesson also suggest that this might be the only additional condition for containment in symmetric linear Datalog, besides the known necessary conditions to be in linear Datalog. Kazda [30] confirms the symmetric linear Datalog conjecture conditionally on the truth of the linear Datalog conjecture, i.e., he shows that if a finite-domain CSP is in linear Datalog and does not admit a gadget reduction from a CSP that corresponds to the directed reachability problem, then it is in symmetric linear Datalog (generalizing an earlier result of Dalmau and Larose [20]).

In this paper, we study the Datalog fragment that can be obtained by combining all the previously considered restrictions, namely symmetric linear arc monadic (slam) Datalog. Before stating our result we illustrate this fragment with some examples. For $n\ge 1$, let ${𝔓}_n$ be the directed path with $n$ vertices and $n-1$ edges. An example of a slam Datalog program which solves CSP$({𝔓}_2)$ is

(in this case, the program is even recursion-free). An example of a slam Datalog program which solves CSP$({𝔓}_3)$, this time with recursion and IDBs $A$ and $B$, is

The idea why this program is correct is that a finite digraph $𝔄$ has a homomorphism to ${𝔓}_3$ if and only if certain orientations of paths (those of net length three; for a formal description, see Example 8) do not have a homomorphism to $𝔄$; and the program derives the goal predicate on $𝔄$ precisely if there is a homomorphism from such a path to $𝔄$.

It follows from our results that the class of CSPs that can be solved by slam Datalog programs is closed under gadget reductions, despite the many restrictions that we imposed.

We provide a full description of the power of a Datalog fragment in terms of gadget reductions: we show that a CSP can be solved by a slam Datalog program if and only if it has a gadget reduction to CSP$({𝔓}_2)$.¹¹1The statement even holds for infinite-domain CSPs, since being solved by an arc monadic Datalog program implies the existence of a finite template [8] and admitting a gadget reduction to a finite-domain CSP implies the existence of a finite template as well [21]. The particular role of the structure ${𝔓}_2$ is explained by the fact that it is a representative of the unique class of CSPs which is non-trivial and weakest with respect to gadget reductions – a formalisation of this can be found in Section 2.3.²²2We mention that ${𝔓}_2$ is a Boolean structure which simultaneously satisfies the Schaefer conditions of being Horn, dual Horn, affine, and bijunctive [37]. This shows that slam Datalog is the smallest non-trivial fragment of Datalog that is closed under gadget reductions.

Our main result (Theorem 18) establishes a tight connection between the power of slam Datalog and various central themes in structural combinatorics and universal algebra. Specifically, the power of slam Datalog can be characterised by a combinatorial duality which we call unfolded caterpillar duality (restricting the concept of caterpillar duality of Carvalho, Dalmau, and Krokhin [16], and using ideas that appear implicitly in the literature on symmetric Datalog [20, 23, 30]), and by the existence of a quasi Maltsev polymorphism (a central concept in universal algebra) in combination with $kn$-ary $k$-absorbing polymorphisms for every $k,n\ge 1$ (introduced in  [16] as well). Our result also implies that the following meta-problem can be decided algorithmically: given a finite structure $𝔅$, can $\mathrm{CSP}(𝔅)$ be solved by a slam Datalog program?

Solvability of finite-domain CSPs by (unrestricted) Datalog was first studied by Feder and Vardi; they proved that $\mathrm{CSP}(𝔅)$ can be solved by Datalog if and only if $𝔅$ has bounded treewidth duality, and they showed that CSPs for systems of linear equations over finite Abelian groups cannot be solved by Datalog. Larose and Zadori [33] showed that solvability by Datalog is preserved by gadget reductions and they asked whether having a gadget reduction from CSPs for systems of linear equations is not only a sufficient, but also a necessary condition for not being solvable by Datalog. This questions was answered positive by Barto and Kozik [4]. Kozik, Krokhin, and Willard [31] gave a characterisation of Datalog in terms of minor conditions.

Linear (but not necessarily symmetric) monadic arc Datalog has been studied by Carvalho, Dalmau, and Krokhin [16]; our proof builds on their result. In their survey on Datalog fragments and dualities in constraint satisfaction [13] Bulatov, Krokhin, and Larose write “it would be interesting to find (…) an appropriate notion of duality for symmetric (Linear) Datalog (…)”. We do find such a notion for symmetric linear arc monadic Datalog, namely unfolded caterpillar duality (Theorem 18).

Another fragment of Datalog consists of the set of conjunctive queries; the CSPs that can be solved by such Datalog programs are precisely the CSPs that are first-order expressible, by Rossman’s theorem [36]. This is also known to be equivalent to CSPs having finite duality. However, note that first-order definability is not preserved under gadget reductions (as we will see in Section 2.6).

We assume familiarity with the concepts of relational structures and first-order formulas from mathematical logic, as introduced for instance in [28]. The arity of a relation symbol $R$ is denoted by $\mathrm{ar}(R)$. If $𝔄$ is a $\tau$-structure, then we sometimes use the same symbol for $R\in \tau$ and the respective relation $R^{𝔄}$ of $𝔄$. We write $𝔄[S]$ for the substructure of $𝔄$ induced on $S$.

A (directed) graph is a relational structure with a single binary relation $E$. For instance the clique with $n$ vertices is the graph ${𝔎}_n$ with domain $[n]$ and edges $E^{{𝔎}_n}:=\{(a,b)\mid a\ne b\}$. Let $𝔊$ be a graph. An (undirected) path from $a$ to $b$ in $𝔊$ is a tuple $P=(a_1,\mathrm{\dots },a_n)$ such that $a_1,\mathrm{\dots },a_n$ are pairwise distinct, $a_1=a$, $a_n=b$, and for all $i\in [n-1]$ there is an edge between $a_i$ and $a_{i+1}$ (from $a_i$ to $a_{i+1}$ or from $a_{i+1}$ to $a_i$). If $i\in [2,n-1]$, then we say that $P$ passes through $a_i$. A graph $𝔊$ is called connected if for any two elements $a,b$ there exists a path from $a$ to $b$ in $𝔊$. A cycle is a path from $a$ to $b$ of length $n$ at least three such that there is an edge between $a$ and $b$. A graph is called acyclic if it does not contain any cycle. A graph is called a tree if it is connected and acyclic. A graph has girth $k$ if the length of the shortest cycle is $k$.

Let $\tau$ be a relational signature and let $𝔄$ and $𝔅$ be $\tau$-structures. Then a homomorphism from $𝔄$ to $𝔅$ is a map $h:A\to B$ such that for $R\in \tau$, say of arity $k$, we have $(h(a_1),\mathrm{\dots },h(a_k))\in R^{𝔅}$ whenever $(a_1,\mathrm{\dots },a_k)\in R^{𝔄}$. An embedding of $𝔄$ into $𝔅$ is an injective map $e:A\to B$ such that $(e(a_1),\mathrm{\dots },e(a_k))\in R^{𝔅}$ if and only if $(a_1,\mathrm{\dots },a_k)\in R^{𝔄}$. We write $𝔄\to 𝔅$ if there exists a homomorphism from $𝔄$ to $𝔅$ and $𝔄\to ̸𝔅$ if there exists no homomorphism from $𝔄$ to $𝔅$.

If $\tau$ is a finite relational signature and $𝔅$ is a $\tau$-structure, then $\mathrm{CSP}(𝔅)$ denotes the class of all finite $\tau$-structures $𝔄$ such that $𝔄\to 𝔅$. It can be viewed as a computational problem. For example, $\mathrm{CSP}({𝔎}_n)$ consists of the set of all finite $n$-colourable graphs, and can therefore be viewed as the $n$-colorability problem. Clearly, for finite structures $𝔅$, this problem is always in NP. Note that from the database perspective, by the work of Chandra and Merlin [17], $\mathrm{CSP}(𝔅)$ can be viewed as the expression complexity of conjunctive queries over $𝔅$.

A $\tau$-structure $𝔅$ is homomorphically equivalent to a $\tau$-structure $ℭ$ if there are homomorphisms from $𝔅$ to $ℭ$ and vice versa. Clearly, homomorphically equivalent structures have the same CSP. A relational $\tau$-structure $ℭ$ is called a core if all endomorphisms of $ℭ$ are embeddings. It is well-known and easy to see that every finite structure $𝔅$ is homomorphically equivalent to a core $ℭ$, and that all core structures $ℭ$ that are homomorphically equivalent to $𝔅$ are isomorphic; therefore, we refer to $ℭ$ as the core of $𝔅$.

A $\tau$-formula $\varphi$ is called a conjunctive query (in constraint satisfaction and model theory such formulas are called primitive positive, or short pp) if it is built from atomic formulas (including atomic formulas of the form $x=y$) using only conjunction and existential quantification. If $𝔅$ is a $\tau$-structure, and $\varphi$ is a conjunctive query over the signature $\tau$, then the relation $R=\{(t_1,\mathrm{\dots },t_k)\mid 𝔅\vDash \varphi (t_1,\mathrm{\dots },t_k)\}$ is called the relation defined by $\varphi$.

Observe that the canonical database of the canonical conjunctive query of a structure $𝔅$ equals $𝔅$. The following concepts have been introduced by Barto, Opršal, and Pinsker [5].

Primitive positive constructions turned out to the the essential tool for classifying the complexity of finite-domain CSPs, because if $ℭ$ has a pp-construction from $𝔅$, then there is a so-called gadget reduction from $\mathrm{CSP}(ℭ)$ to $\mathrm{CSP}(𝔅)$; in fact, the converse is true as well, see Dalmau and Opršal [21].

For instance, the solution to the Feder-Vardi conjecture mentioned in the introduction states that $\mathrm{CSP}(𝔅)$, for a finite structure $𝔅$, is NP-hard if and only if ${𝔎}_3$ has a pp-construction from $𝔅$ (unless $\mathrm{P}=\mathrm{NP}$); by what we have stated above, this is true if and only if the 3-coloring problem has a gadget reduction to $\mathrm{CSP}(𝔅)$.

Given the fundamental importance of conjunctive queries and homomorphisms in database theory, we believe that pp-constructions and gadget reductions are an interesting concept for database theory as well.

Let $\tau$ and $\rho$ be finite relational signatures such that $\tau \subseteq \rho$. A Datalog program is a finite set of rules of the form ${\varphi }_0:-{\varphi }_1,\mathrm{\dots },{\varphi }_n$ where each ${\varphi }_i$ is an atomic $\tau$-formula. The formula ${\varphi }_0$ is called the head of the rule, and the sequence ${\varphi }_1,\mathrm{\dots },{\varphi }_n$ is called the body of the rule. The symbols in $\tau$ are called EDBs (extensional database predicates) and the other symbols from $\rho$ are called IDBs (intensional database predicates). In the rule heads, only IDBs are allowed. There is one special IDB of arity 0, which is called the goal predicate. IDBs might also appear in the rule bodies. We view the set of rules as a recursive specification of the IDBs in terms of the EDBs – for a detailed introduction, see, e.g., [8]. A Datalog program is called

• $\mathrm{■}$

  linear if in each rule, at most one IDB appears in the body (we then assume without loss of generality that in every rule whose body contains an IDB, the IDB is listed first).

• $\mathrm{■}$

  arc if each rule involves at most one EDB.

• $\mathrm{■}$

  symmetric if it is linear and for every rule ${\varphi }_0:-{\varphi }_1,{\varphi }_2,\mathrm{\dots },{\varphi }_n$ where ${\varphi }_0$ and ${\varphi }_1$ are build from IDBs, the Datalog program also contains the reversed rule ${\varphi }_1:-{\varphi }_0,{\varphi }_2,\mathrm{\dots },{\varphi }_n$.³³3Note that we do not have to exclude that ${\varphi }_0$ is the goal predicate, because we may always add its symmetric version without changing the set of structures on which the goal predicate is derived.

If $𝔅$ is a $\tau$-structure, then we say that $\mathrm{CSP}(𝔅)$ is solved by a Datalog program $\mathrm{\Pi }$ with EDBs $\tau$ if the following holds: the goal predicate is derived by $\mathrm{\Pi }$ on a finite $\tau$-structure $𝔄$ if and only if there is no homomorphism from $𝔄$ to $𝔅$. We say that a Datalog program has width $(\mathrm{\ell },k)$ if all IDBs have arity at most $\mathrm{\ell }$, and if every rule has at most $k$ variables. For given $(\mathrm{\ell },k)$ and a structure $𝔅$, there exists a Datalog program $\mathrm{\Pi }$ of width $(\mathrm{\ell },k)$ with the remarkable property that if some Datalog program of width $(\mathrm{\ell },k))$ solves $\mathrm{CSP}(𝔅)$, then $\mathrm{\Pi }$ solves $\mathrm{CSP}(𝔅)$. This Datalog program is referred to as the canonical Datalog program for $𝔅$ of width $(\mathrm{\ell },k)$, and is constructed as follows [25]: For every relation $R$ over $B$ of arity at most $\mathrm{\ell }$, we introduce a new IDB. The empty relation of arity 0 is the goal predicate. Then $\mathrm{\Pi }$ contains all rules $\varphi :-{\varphi }_1,\mathrm{\dots },{\varphi }_n$ with at most $k$ variables such that the formula $\forall \overline{x}({\varphi }_1\wedge \mathrm{\cdots }\wedge {\varphi }_n\Rightarrow \varphi )$ holds in the expansion of $𝔅$ by all IDBs. If the canonical Datalog program for $𝔅$ derives the goal predicate on a finite structure $𝔄$, then there is no homomorphism from $𝔄$ to $𝔅$ (see, e.g., [8]).

If $k$ is the maximal arity of the EDBs, we may restrict the canonical Datalog program of width $(1,k)$ to those rules with only unary IDBs and at most one EDB; in this case, we obtain the canonical arc monadic Datalog program, which is also known as the arc consistency procedure. Analogously, we may define the canonical linear, and the canonical symmetric Datalog program. We may also combine these restrictions, and in particular obtain a definition the canonical slam Datalog program, i.e., the canonical symmetric linear arc monadic Datalog program, which has not yet been studied in the literature before. The following lemma can be shown analogously to the well-known fact for unrestricted canonical Datalog programs of width $(\mathrm{\ell },k)$ (see, e.g., [8]).

Several results from graph theory concerning acyclicity and high girth can be generalised to general structures. To formulate these generalisations, we need the following notion. The incidence graph of a structure $𝔄$ with the relational signature $\tau$ is the bipartite graph where one color class is $A$, and the other consists of all pairs of the form $(t,R)$ such that $t\in R^{𝔄}$ and $R\in \tau$. We put an edge between $a$ and $(t,R)$ if $t_i=a$ for some $i$. The girth of an (undirected) graph $𝔊$ is the length of the shortest cycle in $𝔊$. We say that a relational structure is a generalised tree if its incidence graph is a tree. A leaf of a generalised tree $𝔗$ is an element of $T$ which has degree one in the incidence graph of $𝔗$. A structure $𝔅$ is called injective if all tuples that are in some relation in $𝔅$ are injective (i.e., have no repeated entries). A structure is called an (injective) tree if it is injective and its incidence graph is a tree.

For a $\tau$-structure $𝔅$ and a class of $\tau$-structures $ℱ$ the pair $(ℱ,𝔅)$ is called a duality pair if a finite structure $𝔄$ has a homomorphism to $𝔅$ if and only if no structure $𝔉\in ℱ$ has a homomorphism to $𝔄$. Several forms of duality pairs will be relevant here, depending on the class of structures $ℱ$. A $\tau$-structure $𝔅$ has finite duality if there exists a finite set of $\tau$-structures $ℱ$ such that $(ℱ,𝔅)$ is a duality pair. The property of having finite duality is among the very few notions studied in the context of constraint satisfaction which is not preserved under gadget reductions, as illustrated in the following example.

A more robust form of duality is tree duality, which plays a central role in constraint satisfaction, and is studied in the graph homomorphism literature in the 90s. A structure $𝔅$ has tree duality if there exists a (not necessarily finite) set of trees $ℱ$ such that $(ℱ,𝔅)$ is a duality pair. The following is well known; see Theorem 7.4 in [14]. The equivalence of 1. and 3. is from [25]; also see [6].

There are finite structures with tree duality that have a P-complete CSP, such as the structure $(\{0,1\};\{0\},\{1\},{\{0,1\}}^3\setminus \{(1,1,0)\})$, which is essentially the Boolean HornSAT problem. In the following, we therefore introduce more restrictive forms of dualities.

See Figure 1 (left) for an example. A relational structure $𝔄$ is called an (injective) caterpillar if it is injective and a generalised caterpillar (this definition of a caterpillar is equivalent to the one given in [16]). A structure $𝔅$ has caterpillar duality if there exists a set of caterpillars $ℱ$ such that $(ℱ,𝔅)$ is a duality pair. The structures $𝔅$ with caterpillar duality have been characterised by [16] (Theorem 17) in terms of linear arc Datalog.

To capture the power of symmetric linear arc Datalog, we present a more restrictive form of duality. Let $𝔗$ be an (injective) tree and let $a$ and $b$ be distinct elements of $𝔗$. Write the canonical query of $𝔗$ as ${\varphi }_a\wedge {\varphi }_{a,b}\wedge {\varphi }_b$ where ${\varphi }_a$ contains all conjuncts of the form $R(\overline{u})$ such that in the incidence graph, all paths from the vertex $(\overline{u},R)$ to the vertex $b$ pass though $a$. Similarly, we define ${\varphi }_b$, switching the roles of $a$ and $b$. Note that ${\varphi }_a$ and ${\varphi }_b$ do not share any conjuncts. All the remaining conjuncts of the canonical query form $\psi$. Let ${\varphi }_1$ be obtained from ${\varphi }_a$ (${\varphi }_b$) by existentially quantifying all variables except for $a$ ($b)$, and let $\psi$ be obtained from ${\varphi }_{a,b}$ by existentially quantifying all variables except for $a$ and $b$. We introduce the following concept; see Figure 2 for an example.

Note that an unfolding of a tree $𝔗$ is again a tree and has a homomorphism to $𝔗$. It can also be shown that the unfolding of a caterpillar is a caterpillar as well (Lemma 24). We say that a structure $𝔅$ has unfolded caterpillar duality if there exists a set $ℱ$ of caterpillars such that $(ℱ,𝔅)$ is a duality pair, and $ℱ$ contains every unfolding of a caterpillar in $ℱ$. Clearly, unfolded caterpillar duality implies caterpillar duality. Unfolded generalised caterpillar duality is defined analogously.

If $𝔅$ is a structure and $k\ge 1$, then a polymorphism of $𝔅$ of arity $k$ is a homomorphism from ${𝔅}^k$ to $𝔅$. The set of all polymorphisms of $𝔅$ is denoted by $\mathrm{Pol}(𝔅)$. An (operation) clone is a set of operations which contains the projections and is closed under composition. Note that $\mathrm{Pol}(𝔅)$ is a clone. An operation $f:B^n\to B$ is called idempotent if $f(x,\mathrm{\dots },x)=x$ for all $x\in B$. A clone is called idempotent if all of its operations are idempotent.

If $𝔄$ and $𝔅$ are a structures and $k\ge 1$, then a polymorphism of $(𝔄,𝔅)$ of arity $k$ is a homomorphism from ${𝔄}^k$ to $𝔅$. The set of all polymorphisms of $(𝔄,𝔅)$ is denoted by $\mathrm{Pol}(𝔄,𝔅)$. Let $f:A^n\to B$ be a function and let $\sigma :[n]\to [m]$, then the map

is called a minor of $f$. A minion is a set or functions from $A^n$ to $B$ that is closed under taking minors. Note that $\mathrm{Pol}(𝔄,𝔅)$ is a minion. Let $ℳ$ and $𝒩$ be minions. A map $\xi :ℳ\to 𝒩$ is called a minion homomorphism if $\xi$ preserves arity and for every $f\in ℳ$ of arity $n$ and every map $\sigma :[n]\to [m]$ we have $\xi (f_{\sigma })={(\xi (f))}_{\sigma }$.

Let $\tau$ be a function signature, i.e., a set of function symbols, each equipped with an arity. A minor condition is a finite set $\mathrm{\Sigma }$ of minor identities, i.e., expressions of the form

where $f$ is an $n$-ary function symbol from $\tau$, $g$ is an $m$-ary function symbol from $\tau$, and $x_1,\mathrm{\dots },x_n,y_1,\mathrm{\dots },y_m$ are (not necessarily distinct) variables. If $ℳ$ is a minion, then a map $\xi :\tau \to ℳ$ satisfies a minor condition $\mathrm{\Sigma }$ if for every minor identity $f(x_1,\mathrm{\dots },x_n)\approx g(y_1,\mathrm{\dots },y_m)\in \mathrm{\Sigma }$ and for every assignment $s:\{x_1,\mathrm{\dots },x_n,y_1,\mathrm{\dots },y_n\}\to B$ we have

We say that a minion $ℳ$ satisfies $\mathrm{\Sigma }$ if there exists a map $\xi :\tau \to ℳ$ that satisfies $\mathrm{\Sigma }$.⁴⁴4It is convenient and standard practise to notationally drop the distinction between $f\in \tau$ and $\xi (f)\in ℳ$. If $\mathrm{\Sigma }$ and ${\mathrm{\Sigma }}^{\prime }$ are minor conditions, then we say that $\mathrm{\Sigma }$ implies ${\mathrm{\Sigma }}^{\prime }$ if every clone that satisfies $\mathrm{\Sigma }$ also satisfies ${\mathrm{\Sigma }}^{\prime }$. We present some concrete minor conditions that are relevant in the following.

The list of equivalent statements from Theorem 10 can now be extended as follows.

We will make crucial use of the following theorem.

The following lemma is used for the implication from (1) to (2) in the proof of Theorem 18. Note that in the canonical linear arc monadic Datalog program $\mathrm{\Pi }$ we can use the “strongest possible rules”⁵⁵5These comments are intended to illustrate the challenges in the proof of next lemma; it will not be necessary to formalise what we mean by strongest possible rules. when deriving the goal predicate. However, the canonical slam Datalog program ${\mathrm{\Pi }}_S$ might need to use weaker rules in order to be able to apply symmetric rules later on in the derivation. See Example 22.

A proof of the lemma can be found in the long version of the article which is available on ArXiv [10].

This section is devoted to the implication (3) to (4) in Theorem 18; the full proofs can be found in the long version of the article which is available on ArXiv [10]. We first present a general result about obstruction sets for finite-domain CSPs that closes a gap in the presentation of the proof of Lemma 21 in [16] and essentially follows from the sparse incomparability lemma (Theorem 7); we thank Víctor Dalmau for clarification.

Note that Theorem 17 implies that if $\mathrm{CSP}(𝔅)$ is solved by a linear arc monadic Datalog program, then $𝔅$ has caterpillar duality; the proof given in [16] only shows generalised caterpillar duality. However, Lemma 23 implies that $𝔅$ in this case also has (injective) caterpillar duality.

In order to prove the implication (3) to (4) in Theorem 18, it only remains to prove that $𝔅$ also has unfolded caterpillar duality (Lemma 25). We need the following lemma, which has already been mentioned in Section 2.6.

From this we obtain the implication (4) to (5) in Theorem 18.

We finally prove Theorem 18.