Bodirsky-Pinsker Tractability Conjecture for Infinite-Domain Constraint Satisfaction

Bodirsky-Pinsker Tractability Conjecture for Infinite-Domain Constraint Satisfaction

Definitions and mathematical statement

Fix a finite-signature reduct $A$ of a countable homogeneous relational structure $B$, where homogeneity extends every finite partial isomorphism to an automorphism, and finite boundedness describes the finite induced substructures by finitely many forbidden structures. The relations of $A$ are first-order definable in $B$. CSP$(A)$ takes a finite structure and asks for a homomorphism into the fixed template $A$. A primitive-positive definition uses existential quantifiers and conjunctions of atomic formulas. In the source's construction convention, primitive-positive powers and homomorphic equivalence determine whether $A$ can construct $K_3$. The assertion is \[ K_3\text{ has no such pp-construction from }A \quad\Longrightarrow\quad\operatorname{CSP}(A)\in\mathrm P. \] The template is fixed, not part of the finite input; its precise pp-construction convention is retained from the source.

Formulation and concept references: [S1].

Short English statement

For the specified infinite-domain templates, does the absence of a primitive-positive construction of three-coloring guarantee a polynomial-time constraint-satisfaction algorithm?

Research attempt

Scope, process, and first gap.

This attempt by GPT-6 Astra Ultra, dated 27 September 2026, proves the finite-certificate NP upper bound in the source's setting, gives an explicit tractable template with a polymorphism obstruction to constructing $K_3$, and tests reduction to a finite orbit quotient. The template is fixed throughout; it is not encoded as part of the instance.

Source [S1, Conjecture 1.4] separates the already-established algebraic consequence from the still-requested algorithmic implication. In particular the pseudo-Siggers conclusion is not itself treated here as an algorithm. The first gap is deriving a polynomial-time consistency procedure for every allowed template that does not pp-construct $K_3$.

Why these instances have finite certificates.

Use the source's finite relational signature for the finitely bounded homogeneous structure $B$. For a tuple of fixed length, its full atomic diagram, including equality and negated relation facts, determines its automorphism orbit: the coordinate correspondence is an isomorphism of the finite induced substructures, and homogeneity extends it to an automorphism.

There are only finitely many atomic diagrams of any fixed arity. Consequently each fixed first-order definable relation of $A$ is a union of finitely many tuple orbits, and is represented on $B$ by a quantifier-free formula listing those diagrams. The formulas are fixed with the template. No algorithm for discovering them from an arbitrary template presentation is required for this fixed-template statement.

Given an instance with $m$ variables, guess their equality classes, then guess a finite $B$-structure on those at most $m$ classes. If $r$ is the maximum relation arity of $B$, its full relation tables have $O(m^r)$ bits. Verify that it contains no induced embedding of any of the finitely many forbidden structures defining the age of $B$. Each forbidden structure has fixed size, so enumeration of all its candidate embeddings takes polynomial time.

Finally check each input constraint using the fixed quantifier-free formula for the corresponding $A$-relation. Negative atomic facts in those formulas are checked against the guessed full structure; they are not simply dropped.

If a homomorphism into $A$ exists, its finite image induces exactly such a certificate in $B$. Conversely a guessed structure passing the forbidden-substructure tests embeds into $B$, by finite boundedness, and its verified relation facts then give a homomorphism into $A$. This proves membership in NP. It does not replace the nondeterministic guesses by polynomially many deterministic choices.

A complete order-template algorithm.

Take $A=(\mathbb Q;<)$, which belongs to the stated class: finite strict linear orders are characterized by finitely many bounded-size failures of irreflexivity, totality and transitivity, and finite partial order-isomorphisms extend to automorphisms of the rational order.

An instance is a directed graph of requirements $x<y$. If it contains a directed cycle, transitivity and irreflexivity make it unsatisfiable. If it is acyclic, take a topological ordering and assign distinct increasing integers, viewed as rationals, to its vertices. Every required inequality is satisfied.

Thus cycle detection and topological sorting give a polynomial-time decision and construction procedure. A self-loop is correctly rejected as a cycle. No density property of the rational order beyond containing arbitrary finite chains is needed for this particular algorithm.

A direct certificate that this template cannot construct $K_3$.

The binary operation $\min$ preserves $<$: if $a_1<b_1$ and $a_2<b_2$, choose $j$ with $b_j=\min(b_1,b_2)$; then \[ \min(a_1,a_2)\le a_j<b_j=\min(b_1,b_2). \] It is also commutative. More generally, every operation preserving the basic relations preserves all primitive-positive definitions: apply it coordinatewise to satisfying tuples and their existential witnesses, and every atomic conjunct remains true. Coordinatewise operations likewise preserve pp-powers.

Suppose a pp-power of $A$ were homomorphically equivalent to $K_3$, with homomorphisms $g:K_3\to C$ and $h:C\to K_3$. The operation \[ f(a,b)=h\left(\min_C(g(a),g(b))\right) \] would be a commutative binary polymorphism of $K_3$, where $\min_C$ acts coordinatewise.

But no such operation exists. For distinct vertices $a,b$ of $K_3$, the pairs $(a,b)$ and $(b,a)$ are coordinatewise adjacent. Preservation of adjacency would require $f(a,b)$ and $f(b,a)$ to be adjacent, while commutativity makes them equal. The graph has no loops, a contradiction.

This proves absence of the specified pp-construction for this example without assuming $\mathrm P\ne\mathrm{NP}$. Both the algebraic premise and the algorithmic conclusion of the conjecture are therefore verified directly in this restricted template.

Why pp-constructions have the hardness direction.

A fixed primitive-positive definition can be expanded into a bounded-size constraint gadget: introduce its existential variables and impose its atomic conjuncts. A fixed power replaces each variable by a fixed-length tuple. Homomorphically equivalent templates have the same satisfiable finite instances, because a solution can be composed with either of the homomorphisms.

Consequently a fixed pp-construction of $K_3$ gives a polynomial-time reduction from graph three-coloring to the original CSP. This explains the direction used in the conjecture: construction of $K_3$ is a hardness certificate.

The contrapositive cannot be strengthened into the desired algorithm. Absence of one kind of hardness construction does not by itself enumerate solutions or establish a deterministic runtime. The established algebraic characterizations in [S1] add significant structure, but their conversion into a general algorithm remains the requested step.

A one-orbit quotient loses all order information.

All individual elements of $(\mathbb Q;<)$ lie in one automorphism orbit. Collapsing that orbit to one point and declaring the quotient relation true whenever some pair in the original relation exists gives a one-point template with a loop. Every directed instance maps to it, including a directed cycle, although cycles do not map to the rational strict order.

If instead the quotient relation requires every representative pair to satisfy $<$, the resulting relation is empty and even a single inequality is rejected. Neither choice is a correct reduction. Tuple orbits encode order relations between coordinates; unary orbits alone do not.

Homogeneity provides finite orbit information at each fixed arity. It does not say that replacing each variable by its unary orbit preserves compatibility among unboundedly many constraints.

Even a finite equivalent template need not exist.

The order example gives a stronger obstruction to importing the finite-domain dichotomy by a naive template replacement. Suppose a finite directed graph $H$ had exactly the same CSP as $(\mathbb Q;<)$. Every finite directed path is acyclic, so paths of arbitrarily large length would map into $H$.

Take a path longer than the number of vertices of $H$. Along its image some vertex repeats, yielding a directed closed walk and therefore a directed cycle in $H$. That cycle, regarded as a finite input, maps into $H$ but cannot map into a strict order. This contradicts the assumed equivalence.

Thus a tractable infinite-domain example in the conjecture's scope need not be homomorphically replaceable by any fixed finite template of the same relational type. More sophisticated finite reductions or promise constructions may still be useful, as [S1] investigates; the simple finite-template shortcut is disproved.

A second elementary tractable relation language.

For constraints using only equality and disequality on a countably infinite set, first merge equality-connected variables. If a disequality has both endpoints in one resulting class, reject. Otherwise assign distinct domain elements to all classes; the infinite domain supplies enough values. This is again polynomial time.

The argument is not a three-coloring algorithm: unrestrictedly many distinct values are allowed, while a three-element domain has a global shortage of colors. Nor is it a classification of every equality-definable relation, which may encode much more complicated disjunctions. The displayed language is the exact restricted subclass proved.

Verification and outcome.

Finite checks compare acyclicity with existence of assignments to sufficiently long finite chains, verify preservation by $\min$, and test the unary-orbit quotient on directed cycles. The pp preservation proof retains existential witnesses and the homomorphism direction. No unproved finite-template equivalence is used.

UNRESOLVED. The NP certificate mechanism, tractable order and equality examples, and the explicit nonconstruction argument are established. The first remaining gap is a uniform-in-input polynomial algorithm for each arbitrary allowed fixed template satisfying the conjecture's algebraic premise.

Sources

• S1 Pinsker, Rydval, Schöbi, Spiess and Winkler, Three Fundamental Questions in Infinite-Domain Constraint Satisfaction, arXiv:2502.06621v4 (6 May 2026). https://arxiv.org/html/2502.06621v4. Formulation source.