Temporal constraint satisfaction problems in fixed-point logic

DOI10.1145/3373718.3394750MaRDI QIDQ5145634zbMATH OpenOpenAlexWikidataFDO

Authors Manuel Bodirsky, Wied Pakusa, Jakub Rydval

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2002.09451

zbMATH Keywords

fixed-point logicMaltsev conditionstemporal constraint satisfaction problems

Mathematics Subject Classification ID

Logic in computer science (03B70) Operations and polynomials in algebraic structures, primal algebras (08A40) Applications of universal algebra in computer science (08A70)

Abstract: 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 coincides with an important dichotomy in universal algebra; in particular, the border 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.

Recommendations

• Datalog and Constraint Satisfaction with Infinite Templates
• Datalog and constraint satisfaction with infinite templates
• Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates
• The complexity of temporal constraint satisfaction problems
• Quantified Positive Temporal Constraints

Cited in

(23)

• On the descriptive complexity of temporal constraint satisfaction problems
• scientific article; zbMATH DE number 1222101 (Why is no real title available?)
• scientific article; zbMATH DE number 6863862 (Why is no real title available?)
• Smooth approximations: an algebraic approach to CSPs over finitely bounded homogeneous structures
• Tractable combinations of temporal CSPs
• Experimental analysis of numeric and symbolic constraint satisfaction techniques for temporal reasoning
• Efficient Temporal Satisfiability
• Affine Systems of Equations and Counting Infinitary Logic
• Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates
• Trends in Temporal Reasoning: Constraints, Graphs and Posets
• Datalog-expressibility for monadic and guarded second-order logic
• Smooth approximations and relational width collapses
• Complexity classification transfer for CSPs via algebraic products
• Quantified Positive Temporal Constraints
• Datalog and Constraint Satisfaction with Infinite Templates
• Temporal induction by incremental SAT solving
• Datalog and constraint satisfaction with infinite templates
• Smooth approximations and CSPs over finitely bounded homogeneous structures
• Search strategies for resolution in temporal logics
• Collapsing the bounded width hierarchy for infinite-domain constraint satisfaction problems: when symmetries are enough
• Discrete temporal constraint satisfaction problems
• Solving equation systems in ω-categorical algebras
• ASNP: a tame fragment of existential second-order logic

This page was built for publication: Temporal constraint satisfaction problems in fixed-point logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145634)