Persist learned clauses across incumbents in optimisation search

[lifebeyondfife]

Motivation

StateInteger.Search(optimiseVar) calls LearnedClauses.Clear() and PropTrail.Clear() at every improving incumbent. Clearing the propagation trail is correct (the search restarts from depth 0), but clearing the clause store discards knowledge that is still valid: a learned clause is implied by the constraint set plus the objective bound in force when it was learned, and each new incumbent only tightens that bound, so every stored clause remains implied for the rest of the run.

The cost is highest exactly where clause learning should pay off: late in an optimisation run, when the search is re-proving large subtrees infeasible under a slightly tighter bound, all previously learned refutations are gone.

Proposal

• Stop clearing LearnedClauses on incumbent improvement; keep clearing PropTrail
• Clause literals reference variable ids and bound values only, so no re-indexing is needed when the optimisation constraint is replaced
• Watch lists self-repair lazily in NotifyBoundChange, but verify watches behave sensibly after a full backtrack to root (all literals may be non-falsified again)
• ReduceDatabase becomes the only bound on store growth across incumbents; confirm MaxClauses remains appropriate

Acceptance criteria

• Optimisation results unchanged on the calibration regression guards (j3010_1, j3014_4, j6026_2, j6017_1, ft06, la06 all prove their published optima)
• calibrate probe --family jssp and --family rcpsp with clause learning enabled show zero UNSOUND rows
• Add clause learning quality diagnostics #159 counters demonstrate clauses surviving incumbents and triggering unit propagations in later iterations
• Unit test covering an optimisation run with clause learning enabled across at least two incumbents

Context

CDCL Phase 1 (follow-on from #164, which wired sound backjumping). Precedes the #159 measurements that gate the #158 epic decision.