Documentation

CslibFrontier.Algorithms.Lean.EdgeCSP.Blossom.Optimality

Forward improvement and reference optimality transfer #

Lemma 42 of [KKR18], arXiv:1602.03124v6, printed p. 20, transfers optimality of the contracted reference back to the prepared original labeling. The constructive forward map below projects an original augmentation, stopping at its first internal port when necessary. Together with liftComparison_spec, it supplies the two mathematical outcomes needed after recursively optimizing the actual contracted instance.

source
def Cslib.Logic.PL.CSP.Blossom.projectAugmentation {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w p : F.Walk) :
Option ((contract f (internal w)).OccurrenceLabeling Bool)

Project an original augmenting walk, stopping at its first blossom variable if it enters. The all-outside case retains the honest reference central row. The entering case changes the central row to the actual touched-constraint indicator of the first internal port.

Instances For
    source
    theorem Cslib.Logic.PL.CSP.Blossom.projectAugmentation_spec {F : CSP Table ℕ} {w p : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (hp : Walk.IsAugmenting Table.sem f p) (hx : p.start ≠ w.start) :
    ∃ (g : (contract f (internal w)).OccurrenceLabeling Bool), projectAugmentation f w p = some g ∧ ValidLabeling Table.sem g ∧ (defects g).card + 2 = (defects f).card

    The executable forward construction projects every actual original augmentation starting away from the base and removes exactly two contracted-reference defects.

    source
    theorem Cslib.Logic.PL.CSP.Blossom.isOptimal_of_reference {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (hopt : IsOptimalLabeling Table.sem (reference f (internal w))) :
    IsOptimalLabeling Table.sem f

    Lemma 42 for the actual executable whole-instance contraction. Optimality of its prepared reference implies optimality of the original prepared labeling, with no model or oracle.