[Bug] extract_solution produces invalid source config for ThreePartition → SequencingToMinimizeWeightedTardiness

[zazabap]

Summary

The ILP solver finds a valid target solution for SequencingToMinimizeWeightedTardiness (Or(true)), but extract_solution decodes the Lehmer code back to an invalid source config.

Reproduction

pred create --example ThreePartition -o tp.json
pred reduce tp.json --to SequencingToMinimizeWeightedTardiness -o bundle.json
pred solve bundle.json

Result: Target evaluates to Or(true), but extracted source config [1,0,0,1,1,1] evaluates to Or(false).

The correct source config [0,0,0,1,1,1] evaluates to Or(true) — the Lehmer code decoding is producing wrong group assignments.

Origin

Reduction implemented in PR #972.

[zazabap]

Fix should include: Add assert_bf_vs_ilp (from src/rules/test_helpers.rs) to this reduction's closed-loop test. The helper already exists and is used by 56 other tests — this reduction just wasn't wired up to it. The current test only verifies extraction with brute-force witnesses, which happen to work. ILP finds structurally different valid witnesses that break extraction.

[zazabap]

Superseded by #1006. Root cause is unsound reduce_to() constructions, not extract_solution bugs.