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.
翻译:当且仅当Datalog程序在约束满足问题(CSP)的不可满足实例上推导出目标谓词时,该程序可解决该CSP。对于有限域约束满足问题,存在三个特别重要的Datalog片段:弧一元Datalog、线性Datalog与对称线性Datalog,各自具备良好的计算性质。本文研究同时施加所有这些限制的Datalog片段,即探讨\emph{对称线性弧一元(slam)Datalog}。我们通过构件归约到特定布尔约束满足问题,刻画了可由slam Datalog程序求解的CSP类别。同时提出基于同态对偶(称为\emph{展开毛虫对偶})的精确刻画,并在泛代数层面(利用已知的次要条件,即对所有$n,k \geq 1$存在拟Maltsev运算与$nk$元的$k$吸收运算)给出特征描述。我们的刻画结果还表明:判定给定有限域CSP是否可由slam Datalog程序表达的问题是可判定的。