Temporal Constraint Satisfaction Problems in Fixed-Point Logic
Manuel Bodirsky, Wied Pakusa, Jakub Rydval
摘要
Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q; <); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper1
问问它们各自怎么用它它引用的顶会 Paper1
相关 Paper
- Algebraic and algorithmic synergies between promise and infinite-domain CSPsAntoine MottetLICS 2025 · 被引用 1 次
- ∏2P vs PSpace Dichotomy for the Quantified Constraint Satisfaction ProblemDmitriy ZhukFOCS 2024 · 被引用 2 次
- Canonical Polymorphisms of Ramsey Structures and the Unique Interpolation PropertyManuel Bodirsky, Bertalan BodorLICS 2021 · 被引用 6 次
- Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationHiroshi Unno, Tachio Terauchi, Yu Gu, Eric KoskinenPOPL 2023 · 被引用 23 次
- Solving Infinite-Domain CSPs Using the Patchwork PropertyKonrad K. Dabrowski, Peter Jonsson, Sebastian Ordyniak, George OsipovAAAI 2021 · 被引用 5 次
