PaperlayerView exact revision on arXiv

Source-linked AI summary

Finite-on-Top-of-Temporal CSPs in Fixed-Point Logic

Manuel Bodirsky, Philipp A. Grzywaczyk

arXiv:2610.18287v1cs.LOmath.LO

TL;DR

The paper asks how fixed-point definability behaves for CSPs whose templates combine finite-domain and temporal structure. It classifies finite-on-top-of-temporal templates and proves a sampling-and-consistency algorithm correct; the resulting classification places positive cases in FP* and negative cases outside FPC.

  • Problem

    For CSP templates combining finite and temporal structure, the paper studies when the resulting problems are definable in fixed-point logic.

    Source: §1 · pp. 2–3

  • Method

    The paper samples a finite substructure, runs an extended constraint-singleton consistency algorithm, and combines consistency certificates using finite CSP theory and algebraic-product normal forms.

    Source: §5.3 · pp. 14–16, §8 · p. 21

  • Results

    Every CSP for a finite-on-top-of-temporal template is expressible in FP* or is not expressible in FPC.

    Source: §8 · p. 21

  • Takeaways & Limitations

    The classification identifies FP* as sufficient for the positive cases, while whether ordinary FP suffices throughout that class remains open.

    Source: §8 · p. 21

    The presented classification covers first-order expansions of Dk; the corresponding result for arbitrary first-order reducts is left to the full version.

    Source: §1.4 · p. 6

Abstract

from arXiv · show

We study definability in fixed-point logic with counting (FPC) for a class of constraint satisfaction problems (CSPs) that simultaneously generalises finite-domain CSPs and temporal CSPs. The templates for the CSPs are first-order expansions of the structure $([k] \times {\mathbb Q};<_1,\dots,<_k,\sim)$ where $<_i \, := \{((i,x),(i,x')) \mid x<x'\}$ and $\sim \, := \{((i,x),(i,x')) \mid i \in [k], x,x' \in {\mathbb Q}\}$, i.e., $k$ copies of $({\mathbb Q};<)$. Such a CSP is definable in FPC precisely when the template pp-constructs neither the ternary temporal relation $X$, which holds on three elements if the minimum is attained exactly twice, nor a nontrivial finite affine structure. Equivalently, the template has global polymorphisms that witness the tractability of the temporal CSPs on the copies, and that provide 3-4 weak near-unanimity operations on the set of copies of ${\mathbb Q}$. In this case, we prove that the CSP is even expressible in the less expressive logic FP$^*$, which is the restriction of FPC without counting terms (i.e., the extension of first-order logic by a fixed point operator and an ordered auxiliary number sort). Our algorithm samples finitely many values in each copy and then performs nested constraint-singleton consistency tests (which is a uniform polynomial-time algorithm for finite-domain CSPs). The correctness proof uses finite-domain CSP theory to combine consistency certificates by a single polymorphism term, fixing each variable to one copy without destroying the certificates needed for the temporal algorithm. We then use a known normal form for algebraic products to control the remaining interactions between different copies.

1 Introduction

The introduction places the paper at the intersection of finite-domain and temporal CSPs, asking how their descriptive complexity behaves when combined. It presents a classification for finite-on-top-of-temporal templates and sketches the sampling-and-consistency approach used to establish it.

1 Introduction

  • CSPs ask whether variables can be assigned values in a fixed template while satisfying all constraints, and their descriptive complexity varies with the allowed constraints.Some CSPs in P are not definable in fixed-point logic, motivating the study of which CSPs these logics capture.Source: §1 · p. 2

1.1 Finite on Top of Temporal

  • Finite-on-top-of-temporal templates are first-order expansions of k ordered copies of the rationals, with an equivalence relation identifying elements in the same copy.The class generalizes both finite-domain CSPs and temporal CSPs.Source: §1.1 · p. 3

1.2 Restricted Orbit Growth

  • Finite-on-top-of-temporal structures have polynomial restricted orbit growth, a setting connected to classifications of countable structures with polynomial orbit growth.The introduction places this setting within a broader hierarchy of orbit-growth classes.Source: §1.2 · p. 4

1.3 The Classification

  • For finite-on-top-of-temporal templates, FPC definability is equivalent to pp-constructing neither X nor any finite affine structure, and also to FP* definability.The theorem also gives an equivalent polymorphism characterization involving temporal operations on each copy and 3-4 weak near-unanimity operations on the colour set.Source: §1.3 · pp. 4–5

1.4 Algorithm and Proof Idea

  • The algorithm samples a finite substructure and runs constraint-singleton arc-consistency with an outer test over available tuples in auxiliary pair constraints.For correctness, finite CSP theory combines consistency certificates into a term, and algebraic-product normal forms help handle prescribed colours.Source: §1.4 · p. 5

1.3 The Classification

  • The classification combines temporal and finite-domain obstructions without requiring the same temporal operation on every part.The introduction notes that finite-domain CSPs have equivalent FP, Datalog, and FPC characterizations, while such equivalences fail for arbitrary infinite-domain templates.Source: §1 · pp. 2–3, §1.4 · p. 5

1.5 Related Work

  • The paper treats first-order expansions of Dk, while the full version is intended to extend the classification to arbitrary first-order reducts.Prior work introduced sampling for infinite-domain CSPs [9], developed it for combinations of theories [6], and applied it to temporal CSP algorithms [24, 28].Source: §1.4 · p. 6, §1.5 · p. 6

2 Preliminaries

The preliminaries set out the logics, relational structures, and algebraic tools used to study CSP definability. They also recall when temporal CSPs are expressible in fixed-point logic.

2.1 Fixed-Point Logic

  • FP extends first-order logic with fixed points; FPC adds counting terms and an ordered number sort, while FP* omits counting terms but retains the number sort and mixed-sort fixed points.The paper uses least fixed points for monotone operators.Source: §2.1 · p. 6

2.2 Relational Structures, CSPs and Polymorphisms

  • A CSP asks whether a finite input structure has a homomorphism to its template, and polymorphisms are operations preserving every template relation coordinatewise.Primitive-positive definitions use atomic formulas, conjunctions, and existential quantifiers; pp-constructability is defined via homomorphic equivalence to a pp-power.Source: §2.2 · pp. 6–7

2.3 Algebras and Terms

  • Algebras pair operations with a domain; terms recursively compose those operations, and powers interpret them coordinatewise.The subalgebra generated by a nonempty set is the smallest subalgebra containing it.Source: §2.3 · p. 7

2.4 Temporal CSPs

  • For temporal structures, FPC expressibility is equivalent to avoiding pp-constructions of both (0,1);1IN3 and X, and to preservation by one of several listed operations or a constant operation.The section also states that temporal CSPs with min, mi, or ll polymorphisms are expressible in FPC.Source: §2.4 · p. 8

3 Nested Singleton Consistency

The algorithm works with finite constraint lists and nested consistency checks. The finite cycle-consistency theorem supplies a solution criterion, and the procedure runs in polynomial time.

3.1 Tuber Systems

  • A tuber system stores allowed tuples per constraint; CSAC requires arc consistency and an arc-consistent certificate after fixing any listed constraint tuple.Arc consistency can be obtained by deleting tuples without matching projected values, and CSAC repeats singleton restrictions and consistency checks.Source: §3.1 · pp. 8–9
  • For finite relational structures with 3-4 weak near-unanimity polymorphisms, every cycle-consistent CSP instance has a solution.Cycle consistency requires each value of a variable to extend to a realization of every closed constraint walk starting and ending there.Source: §3.1 · p. 9

3.2 The Algorithm

  • The algorithm samples n values from each copy, initializes finite constraint lists and pair constraints, then repeatedly applies CSAC and tests pair-constraint tuples by singleton restriction.It rejects if a consistency check empties a list, removes tuples whose restriction fails, and accepts if the process terminates without an empty list; the procedure runs in polynomial time.Source: §3.2 · p. 9

4 Determining the Colours

The colour-determination argument builds a finite CSP on the copies’ colours from consistency certificates. Solving it yields a colour assignment and a finite CSAC system whose tuples respect those colours.

4 Determining the Colours

  • The accepted instance yields a finite colour algebra, and the projected certificate relations form an SAC system from which finite CSAC certificates can be obtained for each pair constraint and value.The construction closes sampled relations under the two polymorphisms and projects them to the finite set of colours.Source: §4 · pp. 10–11
  • A single polymorphism term combines the certificates to produce a finite CSAC tuber system whose tuples satisfy each constraint and use only the colour assigned to each variable.This is the colour-determined system required for the subsequent solution argument.Source: §4 · pp. 10–12
  • A finite auxiliary CSP with 3-4 weak near-unanimity polymorphisms is built from the colour domains, pair relations, and a generated relation; cycle consistency gives a solution constant across each variable’s copies.The generated relation preserves projections of the pair certificates, enabling the auxiliary instance’s consistency argument.Source: §4 · p. 12

5 Solutions from Determined Colours

The paper proves that a finite colour-determined CSAC system yields a solution. It controls interactions among copies using product normal forms and palette operations, then applies them to the coloured constraints.

5 Solutions from Determined Colours

  • A finite non-empty colour-determined CSAC tuber system guarantees a solution in the template with the prescribed colours.The proof combines normal forms for algebraic products with palette totally-symmetric maps.Source: §5 · p. 13

5.1 Syntactical Normal Forms for Algebraic Products of (Q; <)

  • The product normal form describes relations by clauses whose forms depend on whether a coordinate admits an ll-operation or instead has pp-operation support without a lex-operation.It provides syntactic control over relations across the copies.Source: §5.1 · p. 13

5.2 Palette Maps

  • Palette totally-symmetric operations preserve palette tuples, and if such polymorphisms exist for all block sizes, every instance with a finite non-empty CSAC system has a solution.The section gives their existence for temporal structures with mi or ll polymorphisms.Source: §5.2 · pp. 13–14

5.3 Proof of Lemma 15

  • The proof constructs palette operations preserving the coloured constraints, applies the palette-map solution theorem, and lifts the resulting solution to the original instance.The construction uses product normal forms to separate ll-invariant temporal relations from coordinate-specific constraints; correctness of the preceding algorithm follows by combining this lemma with colour determination.Source: §5.3 · pp. 14–15

6 Fixed-Point Implementation

The section gives a uniform FP* implementation of the algorithm for finite-on-top-of-temporal templates. Its sentence decides whether an input has a homomorphism to the template under conditions (a) and (b).

6 Fixed-Point Implementation

  • Ψ uses three nested fixed points for arc-consistency deletions, singleton tests for CSAC, and colour-pair tests.The tests perform currently justified deletions in parallel.Source: §6 · pp. 16, 18
  • Diagonal pair constraints store variable lists, while pinning a pair tuple lets the outer tests check whether CSAC survives fixing it.Adding Pt restricts the list containing t to that tuple; the diagonal constraints provide the information otherwise stored in variable lists.Source: §6 · pp. 16–17
  • Under conditions (a) and (b), the FP* sentence Ψ accepts exactly the finite structures that have a homomorphism to B.Thus CSP(B) is definable in FP*; inputs smaller than M are handled separately by a fixed first-order sentence.Source: §6 · pp. 16, 18
  • For inputs of size at least M, numerical codes represent colours, sampled values, constraint labels, and tuples in the constraint lists.The sample is [k] × [n], with one numerical variable for each value’s colour and rank; the smaller-input case uses κB.Source: §6 · pp. 16, 18
  • The correctness proof shows that the tests preserve a homomorphism’s tuples and that surviving pinned-pair certificates yield a homomorphism.It uses the finite non-empty colour-determined CSAC system obtained from the surviving certificates.Source: §6 · p. 19

7 Obstructions and the Classification

The section proves the obstruction side of the classification: failure of either polymorphism condition yields a pp-construction of X or a finite affine structure, making CSP(B) inexpressible in FPC. Together with the positive result, this establishes the stated equivalence.

Obstruction proof

  • Lemma 24 characterizes operations induced on one copy by global binary polymorphisms whose restrictions factor through an embedding.The proof uses order automorphisms for finite partial maps in one direction and compactness with downward Löwenheim–Skolem in the other.Source: §7 · pp. 19–20
  • If B fails either condition in Theorem 8, it pp-constructs X or a finite affine structure, and CSP(B) is inexpressible in FPC.Combined with the positive implication, this completes the equivalence of the four items in Theorems 7 and 8.Source: §7 · p. 20
  • Failure of condition (a) yields a temporal structure with no polymorphism from T, which pp-constructs X or a finite affine structure.The proof transfers this obstruction to B through pp-constructions and the preservation of FPC inexpressibility.Source: §7 · p. 20
  • Failure of condition (b) yields a clone on the colours lacking 3-4 weak near-unanimity operations, which pp-constructs a finite affine structure.The resulting pp-construction in B transfers FPC inexpressibility to CSP(B).Source: §7 · p. 20

Decidability

  • Given k and first-order definitions of B’s additional relations, it is decidable whether conditions (a) and (b) hold and hence whether CSP(B) is FPC-definable.The paper says this follows essentially from results and techniques in [11] and will be presented in the full version.Source: §7 · p. 20

8 Conclusion and Open Problems

The paper concludes that every CSP for a finite-on-top-of-temporal template is expressible in FP* or not expressible in FPC. The positive proof uses a costly sampling-and-consistency algorithm, while several complexity and logic questions remain open.

Conclusion

  • Every CSP for a finite-on-top-of-temporal template is expressible in FP* or not even expressible in FPC.The positive case uses finite sampling followed by an extension of constraint singleton arc consistency.Source: §8 · p. 21

Limitations and open problems

  • The positive algorithm is relatively expensive, and the authors do not know whether a simpler, less expensive consistency form suffices.Their proof strategy relies on the consistency method used.Source: §8 · p. 21
  • Whether ordinary FP suffices throughout the positive class remains open.The paper also identifies classification by P containment and NP-hardness for these templates as a research direction.Source: §8 · p. 21
Loading 2610.18287v1…