Source-linked AI summary

A dichotomy theorem for nonuniform CSPs

Andrei A. Bulatov

arXiv:1703.03021v2cs.CC

TL;DR

The paper addresses the complexity dichotomy for nonuniform constraint satisfaction problems over finite domains. It uses algebraic strategies and congruence-based tightening to construct algorithms, proving that every finite constraint language is either polynomial-time solvable or NP-complete, with a uniform algorithm for qualifying finite idempotent algebras.

  • Problem

    The paper addresses the open Dichotomy Conjecture asking whether every finite constraint language yields a polynomial-time solvable or NP-complete CSP.

    Source: §1 · p. 4
  • Method

    The proof develops algebraic strategies for block-minimal instances and tightens them through congruence-based domain reductions to solve quotient problems and reduce semilattice edges.

    Source: Technicalities · p. 18, §7 · p. 52
  • Results

    Every finite constraint language over a finite set has a CSP that is either solvable in polynomial time or NP-complete, and qualifying finite idempotent algebras have a uniform solution algorithm.

    Source: §1 · pp. 4–5
  • Takeaways & Limitations

    The dichotomy is confirmed for arbitrary finite constraint languages, while the solution algorithm for the algebraic formulation depends only on the finite idempotent algebra.

    Source: §1 · p. 4

    The strategy-reduction step uses the condition MAX(P) ∩ Center(P) = ∅.

    Source: §3.2 · p. 17

Abstract

from arXiv · show

In this paper we prove the Dichotomy Conjecture on the complexity of nonuniform constraint satisfaction problems posed by Feder and Vardi.

1 Introduction

The paper proves the Feder–Vardi Dichotomy Conjecture for every finite constraint language over a finite set, using an algebraic approach. It also establishes a uniform algorithm for finite idempotent algebras satisfying the conjecture’s tractability conditions.

Background

  • Nonuniform CSPs restrict allowed relations to a constraint language Γ and encompass homomorphism problems and MMSNP-equivalent problems.The paper focuses specifically on decision nonuniform CSPs among the many studied CSP variants.Source: §1 · p. 3

Prior work

  • The algebraic approach associates each constraint language with its polymorphism algebra and has yielded tractability results, algorithms, and refined complexity classifications.Prior confirmations covered languages over sets of size up to 7, conservative languages, and some digraph classes.Source: §1 · p. 4

Main results

  • For every finite constraint language Γ over a finite set, CSP(Γ) is either solvable in polynomial time or NP-complete.This confirms the Dichotomy Conjecture and gives the main complexity classification.Source: §1 · p. 4
  • The main technical achievement is a polynomial-time algorithm for languages satisfying the algebraic tractability condition and containing all constant relations {(a)}.The known hardness direction, together with this algorithm, implies the general dichotomy via.Source: §1 · p. 4
  • For a finite idempotent algebra satisfying the Dichotomy Conjecture’s conditions, the paper provides a uniform solution algorithm for CSP(A).The algorithm depends only on the algebra A, even when contained nonuniform problems CSP(Γ) may admit different algorithms.Source: §1 · pp. 4–5

Scope and organization

  • Theorems 1 and 2 motivate a Meta-problem: deciding whether a constraint language or finite algebra satisfies the stated conditions.The paper first develops an accessible algorithmic introduction, then presents further algebraic developments and technical proofs.Source: §1 · p. 5

Outline of the algorithm · 2 Introduction to CSP

The section defines nonuniform CSPs and develops their algebraic formulation through polymorphisms, invariant relations, idempotent algebras, congruences, and quotients. It then introduces bounded-width propagation and few-subpowers algorithms, including structural conditions yielding polynomial-time solvability.

2.1 CSP, universal algebra and the Dichotomy conjecture

  • A CSP instance consists of variables and explicitly represented constraint relations, and a solution assigns domain elements satisfying every constraint.The language may be infinite, in which case representation choices can affect complexity.Source: §2.1 · pp. 5–6
  • Polymorphisms preserve every relation in a constraint language, and shared polymorphisms support reductions between CSPs when one language’s polymorphisms include another’s.For finite Γ, if every polymorphism of Δ is also a polymorphism of Γ, then CSP(Γ) reduces to CSP(Δ) in polynomial time, even log space.Source: §2.1 · p. 6
  • The algebraic framework studies CSP(A) using relations invariant under algebra operations, with subalgebras, congruences, and quotient algebras as central structural elements.For idempotent algebras, constant relations are invariant and every congruence block is a subalgebra.Source: §2.1 · pp. 7–8
  • For finite idempotent algebras, CSP(A) is polynomial-time solvable exactly when A has a weak near-unanimity term operation; otherwise it is NP-complete.This is equivalent to every algebra in HS(A) having a nontrivial term operation, and the equivalence of these conditions with tractability is the paper’s main result.Source: §2.1 · p. 8

2.2 Bounded width and the few subpowers algorithm

  • Bounded-width algorithms tighten instances through local propagation, including 1-minimality and (k, k + 1)-minimality, while preserving invariance under the algebra’s term operations.A CSP has bounded width when some fixed-level minimality guarantees a solution; for idempotent algebras this is equivalent to solvability of every (2,3)-minimal instance.Source: §2.2 · pp. 9–10
  • Bounded width is characterized by weak near-unanimity terms of every arity k ≥3 and by the absence of module-equivalent algebras in HS(A).The characterization also requires every algebra in HS(A) to have a nontrivial operation.Source: §2.2 · p. 10
  • Few-subpowers algorithms generalize Gaussian elimination by exploiting polynomial-size generating sets for solution spaces, formally corresponding to only exponentially many invariant n-ary relations.Algebras with few subpowers admit polynomial-time CSP algorithms and can be characterized using edge terms.Source: §2.2 · p. 10
  • If an idempotent algebra has no semilattice edges, it has few subpowers and its CSP is solvable in polynomial time.A common binary term operation acts as a semilattice operation on every semilattice edge and otherwise produces either the first element or a semilattice edge.Source: §2.2 · p. 10

3 Solving CSPs

This section develops algebraic tools for analyzing CSP structure and uses them to design a polynomial-time recursive algorithm based on instance decomposition and reductions. It also identifies the condition MAX(P) ∩ Center(P) = ∅ as essential for the strategy reductions.

3.1 Congruence separation and centralizers

  • Congruence separation compares prime intervals via unary polynomials, and under mild conditions the resulting cannot-be-separated relation behaves as an equivalence relation.The same separation notion applies to prime intervals in different coordinate positions of a relation.Source: §3.1 · p. 11
  • Quasi-centralizers are introduced as a second key ingredient; large quasi-centralizers induce injective block mappings that can lift CSP solutions between algebra blocks.For blocks B and C connected by a semilattice edge, the mapping sends each a ∈ B to the unique corresponding ab ∈ C.Source: §3.1 · pp. 11–12

3.2 The algorithm

  • If corresponding prime intervals cannot be separated, CSP relations become aligned by quasi-centralizer blocks, allowing instances to split into subinstances whose domains are those blocks.Lemma 10 states that every solution belongs to one decomposed instance, with each variable domain restricted to a ζv-block.Source: §3.2 · p. 13
  • The full procedure handles semilattice-free domains with the few subpowers algorithm and otherwise uses block-minimality, quotienting, branching, or solution-preserving transformations to recurse on smaller CSPs.The transformation P · ϕ preserves solvability while reducing size, and block-minimality can be established by solving a quadratic number of strictly smaller CSPs.Source: §3.2 · pp. 14–15
  • When a subdirectly irreducible, (2,3)-minimal, block-minimal instance has no maximum-size variable in Center(P), Theorem 12 guarantees that it has a solution.Here MAX(P) ∩ Center(P) = ∅ is the stated condition.Source: §3.2 · p. 15
  • The algorithm runs in polynomial time because every recursive call strictly decreases the size of non-semilattice-free domains, bounding recursion depth by |A| for CSP(A).The procedure relies on Lemma 11 and Theorems 12 and 13, with recursion depth bounded by |A|.Source: §3.2 · p. 15
  • The reduction of strategies uses the condition MAX(P) ∩ Center(P) = ∅.This condition is invoked when β_v = μ∗.Source: §3.2 · p. 17
  • When β_v = μ∗, conditions (S1)–(S3) only give information about solutions to problems of the form P_W/μ∗ or something very close.Source: §3.2 · p. 17
  • This limitation creates a barrier that cannot be penetrated.The most important β-strategy conditions are stated here, with a complete precise list available in Section 9.3 or [23].Source: §3.2 · p. 17

Technicalities

This section develops algebraic preliminaries and operators underpinning the algorithm, then presents its recursive structure and key strategy-tightening theorem. The proof handles Abelian and non-Abelian cases through different transformations.

Technicalities

  • The technical framework extends results on colored graphs of algebras and relational structures [20], develops factor separation [22], and studies quasi-centralizers to split CSPs.These tools support the algorithm and advance prior results in Sections 4.4–4.6.Source: Technicalities · p. 18
  • The algorithm uses few subpowers when domains lack semilattice edges [11, 40], block-minimality otherwise, and quotienting by centers to recurse on smaller instances when block-minimality fails.Replacing domains by quotients modulo their centers reduces semilattice edges and enables recursion on smaller domains.Source: Technicalities · p. 18
  • Theorem 68 shows that a strategy for block-minimal instances can be tightened into a solution of the quotient problem required to reduce semilattice edges.Tightening repeatedly reduces domains to classes of maximal congruences; this is the proof’s most difficult technical component.Source: Technicalities · p. 18
  • The tightening transformations differ by congruence type: the Abelian case uses generalized rectangularity, whereas the non-Abelian case parallels bounded-width methods.These cases are treated separately in Sections 10.1 and 10.2.Source: Technicalities · pp. 18–19

4 Preliminaries

This section establishes the notation and preliminary structural tools used throughout the paper, covering universal algebra, CSP transformations and consistency, tame congruence facts, and coloured-graph machinery. It develops results on maximality, quasi-majority operations, connectivity and lifting, 2-decomposition, and rectangularity in linked subdirect products.

4.1 Universal algebra and CSP: notation and agreements

  • The notation also establishes polynomial operations, congruences, projections, subdirect products, and the standing assumptions that all algebras are finite, idempotent, and omit type 1.These conventions support componentwise operations and congruence calculations on algebraic relations throughout the paper.Source: §4.1 · pp. 19–20
  • CSP instances over finite idempotent algebras are defined with typed variables and invariant constraint relations, alongside tightening, quotient transformations, and standard minimality and consistency notions.The class of algebras is assumed closed under subalgebras and quotients, and constraint propagation can polynomially produce 1-minimal, (2,3)-consistent, or (2,3)-minimal instances.Source: §4.1 · pp. 20–21

4.2 Minimal sets and polynomials

  • For consecutive congruences, minimal sets are polynomially isomorphic and admit idempotent unary polynomials, while their traces and types characterize the relevant tame-congruence structure.Types 2–5 yield traces polynomially equivalent to vector spaces, Boolean algebras, two-element lattices, or two-element semilattices; type 1 is excluded under the paper’s tractability assumptions.Source: §4.2 · pp. 21–22

4.3 Coloured graphs

  • Coloured graphs encode semilattice, majority, and affine edge types through congruences and term operations, with type 1 omission characterized by connectivity of graphs on subalgebras.The paper thereafter assumes sm-smooth algebras and uses uniform witnessing operations, oriented thin edges, and their preservation under subalgebras, quotients, and projections.Source: §4.3 · pp. 23–25
  • Coloured-graph arguments construct binary term operations using projections, Mal'tsev operations, and module structure to obtain the required edge relations.The supplied proof fragments use projections on quotient algebras, Mal'tsev operations, and the fact that a quotient is a module.Source: §4.3 · pp. 26–27

4.4 Maximality

  • Maximality theory defines as-components and u-maximal elements, proves their directed connectivity and hereditary behavior, and lifts maximal, affine, and path structures through subdirect-product projections.The Maximality Lemma also extends these lifting properties to u-maximal elements and asm-paths; type-2 congruence intervals yield module-equivalent quotients whose pairs are thin affine edges.Source: §4.4 · pp. 27–29

4.5 Quasi-decomposition and quasi-majority

  • The 2-Decomposition Theorem yields a quasi-majority term operation whose repeated-input values remain as-connected to the repeated element, and hence stay in its as-component when it is as-maximal.The construction applies to finite classes of finite similar sm-smooth algebras omitting type 1.Source: §4.5 · pp. 30–31

4.6 Rectangularity

  • Rectangularity results show that linked subdirect products contain the full product of intersecting as-components, with extensions to blocks and path-connected subsets.The section also proves an auxiliary lemma guaranteeing a distinct as-maximal pair in a congruence block under the stated generation assumptions.Source: §4.6 · pp. 31–32

5 Separating congruences

This section develops separating congruences through the study of prime intervals, unary-polynomial behavior, and subdirect-product structure. It establishes separation and collapsing-polynomial results, while relating inseparable intervals to link congruences, minimal sets, and common types.

(2) If there is a (0

  • For algebras omitting type 1, a nontrivial as-component inside an α-block forces the prime interval 0 ≺ α to have type 2 or 3.The argument excludes types 4 and 5 using polynomial exchanges within the component, while type 1 is excluded by hypothesis.Source: (2) If there is a (0 · p. 34
  • If an α-block contains a semilattice or majority edge, then the prime interval 0 ≺ α has type 3, 4, or 5 rather than type 2.The block contains a non-Abelian subalgebra, which rules out type 2 for the interval.Source: (2) If there is a (0 · p. 35

5.2 Separation

  • Separation means that a unary polynomial preserves one prime interval’s lower congruence while failing to preserve the other’s, both in algebras and subdirect products.For subdirect products, the separating polynomial acts on congruences belonging to different factors.Source: §5.2 · p. 35
  • The algebraic and relational notions of separation coincide when an algebra is represented by its binary equality relation.The same unary polynomial induces the required actions on both projections.Source: §5.2 · p. 35
  • Any polynomial separating two prime intervals can be chosen idempotent with image equal to a minimal set for the interval it does not collapse.The construction composes the original separator with a polynomial mapping its image onto a minimal set, then takes a suitable power.Source: §5.2 · p. 36
  • Under chaining conditions, subtrace connectivity controls link congruences and yields weak symmetry: separation in one direction can be reversed when the target block has a nontrivial as-component.The reversing polynomial can be chosen to fix any two selected elements of that component.Source: §5.2 · pp. 36, 38
  • The proof’s structural claims show that (c, d) is as-maximal in a lk2-block and (a, a) is as-maximal in Q′′, enabling the final Rectangularity argument.These maximality properties support the construction of a subalgebra containing (a, a, c, d) in Q′.Source: §5.2 · pp. 40–41
  • The separation proof establishes that for each relevant (α, β)-subtrace {a′, b′}, some polynomial identifies a′ and b′ while fixing c and d.Claims 5 and 6 provide the required tuple and polynomial constructions, with the argument handled in two cases.Source: §5.2 · pp. 41–42
  • A composed polynomial collapses every relevant β-pair in B′1 while acting identically on c and d.The construction uses a finite sequence of pair-collapsing polynomials whose image strictly decreases until no listed pair remains.Source: §5.2 · p. 43

5.3 Collapsing polynomials

  • Prime intervals that cannot be separated share minimal sets, and a subdirect product admits an idempotent polynomial mapping one factor onto a minimal set for the other interval.Lemma 47 establishes these consequences of mutual non-separability.Source: §5.3 · p. 43
  • An αβ-collapsing polynomial minimizes the image while collapsing every prime interval separable in either direction from (α, β), within prescribed congruence blocks.The definition applies to a subdirect product R and selected congruence bounds βj.Source: §5.3 · p. 44
  • If R is chained with respect to B, β = βi, and priR′/α has a nontrivial as-component, an αβ-collapsing polynomial exists.Lemma 48 obtains such a polynomial by choosing an idempotent polynomial with minimal possible image and showing it is αβ-collapsible.Source: §5.3 · p. 44
  • Collapsing-polynomial arguments derive a contradiction by producing g with |g(R)| < |f(R)|, violating the minimality of f(R).The displayed passage records the final contradiction in the collapsing-polynomials argument.Source: §5.3 · p. 44

5.4 Separation and minimal sets

  • If the common interval type is not 2, each factor’s link congruence meets the upper congruence below the lower one: lk1 ∧β ≤α and lk2 ∧δ ≤γ.Lemma 49 derives these link-congruence inequalities under inseparability and typ(α, β) ≠ 2.Source: §5.4 · p. 44
  • Minimal-set analysis shows that the restricted subdirect product must satisfy R ∩(U1 × U2) ⊆{(1, 1′)} ∪(({0} ∪T1) × ({0′} ∪T2)).The proof studies traces and tails using polynomial operations, with projection and semilattice cases leading to this structural restriction.Source: §5.4 · pp. 44–45
  • Inseparable prime intervals in the two factors have equal types: typ(α, β) = typ(γ, δ).This is Corollary 50 for subdirect products when both prime intervals cannot be separated.Source: §5.4 · p. 46

6 Centralizers and decomposition of CSPs

The section develops a quasi-centralizer on congruence lattices and connects inseparable congruence intervals with algebraic and CSP decompositions. It establishes structural mappings between blocks and alignment properties underlying decomposition into smaller-domain instances.

6 Centralizers and decomposition of CSPs

  • The section introduces a congruence-lattice operator ζ(α, β), called the quasi-centralizer, and studies its role in CSP decompositions.ζ(α, β) is defined through preservation of whether term operations collapse β into α.Source: §6 · p. 46, §6.1 · p. 46

6.1 Quasi-Centralizer

  • ζ(α, β) is an equivalence relation and the greatest relation whose coordinatewise pairs preserve the condition f_a(β) ⊆ α.This characterization also supports showing that ζ(α, β) is preserved by term operations and hence is a congruence.Source: §6.1 · pp. 46–47
  • If ζ(α, β) ≥ β, then (α, β) has type 2, and comparable β-blocks in one ζ-block admit injective mappings preserving α-block order.For any thin edge B ≤ C in A/β, the mapping σ: B/α → C/α satisfies a ≤ σ(a) and excludes other elements of C/α.Source: §6.1 · p. 47
  • For any thin edge between β-blocks in one ζ-block, explicit semilattice, majority, or affine polynomials induce injective maps between their α-quotients; mutually asm-connected blocks have equal quotient sizes.These mappings also propagate αβ-minimality along asm edges under the stated inseparability and type-2 conditions.Source: §6.1 · pp. 48–49

6.2 Decomposition of CSPs

  • When congruence intervals cannot be separated, corresponding coordinates are quasi-centralizer-aligned, enabling consistent blockwise decompositions of (2,3)-minimal CSP instances.Alignment identifies congruence classes across projections; consistency of these mappings represents the instance as a disjoint union of smaller-domain instances.Source: §6.2 · pp. 50–51

7 The Congruence Lemma

This section develops closure and link-congruence lemmas supporting the Congruence Lemma, with results constraining polynomially closed subdirect products. It establishes inclusion for one congruence block and propagates it to other blocks using injective term-operation mappings.

Closure properties

  • Lemma 61 establishes that polynomially closed relations are preserved under suitable intersections, common pp-definitions, and quotienting by coordinate congruences.The analogous as-closure properties are also preserved under these three constructions.Source: §7 · p. 52

Congruence Lemma 64

  • The Congruence Lemma 64 shows that under chaining and polynomial-closure conditions, a restricted generated congruence behaves as the corresponding link congruence.The result addresses when restrictions of link congruences and generated congruences agree on suitable subalgebras and blocks.Source: §7 · p. 53

Auxiliary link-congruence lemmas

  • For linked type-2 intervals, the relevant link congruence has two alternatives: it is contained in γ on the ζ2-block, or it contains δ/γ on its u-maximal elements.In the second case, all δ-blocks above the selected block remain nontrivial modulo γ.Source: §7 · p. 53
  • When the link congruence is nontrivial, any element related to a δ-block is related, modulo γ, to the entire block.Formally, either the relevant rectangle is empty or {c} × B/γ is contained in the relation quotient whenever c has a neighbor in B.Source: §7 · pp. 53–54

Congruence Lemma 64

  • The Congruence Lemma gives either η = β2 or a congruence η on A2 forming an inseparable prime interval with the interval on A1.In the latter case, the restricted relation is the graph of a mapping from B′′2 to C whose kernel is η restricted to B′′2.Source: §7 · p. 55
  • The proof establishes {c} × aθ ⊆ R′ for a specific θ-block, using polynomial closure and the arbitrariness of b′ in aθ.Source: §7 · p. 57
  • For a neighboring θ-block E′, the mapping g is injective on E and, depending on the edge type, yields {c} × E′ ⊆ R′.For affine edges, g maps into {d} × E′ before the preceding argument gives the desired inclusion.Source: §7 · p. 57

8 Chaining

The section strengthens chaining to strong chaining and proves that this property is preserved under specified relation transformations. The preservation lemma is then used to maintain condition (S7) when transforming a β-strategy.

Definitions

  • Strong chaining is introduced as a strengthened relation property, with conditions (Q1s) and (Q2s) based on congruences and preserving polynomials.The section defines strongly chained relations and associated good polynomials before establishing its preservation.Source: §8 · pp. 57–58

Preservation lemma

  • Lemma 65 proves that strong chaining is preserved when restricting a subdirect product to specified congruence blocks and modifying one block through a nontrivial as-component.The lemma considers R′ = R ∩ (B1 × · · · × Bn) and corresponding block transformations, preserving strong chaining with respect to the new blocks.Source: §8 · p. 58

Proof of Lemma 65

  • The preservation proof separates linked and non-linked cases for a two-coordinate projection, with the non-linked case forcing one link congruence to be trivial.For a non-linked Q′, Claim 1 establishes lk2 = 0, while the alternative yields the required congruence behavior for the proof.Source: §8 · pp. 58–59
  • In the linked case, maximal as-components are preserved, and Claim 2 supplies good polynomials connecting pairs within the relevant component.The proof shows amax(E′′) is a union of as-components of E′ and constructs a (γ, δ, D)-good polynomial mapping any chosen pair to a pair in the same component.Source: §8 · pp. 59–60
  • Sequences of preserving polynomials are adjusted to remain inside the required component and fix the selected coordinate, using majority operations and a ternary term operation.The construction handles affine edges with a term operation p satisfying p(a,a,b) in b’s component and p(d_t+1,d_t,d_t) = d_t+1.Source: §8 · pp. 60–61

9 Strategies and solutions

This section develops polynomial-time CSP-solving strategies based on preprocessing, recursive reductions, and β-strategies for constructing solutions from compatible local relations. It establishes correctness and running-time bounds while handling centralizers and reducing to cases addressed in later sections.

9.1 The grand scheme

  • Every CSP instance can be reduced in polynomial time to an equivalent subdirectly irreducible instance, and a (2,3)-minimal instance can be made block-minimal by solving a quadratic number of strictly smaller CSPs.Block-minimality supports the case analysis that either solves the instance or enables further reductions.Source: §9.1 · pp. 61–62
  • Algorithm SolveCSP correctly solves every instance in CSP(A) in polynomial time, with running time O(n^3k), where k is the maximal algebra size.Its recursion uses strictly smaller instances, and the semilattice-free case is handled by the few subpowers algorithm [21].Source: §9.1 · pp. 63, 65

9.2 Proof of Theorem 69

  • Theorem 69 is supported by consistent idempotent mappings whose retraction preserves solvability and strictly shrinks domains on relevant variables, yielding a strictly smaller equivalent problem.The mappings can be found by solving a linear number of auxiliary instances, and the retracted algebras retain a weak near-unanimity term.Source: §9.2 · p. 66

9.3 Strategies

  • Strategies encode compatible subalgebra relations so that their induced constraints form a nonempty (2,3)-strategy and compatible tuples extend to solutions of the relevant subinstances.The extension condition differs according to whether the associated triples belong to W′.Source: §9.3 · p. 67
  • Conditions (S1)–(S3) are the desired invariants, while technical conditions (S4)–(S7) ensure they remain preserved during strategy transformations.The technical conditions involve subalgebra, closure, extension, and strong-chaining properties of the relevant relations.Source: §9.3 · pp. 67–68
  • The strategy framework aims to choose compatible relations whose resulting assignments give a solution of P.The collection of relations R = {R_C,v,αβ} is used to obtain assignments for all v ∈ V; the goal is to show these assignments form a solution.Source: §9.3 · p. 68
  • The reduction of strategies uses the assumption MAX(P) ∩ Center(P) = ∅; otherwise the available information is confined to problems of the form P_W/µ* and cannot cross the resulting barrier.This restriction motivates separating the analysis into two cases.Source: §9.3 · p. 68
  • The remaining analysis splits according to whether a nontrivial pair has type 2 or has type 3, 4, or 5.Case 1 considers some v and α ≺ β_v nontrivial on B_v with typ(α, β_v) = 2 in Section 10.1; Case 2 considers all such pairs with types in {3, 4, 5} in Section 10.2.Source: §9.3 · p. 68

10 Proof of Theorem 68

This section proves Theorem 68.

  • The remaining part of the paper provides the proof of Theorem 68.Source: §10 · p. 68

10.1 Tightening affine factors

This section develops the Case 1 tightening strategy for affine factors, transforming relations around a type-2 congruence interval and establishing the required compatibility and strategy conditions. It completes Theorem 76 by verifying conditions (S1)–(S7), including the preservation and extension properties of the tightened relation R′.

10.1 Tightening affine factors

  • The section targets a tightening strategy with α ≺ β_v and typ(α, β_v) = 2, exploiting the resulting module structure of β_v-blocks.The construction selects an α-block inside a β_v-block and uses this module structure to transform the strategy and induced congruences.Source: §10.1 · p. 69, §10.1.1 · p. 69

10.1.1 Transformation of the strategy and induced congruences

  • The transformed relations preserve a controlled projection structure: relevant compatible tuples are u-maximal elements of restricted original relations, with product containment modulo induced congruences.This structural relation is used to define and analyze the new strategy and its congruences.Source: §10.1.1 · p. 72

10.1.2 Condition (S6)

  • Condition (S6) holds for the transformed strategy: compatible tuples are polynomially closed in the corresponding projection.The proof transfers polynomial closure from the original relations while keeping tuples within the same induced congruence block.Source: §10.1.2 · p. 72

10.1.3 Condition (S1)

  • Condition (S1) holds: the u-maximal compatible relations for variable sets of size at most two form a nonempty (2, 3)-strategy for the transformed instance.The proof uses an auxiliary module-intersection lemma together with the original strategy and the induced congruence cases.Source: §10.1.3 · pp. 72–73
  • The proof of Condition (S1) proceeds through congruence cases, auxiliary subalgebras, and polynomially closed relations to extend compatible tuples.The supplied passages document the case analysis and constructions but do not state a standalone theorem conclusion for (S1).Source: §10.1.3 · pp. 75–76

10.1.4 Conditions (S2), (S3)

  • Lemma 80 proves that R′ satisfies (S2), handling the three choices of quotient variables Y through a unified extension argument.The proof reduces the cases to common properties of the relevant problems and extends u-maximal tuples to R′-compatible solutions.Source: §10.1.4 · pp. 76–78
  • The main technical hurdle is disentangling un-factored tuples from quotient congruence blocks, addressed by duplicating variables and introducing auxiliary relations Q and S.These constructions compare attainable blocks in the original and auxiliary relations while preserving projections and congruence information.Source: §10.1.4 · pp. 78–79
  • Claim 1 shows that the relevant relation is a union of η1-blocks, identifies θ1 with η1, and places each corresponding block product inside S′.Consequently, the attainable τ-blocks for extending a tuple are the same under both congruence analyses, enabling nearly arbitrary extensions.Source: §10.1.4 · p. 79
  • R′ satisfies (S3): every R′-compatible tuple in umax(pr_I R) extends to an R′-compatible tuple in R.The proof reduces to the corresponding conditions for R and repeats the extension argument with a simpler membership claim.Source: §10.1.4 · p. 82

10.1.5 The remaining conditions

  • Theorem 76 is completed because conditions (S1)–(S3) and (S6) were established earlier, while (S4), (S5), and (S7) follow from the preceding structural and maximality lemmas.For (S4), R′ relations are subalgebras and their quotient structures are modules; (S5) follows from (S3) and the corresponding property for R, and (S7) follows from Lemma 65.Source: §10.1.5 · p. 83

10.2 Tightening non-affine factors

This section tightens a non-affine factor by constructing and validating a strategy through domain restriction, aligned congruences, compatible extensions, and conversion to a minimal instance.

10.2.1 Step 1.

  • Proposition 83 establishes that the Q-relations support the required extensions, projections, and subdirect-product properties needed for the restricted instance.In particular, Qxy is a subdirect product of Qx × Qy, and compatible tuples extend to compatible tuples in constraint and auxiliary relations.Source: §10.2.1 · p. 84
  • The collection of relations R′′ constructed above satisfies all the conditions of a stated result, and the cited sets contain all the as-maximal Q-compatible tuples from corresponding collections.Source: §10.2.1 · p. 87

10.2.2 Step 2.

  • Step 2 uses aligned congruences to restrict every variable in Wv,αβv to a corresponding block while preserving extendability of maximal tuples and solutions.Lemma 87 supplies αw ≺ βw and an isomorphism between Bv/α and Bw/αw; Lemma 88 then provides compatible extensions after these domain restrictions.Source: §10.2.2 · pp. 90–91
  • Lemma 89 provides the main structural result: compatible tuples are preserved and extendable, and maximal tuples in the constructed relations retain the required relation to the original relations.Its proof derives pairwise compatibility using (2,3)-consistency, polynomial closure, and the Congruence Lemma, then extends tuples one variable at a time.Source: §10.2.2 · pp. 91–92
  • The preservation argument proceeds inductively while converting the instance to a (2,3)-minimal and block-minimal form, handling both ordinary consistency enforcement and congruence-defined cases.Lemma 88 supplies the necessary P-compatible relations and allows witnesses or extensions to be chosen in the restricted domains B′.Source: §10.2.2 · p. 93
  • R∗ is shown to satisfy the required strategy conditions, including nonempty relations, subalgebra structure, maximality, as-closeness, and the final closure condition.These conditions follow from the construction together with Lemma 89, Lemma 65, and the corresponding properties of R.Source: §10.2.2 · pp. 93–94

Index

The index lists terminology spanning algebraic structures, congruences, paths, compatibility notions, and CSP operations. It also provides page references for key concepts such as minimal instances, monoliths, and edge types.

Index coverage

  • Additional entries address link congruences, link tolerances, linked relations, globally minimal and minimal instances, and tightening of a CSP.The index also includes extensions of polynomials and type functions.Source: Index · pp. 99–100
  • Algebraic and structural entries include majority type, maximal components, maximal congruence, minimal sets, modules, and monoliths.These entries are indexed on pages 13, 21, 23, 25, and 70.Source: Index · p. 99
  • Compatibility and operation entries include P-compatible and T-compatible relations, term operations, relation-preserving operations, and pseudo-meet operations.The index also lists projections, polynomially isomorphic sets, and witnesses of a type.Source: Index · pp. 99–100
  • The index covers semilattice and connectivity terminology, including s-paths, semilattice paths, separated intervals, separating polynomials, and strongly chained relations.Related entries include semilattice free algebras, semilattice types, and strongly semilattice-connected components.Source: Index · p. 100

Notation

This section defines the notation used throughout the paper, including symbols for structures, polymorphisms, relations, and constraint satisfaction instances.

Notation

  • The notation includes symbols for constraint satisfaction problems and related parameters, such as P = (V, C), MAX(P), p(P), and size(P).It also lists symbols including A, G(A), hab, lk1, lk2, maj, max(A), SP, PW, and P′.Source: Notation · p. 101
  • The section defines notation for polymorphism structures and relations, including Pol(A), Pol1(A), prIR, Qx, Qxy, and QA.Additional symbols include PR, P x, P xy, and P x y-related notation as listed in the section.Source: Notation · p. 101
  • Further notation covers auxiliary quantities and objects, including W ′, tab, tol1, tol2, T x, T xy, umax(A), and WP(.The passage also lists size(P), which is separately used among the notation symbols.Source: Notation · p. 101
Loading 1703.03021v2…