2.21. Prefix-Valid Edge-CSP Augmentation🔗

Cslib.Logic.PL.CSP.defects counts distinct inconsistent variables. Cslib.Logic.PL.CSP.Walk.IsFWalk requires distinct endpoints, consistent internal variables, and validity after every variable-ended prefix. An augmenting walk removes exactly two defects:

open Cslib.Logic.PL Cslib.Logic.PL.CSP in
example {Rel V : Type} [DecidableEq V] {F : CSP Rel V}
    (h : EdgeInstance F) {sem : Rel → List Bool → Bool}
    {f : OccurrenceLabeling F Bool} {w : Walk F}
    (hw : w.IsAugmenting sem f) :
    (defects (w.flip f)).card + 2 = (defects f).card :=
  hw.card_defects_flip_add_two h

For even delta-matroid constraints, Cslib.Logic.PL.CSP.EdgeInstance.augmentingWalk is a total deterministic two-phase routine. Its correctness requires an improving valid comparison labeling as input; it does not search for that labeling. The combined exchange count is bounded by half the initial occurrence Hamming distance.

open Cslib.Logic.PL Cslib.Logic.PL.CSP in
example {Rel V : Type} [DecidableEq V] {F : CSP Rel V}
    (h : EdgeInstance F) {sem : Rel → List Bool → Bool}
    (hM : EdgeInstance.EvenConstraints sem F)
    {f : OccurrenceLabeling F Bool} :
    IsOptimalLabeling sem f ↔ ValidLabeling sem f ∧
      ¬ ∃ w : Walk F, w.IsAugmenting sem f :=
  h.isOptimalLabeling_iff_no_augmentingWalk hM

The test module also rejects final-only validity. The search, contraction and complete native edge solver are documented below.

For explicit tables, Cslib.Complexity.CSP.EdgeAugmenting.run takes the CSP, two finite occurrence buffers and the excluded start. Its ordinary native certificate covers the full framed input, including malformed buffers and sparse binary names:

open Cslib.Complexity.CSP.EdgeAugmenting Turing.MultiTapeTM in
example : ComputableInPolyTime (fun input => (run input).isSome)
    encInput encBool := by⊢ ComputableInPolyTime (fun input => (run input).isSome) encInput encBool fun_propAll goals completed! 🐙

Cslib.Complexity.CSP.EdgeAugmenting.run_eq identifies its output with the mathematical routine when buffer widths match. Cslib.Complexity.CSP.EdgeAugmenting.run_spec supplies an actual augmenting walk and the combined exchange bound given a valid improving comparison. A none output does not establish unsatisfiability. The fresh forest search below uses only the base labeling and stops at its first blossom or augmentation. The complete behavioral clients are in CslibFrontierTests/EdgeCSPAugmentingNative.lean.