Table of Contents
Fetching ...

Symmetric Linear Arc Monadic Datalog and Gadget Reductions

Manuel Bodirsky, Florian Starke

TL;DR

This paper characterizes the finite-domain CSPs solvable by symmetric linear arc monadic (slam) Datalog as exactly those with a gadget reduction to CSP$(\mathfrak{P}_2)$, linking this power to unfolded caterpillar duality and universal-algebraic conditions. It develops a tight web of equivalences involving pp-constructability in $\mathfrak{P}_2$, minor conditions, minion homomorphisms, and the presence of quasi Maltsev and $k$-absorptive polymorphisms for all $n,k\ge1$, and proves the decidability of the slam-Datalog expressibility meta-problem. The results show slam Datalog is the smallest non-trivial gadget-closed fragment, and they provide a constructive method to derive slam programs when possible. Overall, the work integrates constraint satisfaction dualities, Datalog fragments, and algebraic polymorphism theory to illuminate the boundary between tractable and intractable finite-domain CSPs in a robust, computable framework.

Abstract

A Datalog program solves a constraint satisfaction problem (CSP) if and only if it derives the goal predicate precisely on the unsatisfiable instances of the CSP. There are three Datalog fragments that are particularly important for finite-domain constraint satisfaction: arc monadic Datalog, linear Datalog, and symmetric linear Datalog, each having good computational properties. We consider the fragment of Datalog where we impose all of these restrictions simultaneously, i.e., we study \emph{symmetric linear arc monadic (slam) Datalog}. We characterise the CSPs that can be solved by a slam Datalog program as those that have a gadget reduction to a particular Boolean constraint satisfaction problem. We also present exact characterisations in terms of a homomorphism duality (which we call \emph{unfolded caterpillar duality}), and in universal-algebraic terms (using known minor conditions, namely the existence of quasi Maltsev operations and $k$-absorptive operations of arity $nk$}, for all $n,k \geq 1$). Our characterisations also imply that the question whether a given finite-domain CSP can be expressed by a slam Datalog program is decidable.

Symmetric Linear Arc Monadic Datalog and Gadget Reductions

TL;DR

This paper characterizes the finite-domain CSPs solvable by symmetric linear arc monadic (slam) Datalog as exactly those with a gadget reduction to CSP, linking this power to unfolded caterpillar duality and universal-algebraic conditions. It develops a tight web of equivalences involving pp-constructability in , minor conditions, minion homomorphisms, and the presence of quasi Maltsev and -absorptive polymorphisms for all , and proves the decidability of the slam-Datalog expressibility meta-problem. The results show slam Datalog is the smallest non-trivial gadget-closed fragment, and they provide a constructive method to derive slam programs when possible. Overall, the work integrates constraint satisfaction dualities, Datalog fragments, and algebraic polymorphism theory to illuminate the boundary between tractable and intractable finite-domain CSPs in a robust, computable framework.

Abstract

A Datalog program solves a constraint satisfaction problem (CSP) if and only if it derives the goal predicate precisely on the unsatisfiable instances of the CSP. There are three Datalog fragments that are particularly important for finite-domain constraint satisfaction: arc monadic Datalog, linear Datalog, and symmetric linear Datalog, each having good computational properties. We consider the fragment of Datalog where we impose all of these restrictions simultaneously, i.e., we study \emph{symmetric linear arc monadic (slam) Datalog}. We characterise the CSPs that can be solved by a slam Datalog program as those that have a gadget reduction to a particular Boolean constraint satisfaction problem. We also present exact characterisations in terms of a homomorphism duality (which we call \emph{unfolded caterpillar duality}), and in universal-algebraic terms (using known minor conditions, namely the existence of quasi Maltsev operations and -absorptive operations of arity }, for all ). Our characterisations also imply that the question whether a given finite-domain CSP can be expressed by a slam Datalog program is decidable.
Paper Structure (23 sections, 15 theorems, 37 equations, 4 figures)

This paper contains 23 sections, 15 theorems, 37 equations, 4 figures.

Key Result

Lemma 2.5

Let ${\mathfrak B}$ be a finite structure with a finite relational signature, and let $\Pi$ be the canonical slam Datalog program for ${\mathfrak B}$. If ${\mathfrak A}$ is a finite structure with a homomorphism to ${\mathfrak B}$, then $\Pi$ does not derive the goal predicate on ${\mathfrak A}$.

Figures (4)

  • Figure 1: An example of the incidence graph of a caterpillar (left) and of a structure that is not a caterpillar (right).
  • Figure 2: Example of an $(a,b)$-unfolding ${\mathfrak T}'$ of a tree ${\mathfrak T}$.
  • Figure 3: At the top there is a picture of a caterpillar ${\mathfrak C}$. Below there is a visualisation of the tuples $t_{0,0},\dots,t_{3,3}$ introduced in the proof of Lemma \ref{['lem:interesting']}. The first column is $t_{0,0}$, the second $t_{0,1}$, and so on. The condition used to identify tuples is the ternary quasi minority condition. The colors indicate the equivalence classes of the $\leftrightarrow^\ast$ relation. Below we have the partially labelled sequence $a_0,\dots,a_{17}$ and the resulting sequence $A_0,\dots,A_5$. At the bottom there is the constructed unfolding of ${\mathfrak C}$.
  • Figure 4: The lattice of 2-element structures with respect to pp-constructability PPPoset; the structures HornSat, ${\mathfrak D}_2$, and ${\mathfrak P}_2$ were relevant in this text for characterisations of Datalog fragments (for arc monadic, linear arc monadic, and slam Datalog, respectively).

Theorems & Definitions (42)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Remark 2.4
  • Lemma 2.5
  • Theorem 2.6: Sparse incomparability lemma for structures FederVardi
  • Theorem 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 32 more