Separate witness feasibility and source solve conclusions at shared boundaries

[isPANN]

Problem and root cause

The repository confuses successful configuration evaluation with a feasible witness, and backend completion with a mathematical conclusion about the source problem.

Problem::evaluate() can return Ok(Or(false)), Ok(Min(None)), Ok(Max(None)), or an infeasible Extremum. These are evaluable configurations, not witnesses. Yet validate_target_solution() in src/rules/traits.rs only returns Ok(target.evaluate(solution)?). Approximately 266 extraction sites use this shared boundary.

In src/solvers/resolver.rs, customized and ILP dispatch call evaluate_dyn() and construct SolveOutcome::Optimal. The current two-outcome API cannot express a feasible solution without established source optimality, or a numerical backend conclusion that does not establish source infeasibility.

The fix belongs in shared extraction and solve-result contracts, not individual model guards.

Concrete failure

For MaximumSetPacking<i64> -> ILP<bool> with one set, target configuration [2] evaluates to an infeasible ILP aggregate. The shared validator accepts it, and the extractor decodes 2 == 1 as false. The resulting empty source packing is feasible, so source-only validation cannot detect the invalid target input.

A separate numerical example is documented in #1145: individually representable integer coefficients can produce two distinct source objectives that collapse in floating-point arithmetic. Re-evaluating one feasible returned assignment cannot prove global optimality. See #1146 for consistent exact CVP evaluation and #1143 for search-space representation.

Required refactor

1. Make validate_target_solution() reject infeasible evaluated values using the existing SolutionAggregate::contributes_to_solution(&value, &value) semantics. Propagate the necessary bounds through shared callers. Preserve malformed/evaluation failures separately from infeasible-witness errors.
2. Use existing evaluate_witness_dyn() at the dynamic solve boundary. Validate the final source witness after extraction, before producing a successful outcome. Cover typed public solve entry points as well; fixing only the CLI is insufficient.
3. Replace the two-state outcome contract with:
   • Optimal { solution, evaluation }: source optimality established under the documented exact algorithm contract, with a validated witness.
   • Feasible { solution, evaluation }: source witness validated; exact source optimality not established.
   • Infeasible: source infeasibility established under the exact algorithm contract.
   • Unknown: no established source conclusion.
     Operational/construction/conversion/backend failures remain typed errors.
4. Exact brute-force/customized algorithms retain their established conclusions when their contracts hold. A floating-point ILP backend's successful optimization generally yields Feasible after source validation; a numerical infeasibility report alone yields Unknown, preserving the backend reason in execution diagnostics. A validated satisfying witness is sufficient to settle a decision problem positively.
5. Update CLI, MCP, typed consumers, and decision-search consumers so they cannot turn Feasible into exact optimality or Unknown into false/infeasible. A failed returned-witness validation is an explicit error, never silently discarded.

Extraction accepts feasible non-optimal target witnesses where allowed by the rule's mathematical mapping; validation must not run a second optimization.

Design references

• MathOptInterface solver contract separates TerminationStatus, PrimalStatus, and ResultCount.
• MathOpt HiGHS adapter separates backend termination and feasibility claims.
• HiGHS numerical tolerances explain why backend optimality is not automatically an exact source certificate.

Reuse existing aggregate/witness facilities. Do not add a solver abstraction framework, certificate infrastructure, automatic fallback, or difficulty-based rejection.

Acceptance tests

• The set-packing counterexample fails with an extraction error through direct, dynamic-chain, and CLI extraction.
• A feasible non-optimal witness remains accepted where the reduction permits it.
• Malformed input, infeasible witness, and unresolved solve remain distinguishable.
• No public solve path reports an infeasible returned witness as success.
• The integer objective rounding counterexample is never reported as exact Optimal.
• Backend numerical infeasibility is not consumed as an exact negative decision.
• Small exact solver results retain optimal/infeasible behavior.

Run focused tests and make check, including ILP-feature tests. Keep regression names semantic, without issue numbers.