Tighten AllDifferent clause explanations via minimal Hall sets

[lifebeyondfife]

Motivation

AllDifferentInteger.Explain currently cites all N variables as the reason for any bound change, producing clauses with 2N literals. For NQueens with 12 variables, every AllDifferent clause has ~24 literals — far too broad for unit propagation to ever trigger.

The theoretical minimum is a Hall set explanation: if a bound change on variable x was caused by a Hall set {v1, v2, ..., vk} (k variables whose domains span exactly k values), the explanation need only cite the 2k bounds of those k variables, plus x's own bounds. For typical Hall sets (k = 2–4), this produces 5–9 literal clauses instead of 24+.

Current state

AllDifferentInteger already computes SCC-based Hall witnesses during propagation (added in #154). The sccBoundReasons dictionary maps SCC indices to the variable IDs that form each Hall set. However, Explain does not use this information — it falls through to the conservative "cite all variables" path.

Proposal

1. During Propagate(), when recording a bound change explanation via MergeExplanation, store the Hall witness variable set (from sccBoundReasons) alongside the bound change
2. In Explain(), emit only the bounds of the Hall witness variables (plus the affected variable) instead of all constraint variables
3. Guard the additional tracking behind ClauseLearningEnabled to avoid overhead when CL is off

Expected impact

• Clause size reduction from ~2N to ~2k+2 literals (where k is typically 2–4)
• May enable unit propagation from learned clauses for the first time
• Measurable via diagnostics from Add clause learning quality diagnostics #159

Acceptance criteria

• Explain emits only Hall witness bounds (not all N variable bounds) for bound changes caused by Hall set propagation
• Clause size for AllDifferent-sourced clauses is proportional to Hall set size, not total variable count
• All existing tests pass
• Unit test verifying explanation minimality on a small AllDifferent instance

Context

Part of the investigation phase for #158. Referenced as #160 in the epic's investigation checklist.