Return infeasibility when solving witness-preserving reduction bundles

[isPANN]

Background

A reduction bundle stores a source problem, its already-constructed target problem, and the witness-preserving extraction path between them. A decision problem can be infeasible, in which case a correct solver result has an aggregate value such as Or(false) and no witness configuration.

The bundle solver currently treats every missing target configuration as a capability failure. Consequently, an infeasible target that supports witnesses is reported as “only supports aggregate-value solving” instead of returning the source problem's infeasible result. This was independently reproduced in the agentic review reports for PR #1106 and PR #1110, against the solver changes in PR #1083.

Objective

Make bundle solving distinguish infeasibility from missing witness capability. For a witness-preserving reduction whose target solves to an infeasible aggregate value, return the corresponding source aggregate value successfully without attempting witness extraction or emitting a capability error.

Interface (Input → Output)

In: a ReductionBundle whose target problem is witness-capable but infeasible, passed to pred solve with any supported deterministic solver.

Out: exit status 0, the source-side infeasible evaluation such as Or(false), and no source witness. Actual capability failures must remain errors.

Technical recommendations

The current failure occurs in problemreductions-cli/src/commands/solve.rs, where target_result.config == None unconditionally enters the witness-capability error path. Determine infeasibility from the solved aggregate value before requiring a target configuration. Do not invoke extract_solution when no witness exists.

Verification

Build the CLI and create a hand-checkable infeasible NAE-SAT instance. The repeated clause (x1, x1) is never NAE-satisfied, and its SAT reduction is also unsatisfiable:

cargo build -p problemreductions-cli --bin pred --locked
PRED_BIN=target/debug/pred

"$PRED_BIN" create NAESatisfiability --num-vars 1 --clauses '1,1' -o /tmp/nae-infeasible.json
"$PRED_BIN" reduce /tmp/nae-infeasible.json --to Satisfiability -o /tmp/nae-infeasible-bundle.json
"$PRED_BIN" solve /tmp/nae-infeasible-bundle.json --solver brute-force --json \
  | jq -e '.evaluation == "Or(false)" and (.solution == null)'

The final command must exit 0. This proves that a negative instance is returned as infeasible rather than being misclassified as a capability error.

Negative control: use the satisfiable clause (x1, x2). Bundle solving must still extract a real source witness and report Or(true):

"$PRED_BIN" create NAESatisfiability --num-vars 2 --clauses '1,2' -o /tmp/nae-feasible.json
"$PRED_BIN" reduce /tmp/nae-feasible.json --to Satisfiability -o /tmp/nae-feasible-bundle.json
"$PRED_BIN" solve /tmp/nae-feasible-bundle.json --solver brute-force --json \
  | jq -e '.evaluation == "Or(true)" and (.solution | type == "array")'

Also add focused CLI regression coverage for both cases and run make check.

Out of scope

• Changing solver selection or reduction-path discovery.
• Synthesizing a witness for an infeasible problem.
• Falling back to another solver after a genuine capability or execution failure.

[isPANN]

Fix in #1083 .