Complexity classification of temporal logic problems simplified and extended
Discrete Temporal CSPs et al
Computational Complexity
Summary
This paper looks at a kind of puzzle called constraint satisfaction problems (CSPs) that involve ordering numbers like integers. The authors revisited and fixed earlier work that classified how hard these puzzles are to solve. They showed that most puzzles that can be solved easily all work well with one standard solving method, instead of many different special tricks. Additionally, they simplified the way to study these puzzles and extended the results to similar puzzles on different structures, like infinite trees and lattices, categorizing them as either easy or hard to solve.
What this means in practice
- •For algorithm designers: Use the unified solving approach to design efficient solvers for temporal CSPs on integer orders and related structures.
- •For database query optimizers: Optimize queries involving temporal or ordering constraints by leveraging the complexity classification to identify tractable cases.
A theory result. No direct application yet.
Authors
Lukas Pieper
Abstract
We revisit the complexity classification of constraint satisfaction problems (CSPs) for first-order reducts of $(\mathbb{Z},<)$, established by Bodirsky, Martin, and Mottet in 2018. Following their approach, we give a self-contained proof of this classification, correcting several errors in the argument. We further show that, with the exception of cases arising from finite-domain CSPs, all tractable cases are solved by a well-known uniform algorithm, eliminating the need for the collection of ad-hoc algorithms used in the original paper. A central component of the proof allows the analysis to be restricted to first-order reducts of $(\mathbb{Z},<)$ that contain the successor relation. We substantially simplify this reduction and generalize the underlying construction. This generalization allows us to apply the same technique to first-order reducts of the triangular lattice graph and of infinite regular trees, yielding a complete complexity classification for these classes of structures, in particular a $\mathsf{P}$ versus $\mathsf{NP}$-complete dichotomy.