Parity Lifts Make Weisfeiler–Leman Refinement Detect Compatible Choices

The manuscript constructs two ordinary graphs whose behavior depends on whether a finite choice problem has a solution. If a compatible choice exists, Weisfeiler–Leman (WL) refinement distinguishes the graphs. If none exists, the graphs remain equivalent under the specified refinement, for every dimension k ≥ 4. That equivalence is not graph isomorphism: it means only that this comparison procedure cannot tell the graphs apart.

The choice problem has t finite domains. One element must be selected from each domain, and every pair of selected elements must agree on a shared label test. The reduction uses t = k + 1 for joint refinement and t = k for separate refinement.

The distinction between those refinement conventions is about what information survives an update. WL colors ordered k-tuples, initially recording equalities and adjacencies among their positions. To update a tuple, it considers replacing each position with a candidate vertex. Joint refinement keeps the full vector of replacement colors together for each candidate, preserving correlations across positions. Separate refinement keeps a separate multiset for each position, losing that correlation. Two graphs are equivalent when their tuple-color histograms agree at every round, with common color names.

A four-domain example makes the choice condition concrete. The domains encode partial Boolean assignments: one requires x = y, another y = z, and a third x = z; the fourth allows either value of z. Choosing all zeros satisfies the tests. But if the third requirement changes to x ≠ z, the first two force what the third forbids, so no compatible choice exists. Empty domains are allowed and make a choice impossible immediately.

To encode the choice system, the construction builds a template with t main vertices forming a clique. A template type is a designated role in this construction, such as a main vertex or a helper associated with a particular triple. For each pair of main vertices and each different third vertex, the template adds a helper adjacent to those three. In the t = 4 illustration, it has four main vertices and 12 helpers. Each main type is replaced by elements of its domain; each helper type is replaced by copies of the relevant pair labels. Main edges require matching labels. A helper checks the pair label at two of its neighbors, while connecting freely to the third domain. These types guide the construction, but the resulting graphs are uncolored.

The next step replaces each base vertex with bit tags. A tag has one bit for every neighboring template type, including types for which that particular base vertex has no neighbor. Along an edge, the two lifted vertices must agree on the bits facing each other.

In one graph, every tag has even parity: its bits sum to zero modulo two. In the other, tags at one main type have odd parity, while all other types remain even. Every positive-degree type has equally many even- and odd-parity tags, so the two graphs have the same number of vertices.

A compatible choice maps the whole template into the base graph: the selected domain elements supply the main vertices, and matching labels supply the helpers. For this fixed map, edge-bit agreement lets us assign one bit to each template edge. In the all-even graph, setting every edge bit to zero satisfies the parity requirements. In the altered graph, summing the vertex equations counts every edge bit twice, so the left side is zero modulo two. The right side is one, because exactly one main type has odd parity. The equations are inconsistent. Thus this template map lifts to the even graph but not to the altered one.

That single difference matters only if other maps cannot cancel it. The manuscript counts all adjacency-preserving maps, not just type-respecting ones. For any fixed projection—that is, a specified map from the construction’s vertices into the base graph—the tag constraints form a linear system Mz = b over the two-element field. With zero right-hand side, solutions form the kernel of M. With the twisted right-hand side, there are either no solutions or a translate of that kernel, giving the same number as before. Each projection therefore contributes either equal counts or an advantage for the even graph—never an advantage for the altered graph. The one strict difference survives in the total.

The converse is the harder direction: if WL distinguishes the graphs, why must there be a compatible choice? The manuscript uses a stated distinguishing homomorphism test and a tree decomposition of its test graph, with bags containing at most t vertices. The bags cover the test graph’s edges, and the bags containing any one vertex form a connected subtree. A linear-algebra certificate assigns binary weights to test vertices and edges, with odd total vertex weight for every template type.

After contracting adjacent identical bags, every remaining separator has at most t − 1 vertices. Some main type must therefore be absent from each separator. Its odd weight lies on exactly one side, which orients the decomposition edge toward that side. At a sink bag, every main type must be present: an absent type would contribute zero weight in the bag and on every outer side, contradicting its odd total. Since the bag holds at most t vertices, it has exactly one representative of each main type.

That does not yet give a compatible choice. The representatives need not form a clique, and their individual weights may be zero. The helper-based part of the certificate is what rules out mismatches: for a mismatched pair, the manuscript constructs a discrepancy with global weight one, while showing its weight is zero in the sink bag and on every outer side. This contradiction is the outline’s reason the pair must match; it is not a complete derivation of the helper calculation. The explainer explicitly says that boundary calculation is omitted, and its diagram is a proof roadmap rather than a substitute for the argument.

Together, the two directions give the switch: no compatible choice means the bounded-bag test counts agree and the graphs are WL-equivalent; a compatible choice gives a template count difference and WL distinguishes them. The helpers make the difference visible within at most two joint rounds or one separate round.

For the computational consequence, the manuscript groups clauses of a sparse 3-SAT instance into t domains. Each domain lists assignments satisfying one group, and shared labels enforce agreement on overlapping variables. The graph-size bound in the manuscript depends on the number of variables per group, with an additional factor depending only on the dimension k.

Under positive-rate ETH—the assumption that no deterministic algorithm solves 3-SAT in time 2^(δN) times a polynomial in input length, for some δ > 0—the manuscript rules out a deterministic O(n^(ck)) solver for some c > 0, for every sufficiently large fixed k. The stated result uses explicit adjacency matrices and a multitape Turing machine. It applies even to the early WL histograms: a small number of rounds does not make the computation cheap.