Optimization by successive two-defect improvements

Repeat the one-improvement routine at most one more than the number of occurring variables. Each successful call removes exactly two defects. The final labeling minimizes defects among all valid occurrence labelings, and it has zero defects exactly when the original CSP is satisfiable. There is no comparison input, optimizer provider or assumed lifting operation.

This is the optimization organization of Section 5 of [KKR18], arXiv:1602.03124v6, printed pp. 8–13. The finite recursion bookkeeping is original.

def Cslib.Logic.PL.CSP.Solver.optimizeAux (F : CSP Table ℕ) : ℕ → F.OccurrenceLabeling Bool → F.OccurrenceLabeling Bool

Run at most rounds improvements, stopping immediately when fresh search certifies optimality. Each improvement has its own fresh contraction-depth allowance.

theorem Cslib.Logic.PL.CSP.Solver.optimizeAux_spec (F : CSP Table ℕ) (rounds : ℕ) (f : F.OccurrenceLabeling Bool) (hr : (defects f).card < rounds) (hF : F.EdgeInstance) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) : IsOptimalLabeling Table.sem (optimizeAux F rounds f)

Enough outer rounds give an actual optimum. The premise is a finite defect count, not a promised optimizer or runtime certificate.

def Cslib.Logic.PL.CSP.Solver.optimize (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) : F.OccurrenceLabeling Bool

Compute a minimum-defect labeling using the original whole-instance contraction. Variable names are never used as loop bounds.

theorem Cslib.Logic.PL.CSP.Solver.card_defects_le_numVars (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) : (defects f).card ≤ F.numVars

Every defect is an occurring variable; no edge or validity hypothesis is needed.

theorem Cslib.Logic.PL.CSP.Solver.optimize_spec (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) : IsOptimalLabeling Table.sem (optimize F f)

The executable optimizer attains the minimum over all valid occurrence labelings. Its model is the actual ordered positional CSP Table ℕ; disconnected instances and duplicate constraints and rows are permitted.

theorem Cslib.Logic.PL.CSP.Solver.optimize_zero_iff (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) : (defects (optimize F f)).card = 0 ↔ Satisfiable Table.sem F

SAT correctness for the actual optimizer, including unsatisfiable edge instances with odd local parities. A zero-defect labeling is exactly a global satisfying assignment.