Valiant's XOR gadget

The four-node weighted graph of Valiant 1979 that couples two edges of a graph so that, in every cycle cover, exactly one of them is used: attached in place of the edges u → v and u' → v', the gadget has no cover of its own, no cover entering through one edge and leaving through the other, and no cover using both edges, while the covers using exactly one edge weigh 4 (DescriptiveComplexity.pdel_attachValiant). The first edge enters at node 0 and leaves from node 3; the second enters at node 3 and leaves from node 0. The six local values are computed by decide.

def DescriptiveComplexity.xorGadget : Fin 4 → Fin 4 → ℤ

Valiant's XOR gadget.

Equations

• DescriptiveComplexity.xorGadget = ![![0, 1, -1, -1], ![1, -1, 1, 1], ![0, 1, 1, 2], ![0, 1, 3, 0]]

@[reducible, inline]

abbrev DescriptiveComplexity.attachValiant {V : Type} [DecidableEq V] (M₀ : V → V → ℤ) (u u' v v' : V) : V ⊕ Fin 4 → V ⊕ Fin 4 → ℤ

Valiant's gadget attached in place of the edges u → v and u' → v'.

Equations

• DescriptiveComplexity.attachValiant M₀ u u' v v' = DescriptiveComplexity.attachXor M₀ DescriptiveComplexity.xorGadget u u' v v' 0 3 3 0

theorem DescriptiveComplexity.pdel_attachValiant {V : Type} [Fintype V] [DecidableEq V] (M₀ : V → V → ℤ) (u u' v v' : V) (A B : Finset V) (huu' : u ≠ u') (hvv' : v ≠ v') (hv : v ∉ B) (hv' : v' ∉ B) : pdel (attachValiant M₀ u u' v v') (Finset.map Function.Embedding.inl A) (Finset.map Function.Embedding.inl B) = 4 * ((if u ∈ A then 0 else pdel M₀ (insert u A) (insert v B)) + if u' ∈ A then 0 else pdel M₀ (insert u' A) (insert v' B))

The expansion of Valiant's gadget: four times the covers using exactly one of the two edges.