2.26. Complete Native Even Edge-CSP Solver🔗

Import CslibFrontier.Computability.PolyTime.CSP.Edge.Solver.Endpoint. The ordinary decision problem checks the actual edge/even-delta-matroid model internally and accepts exactly its satisfiable instances:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Complexity
  Cslib.Complexity.CSP Turing.MultiTapeTM in
example : EdgeSolver.evenEdgeSAT ∈ P (encCSP encTable encNat) :=
  EdgeSolver.evenEdgeSAT_mem_P

Each scope has distinct names; every occurring name appears twice in distinct constraints. Relations are nonempty even delta-matroids, with either common parity permitted. Duplicate constraints/rows, empty CSPs and true nullaries are included. Empty/false or malformed relations, wrong arities, repeated scope names and non-even relations reject. The all-raw runtime has no model premise:

open Cslib.Logic.PL.CSP Cslib.Complexity Cslib.Complexity.CSP
  Turing.MultiTapeTM in
example : ComputableInPolyTime EdgeSolver.solve
    (encCSP encTable encNat) (encOption (encList encBool)) :=
  EdgeSolver.computableInPolyTime_solve

Cslib.Complexity.CSP.EdgeSolver.optimize returns one original-order occurrence bit per port and minimizes the actual number of defective variables:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Complexity.CSP in
example (F : CSP Table ℕ) (h : EdgeSolver.checkModel F = true) :
    ∃ bits, EdgeSolver.optimize F = some bits ∧
      IsOptimalLabeling Table.sem (EdgeAugmenting.labeling F bits) :=
  EdgeSolver.optimize_spec F h

optimize = none means model rejection. An accepted unsatisfiable instance still has an optimal buffer; solve = none also covers positive minimum defect count. The actual finite program agrees with the semantic optimizer and decision:

open Cslib.Complexity.CSP.EdgeSolver in
example : Program.decideSAT [] = true := by⊢ Program.decideSAT [] = true decideAll goals completed! 🐙

open Cslib.Complexity.CSP.EdgeSolver in
example : Program.decideSAT
    [(⟨1, [[false]]⟩, [2 ^ 100]), (⟨1, [[true]]⟩, [2 ^ 100])] = false := by⊢ Program.decideSAT [({ arity := 1, rows := [[false]] }, [2 ^ 100]), ({ arity := 1, rows := [[true]] }, [2 ^ 100])] =
  false
  decide +kernelAll goals completed! 🐙

One improvement makes one recursive child call per blossom and immediately returns its lifted improvement or transferred optimum. The strict measure 2*numVars−positiveCount bounds contraction depth by 2*numVars; at most numVars+1 outer rounds are needed. Complete native bounds include framed rows, binary names/arities/positions, parent frames and quadratic central table data. Clocks traverse actual lists rather than intervals below binary values.

This completes the explicit-table edge layer of KKR v6 Theorem 21, using its Algorithm 1 and contraction/lifting mathematics; the recursion organization and encoded bookkeeping are original. CslibFrontierTests/EdgeCSPSolver.lean executes nonempty preparation, repeated copied constraints, changed outside values, multiple improvements, r=b and sparse 2^250 names. Geometry/recognition, ordered planar hardness and full #3091 remain open.