AllDifferent: precise Hall witness reason generation

[lifebeyondfife]

Background

The clause-learning branch added IExplainableConstraint — a per-propagation explanation interface used by ConflictAnalyser during 1-UIP resolution:

public interface IExplainableConstraint : IConstraint
{
    void Explain(int variableId, bool isLowerBound, int boundValue, IList<BoundReason> result);
}

When a constraint implements this interface, StateInteger.ComputeEagerExplanation calls Explain to get a precise reason for each bound change. Without it, the fallback emits all constraint variable bounds as the reason — which is unsound when domains have holes from interior value removals (see #152).

Goal

Implement IExplainableConstraint on AllDifferentInteger so that clause learning can produce sound learned clauses for conflicts involving AllDifferent propagation.

What's needed

• Implement IExplainableConstraint on AllDifferentInteger
• Explain(variableId, isLowerBound, boundValue, result) is called after propagation to explain why a specific bound change occurred. It must append to result the BoundReason literals that justify the propagation
• For value removal (Régin's algorithm removed value v from variable X, causing a bound change): identify the Hall set — the subset S of variables whose combined domains forced v out of X's domain — and emit the bounds of variables in S as the reason
• The Hall witness can be extracted from the residual graph of the bipartite matching: a Hall set corresponds to a subset reachable from the unmatched value nodes

Acceptance criteria

• AllDifferentInteger implements IExplainableConstraint
• Explain returns only the bounds of the Hall witness variables, not all variables
• Explanation is sound: for every bound change, the emitted BoundReason literals logically entail the bound change under the AllDifferent semantics
• N-Queens N=8 with ClauseLearningEnabled = true returns 92 solutions (no unsound clauses)
• Unit tests covering: explanation on propagation, explanation correctness (Hall set bounds), explanation for different variable/bound combinations

Notes

A conservative fallback (all variable bounds) is acceptable as an interim step if the precise Hall witness computation is deferred. The precise implementation requires additional bookkeeping in BipartiteGraph / CycleDetection during the matching and SCC phases. Even a conservative implementation is a significant improvement over the current state, where AllDifferent's lack of IExplainableConstraint forces the DomainHasHoles workaround to abort all clause learning for conflicts involving domain holes.