[Rule] 3-Dimensional Matching to MinimumWeightDecoding

[isPANN]

Source: 3-Dimensional Matching (ThreeDimensionalMatching)
Target: Minimum Weight Decoding (MinimumWeightDecoding)

Motivation: Establishes NP-hardness of the minimum-weight codeword problem (a.k.a. nearest-codeword / minimum-distance decoding) by encoding a 3-dimensional matching instance as a binary parity-check system over GF(2). Each matching triple becomes a length-3q column with exactly three 1s; the all-ones syndrome forces every element of X ∪ Y ∪ Z to be covered an odd number of times, and the optimal codeword has weight q iff a perfect 3DM matching exists. This is the classical Berlekamp–McEliece–van Tilborg (1978) construction.
Reference: Garey & Johnson, Computers and Intractability, A1.2 MS7; Berlekamp, McEliece, van Tilborg 1978

GJ Source Entry

[MS7] DECODING OF LINEAR CODES
INSTANCE: n×m binary matrix A, binary m-vector ȳ, positive integer K ≤ m.
QUESTION: Is there a binary m-vector x̄ having at most K ones and satisfying Ax̄ = ȳ over GF(2)?
Reference: [Berlekamp, McEliece, and van Tilborg, 1978]. Transformation from 3-DIMENSIONAL MATCHING.
Comment: The problem of computing the minimum Hamming distance of a linear code is a special case.

Reduction Algorithm

Reduction direction and semantics. This is a witness reduction from ThreeDimensionalMatching (whose Value is Or) to MinimumWeightDecoding (whose Value is Min<usize>). The bridge from the source feasibility answer to the target objective value, on the main branch, is

source.evaluate(matching) == Or(true) ⇔ target.evaluate(codeword) == Min(Some(q))

where q = universe_size is the perfect-matching size. A target witness x ∈ {0,1}^{m} decodes back to the column subset S = { t_j ∈ T : x_j = 1 }, and the recovered source answer is source.evaluate(S).

Inputs. A ThreeDimensionalMatching instance with

• universe_size = q, representing three disjoint sets X = Y = Z = {0, 1, ..., q-1},
• triples = T = [t_0, ..., t_{m-1}] with t_j = (a_j, b_j, c_j) ∈ X × Y × Z.

Construction.

1. Sentinel branch (degenerate inputs: T = [] or q = 0). The source model legally accepts triples = [] for any universe_size, and universe_size = 0 with triples = []. But MinimumWeightDecoding::new panics on matrices with zero rows or zero columns (assert!(!matrix.is_empty(), ...) and assert!(num_cols > 0, ...) in src/models/algebraic/minimum_weight_decoding.rs). To keep the reduction total, the algorithm emits a fixed sentinel MinimumWeightDecoding instance whenever T = [] or q = 0:

   matrix       = [[true]]           // 1×1 matrix with a single 1
   target       = [false]            // syndrome 0 of length 1
   

   The unique feasible codeword for this sentinel is x = (0) with Hamming weight 0 (minimum weight 0). The witness-extraction routine then decodes x back to the empty column subset S = ∅ and consults source.evaluate(S) for the recovered source answer. Because the source's evaluate on the empty subset correctly returns

   • Or(true) if q = 0 (the empty matching is a perfect matching of the empty universe), and
   • Or(false) if q ≥ 1 (the empty set of triples cannot cover a non-empty universe),

   the sentinel correctly preserves the source answer through the reduction without any special-case bookkeeping on the bridge side. We use a syndrome of 0 (not 1) precisely so that the unique min-weight codeword has weight 0 and decodes to S = ∅, which is the right object to hand back to source.evaluate.

   Note that the bridge min weight(x) == q does not hold on the sentinel branch in general (e.g., q = 1 with T = [] gives min weight = 0 ≠ 1 but source is correctly Or(false)). The witness-extraction path via source.evaluate(S) is what guarantees correctness on this branch.

2. Main branch (q ≥ 1 and |T| ≥ 1). Build the parity-check matrix H ∈ {0,1}^{3q × m} whose row blocks correspond to X, Y, Z in that order:

   • Row a (for a ∈ X) has H[a, j] = 1 iff the first coordinate of t_j equals a.
   • Row q + b (for b ∈ Y) has H[q + b, j] = 1 iff the second coordinate of t_j equals b.
   • Row 2q + c (for c ∈ Z) has H[2q + c, j] = 1 iff the third coordinate of t_j equals c.

   Each column therefore has exactly three 1s. Set the syndrome (target) to the all-ones vector s = 1^{3q}. The target instance is MinimumWeightDecoding(matrix = H, target = s).

Correctness (main branch).

• Forward. If S ⊆ T is a perfect 3D matching (|S| = q, every element of X ∪ Y ∪ Z covered exactly once), the indicator vector x ∈ {0,1}^{m} with x_j = 1 ⇔ t_j ∈ S has weight q and satisfies Hx ≡ 1^{3q} (mod 2) because each row contains exactly one 1 among the selected columns. Hence the minimum codeword weight is ≤ q.
• Reverse. For any x with Hx ≡ 1^{3q} (mod 2), each row sum is odd, so each row uses at least one selected column, giving total column-coverage ≥ 3q. Each column contributes coverage exactly 3, so 3 · weight(x) ≥ 3q, i.e. weight(x) ≥ q. Equality forces every row to be covered exactly once (any row covered ≥ 3 times would push the total over 3q), which is precisely a perfect 3DM matching on the supports of x.

Combining the two directions: min weight(x) = q iff a perfect matching exists, otherwise min weight(x) > q (or the target is infeasible and returns Min(None)).

Witness extraction (both branches).

Given a target witness x ∈ {0,1}^{|columns|} returned by the MinimumWeightDecoding solver:

1. Compute S = { t_j ∈ T : x_j = 1 }. On the sentinel branch x = (0) and S = ∅; on the main branch S is the subset of triples whose corresponding columns were selected.
2. Call source.evaluate(S) and return its result as the recovered source answer.
3. The bridge min weight(x) = q ⇔ source.evaluate(S) = Or(true) is what guarantees that on the main branch this S is a valid perfect matching iff the target's optimum equals q; if min weight(x) > q or the target returned Min(None), the same source.evaluate(S) will return Or(false) (the extracted S cannot be a perfect matching).

source.evaluate(S) therefore doubles as the bridge's defensive verifier: it catches any case where the target solver returns a feasible but non-optimal x whose support does not cover the universe correctly.

Time complexity of reduction: O(q · m) to construct the matrix on the main branch; O(1) for the sentinel branch. Witness extraction is O(m).

Size Overhead

Symbols:

• universe_size = q = size of each partition set in the 3DM instance (|X| = |Y| = |Z| = q)
• num_triples = m = |T| = number of triples

MinimumWeightDecoding exposes size_fields = [num_cols, num_rows] (see pred show MinimumWeightDecoding --json). The overhead table lists those two fields only — there is no K / weight_bound field on the target. The weight constraint weight(x) = q is not part of the target instance; it is verified implicitly via source.evaluate(S) in witness extraction.

Target metric (code name)	Polynomial (using symbols above)
num_rows	3 * universe_size
num_cols	num_triples

Derivation: On the main branch each element of X ∪ Y ∪ Z becomes a row (3q rows total) and each triple becomes a column (m columns); the matrix is sparse with 3 ones per column. The syndrome is 1^{3q}. On the sentinel branch the target is a fixed 1×1 instance, well within these polynomial bounds.

Validation Method

• Closed-loop test (main branch). Build a 3DM instance with q ≥ 1 and |T| ≥ 1, run the reduction, solve the target by brute-force enumeration of all 2^m binary vectors against the syndrome, apply the witness-extraction recipe (S = supp(x); source.evaluate(S)), and assert that the round-trip recovered answer matches source.evaluate(<original perfect-matching witness>) for YES instances and Or(false) for NO instances.
• Sentinel-branch tests. Cover all degenerate combinations:
  • q = 0, T = [] → sentinel target solves to x = (0), extracted S = ∅, source.evaluate(∅) == Or(true) (empty matching of empty universe).
  • q = 1, T = [] → sentinel target solves to x = (0), extracted S = ∅, source.evaluate(∅) == Or(false) (universe non-empty, no triples).
  • q = 2, T = [] → same as above, Or(false).
• YES instance (main branch). q = 2, T = [(0,0,0), (1,1,1), (0,1,0), (1,0,1)] — both {t_0, t_1} and {t_2, t_3} are perfect matchings; target's optimum should be Min(Some(2)).
• NO instance (main branch). q = 2, T = [(0,0,0), (0,0,1), (1,0,0)] — element 1 ∈ Y is never covered, so the target is infeasible (Min(None)); witness extraction with any feasible attempt returns Or(false).
• GF(2) arithmetic check. For any candidate x over the constructed H, verify Hx ≡ 1^{3q} (mod 2) row by row.

Example

Source instance (3-Dimensional Matching):
q = universe_size = 2, so X = Y = Z = {0, 1}.
T = [t_0 = (0,0,0), t_1 = (1,1,1), t_2 = (0,1,0), t_3 = (1,0,1)].
Perfect matchings: {t_0, t_1} and {t_2, t_3} (each covers every element of X ∪ Y ∪ Z exactly once).

Constructed target instance (MinimumWeightDecoding, main branch):
H ∈ {0,1}^{6 × 4}, with row blocks X (rows 0–1), Y (rows 2–3), Z (rows 4–5):

       t0 t1 t2 t3
X=0:    1  0  1  0
X=1:    0  1  0  1
Y=0:    1  0  0  1
Y=1:    0  1  1  0
Z=0:    1  0  1  0
Z=1:    0  1  0  1

Syndrome (target) = (1, 1, 1, 1, 1, 1). There is no separate K field on the target; the weight q constraint is enforced implicitly by the witness-extraction step calling source.evaluate.

Brute-force solution. Enumerating all 2^4 = 16 binary vectors x and keeping those with Hx ≡ 1^6 (mod 2):

• x = (1, 1, 0, 0) → weight 2 → extracted S = {t_0, t_1}, source.evaluate(S) = Or(true) ✓
• x = (0, 0, 1, 1) → weight 2 → extracted S = {t_2, t_3}, source.evaluate(S) = Or(true) ✓

Both attain the minimum weight 2 = q, confirming min weight(x) = q ⇔ 3DM has a perfect matching. The reduction returns Or(true) with either S as a valid recovered matching.

Sentinel example. For q = 1, T = [], the sentinel target is MinimumWeightDecoding(matrix = [[1]], target = [0]). The unique feasible codeword is x = (0) with weight 0; the extracted subset is S = ∅; and source.evaluate(∅) with q = 1 returns Or(false) (the empty set of triples does not cover element 0). For q = 0, T = [], the same sentinel target gives the same x = (0) and S = ∅, but source.evaluate(∅) with q = 0 returns Or(true).

References

• [Berlekamp, McEliece, and van Tilborg, 1978]: E. R. Berlekamp, R. J. McEliece, and H. C. A. van Tilborg (1978). "On the inherent intractability of certain coding problems." IEEE Transactions on Information Theory IT-24(3), pp. 384–386.
• [Garey and Johnson, 1979]: M. R. Garey and D. S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, p. 226 (MS7).

[isPANN]

Issue Quality Check — Rule (Re-check, --force)

Check	Result	Details
Usefulness	Pass	No existing reduction path ThreeDimensionalMatching → MinimumWeightDecoding; novel edge.
Non-trivial	Pass	Genuine structural construction: each triple becomes a length-3q binary column with three 1s; all-ones syndrome forces a parity cover.
Correctness	Pass	Berlekamp–McEliece–van Tilborg (1978) verified to exist and to contain this reduction from 3-DM; G&J MS7 entry matches. The worked example was reproduced numerically (min weight = q = 2, x = (0,0,1,1) selecting {t3, t4}, which is one of two perfect matchings).
Completeness	Fail	The algorithm breaks on legitimate ThreeDimensionalMatching corner cases (zero columns / zero rows), and the issue silently relies on a K = q weight bound that does not exist on the codebase target.
Well-written	Warn	The Size Overhead table lists weight_bound, which is not a field of MinimumWeightDecoding; the target/decision-vs-optimization mismatch is not addressed.

Overall: 3 passed, 1 failed (Completeness), 1 warning (Well-written)

---

Usefulness

pred path ThreeDimensionalMatching MinimumWeightDecoding reports no existing path:

$ pred path ThreeDimensionalMatching MinimumWeightDecoding
Error: No reduction path from ThreeDimensionalMatching to MinimumWeightDecoding

Currently MinimumWeightDecoding has no reduces_from edges (only an outgoing edge to ILP<i32>), so this rule both populates the in-neighborhood of the decoding model and provides an independent NP-hardness witness inside the library.

Non-trivial

The construction is not a relabeling. It builds a fresh binary matrix A ∈ {0,1}^{3q × |M|} whose columns are characteristic vectors of triples and forces the syndrome equation Ax ≡ 1 (mod 2) to encode the matching constraints. Solution extraction reads the support of x back as the selected triples. This is a textbook gadget reduction, not a subtype coercion or identity rule.

Correctness

• References verified. Berlekamp, McEliece, and van Tilborg, On the inherent intractability of certain coding problems, IEEE TIT 24(3), 1978, exists (Caltech / Eindhoven hosts the original, Semantic Scholar has the bibliographic record) and is the standard citation for this reduction. The G&J MS7 entry quoted in the issue matches the reference book (1979 edition).
• Worked example reproduced. Reconstructing the 6×4 matrix from M = {(w1,x1,y1), (w2,x2,y2), (w1,x2,y1), (w2,x1,y2)} and brute-forcing all 16 binary x yields minimum-weight feasible solutions of weight 2 — both (1,1,0,0) (the issue's choice, {t1,t2}) and (0,0,1,1) ({t3,t4}) satisfy Ax = 1^6. Both correspond to the two perfect 3-DM solutions.
• Aggregate semantics consistent. Over GF(2), each column contributes weight 3 to the row-sum total, and the all-ones syndrome demands 3q odd row-coverages; hence min weight(x) = q ⇔ 3-DM has a perfect matching. So as an Or → Min aggregate reduction this is correct.

Completeness (the failing check)

Literature read

G&J MS7 and Berlekamp–McEliece–van Tilborg 1978 state the reduction for the decision variant of decoding (|x| ≤ K, with K = q). The codebase target MinimumWeightDecoding is the optimization variant (minimize |x| subject to Hx = s), with size fields num_cols, num_rows only — there is no K/weight_bound field (pred show MinimumWeightDecoding --json → size_fields: [num_cols, num_rows]). The issue does not flag this gap and lists weight_bound = q in the Size Overhead, which has no target counterpart. The reduction can still be salvaged as an aggregate Or → Min rule (min weight = q iff matching exists), but the issue does not say so and does not specify how K = q is enforced in the target.

Codebase corner cases I traced by hand

ThreeDimensionalMatching::new(universe_size, triples) accepts:

• empty triples list (triples = []) for any universe_size, and
• universe_size = 0 with triples = [].

MinimumWeightDecoding::new(matrix, target) panics if the matrix has zero rows or zero columns (see src/models/algebraic/minimum_weight_decoding.rs lines 72–82: assert!(!matrix.is_empty(), ...), assert!(num_cols > 0, ...)).

#	3-DM input	Issue's construction	Outcome
1	universe_size = 0, triples = [] (trivially has the empty matching)	0×0 matrix, syndrome (), K = 0	MinimumWeightDecoding::new panics ("Matrix must have at least one row" / "at least one column"). Algorithm fails.
2	universe_size = 1, triples = [] (no perfect matching exists; correct source answer is NO)	3×0 matrix (3 rows, 0 columns), syndrome (1,1,1), K = 1	Panics on "Matrix must have at least one column". Algorithm fails. Equivalent failure for any q ≥ 1 with `
3	universe_size = 1, triples = [(0,0,0)] (trivial matching)	3×1 matrix of all-ones, syndrome (1,1,1), K = 1	OK — x = (1) is the unique min-weight solution; extraction recovers {(0,0,0)}.
4	universe_size = 2, triples = [(0,0,0), (0,1,1)] (no perfect matching: w-element 0 used twice would be the only way)	6×2 matrix; brute force shows no x satisfies Ax = 1^6	Target is infeasible (no x with Ax = s at all), so MinimumWeightDecoding returns Min(None). Issue's extraction step is silent on this case; it just says "positions of 1s in x form the matching", with no guidance for Min(None) or weight > q.

Corner cases (1) and (2) break the algorithm before the target instance is even constructed. They are not exotic — they are inputs that the source model legally accepts and that have well-defined 3-DM answers.

What the fix needs

At minimum the issue needs to (a) restrict the source to triples non-empty (or specify how to construct a valid MinimumWeightDecoding instance when |M| = 0), (b) replace weight_bound in the Size Overhead with the actual num_rows/num_cols fields of the target, (c) explicitly frame this as an aggregate (Or → Min) reduction with the bound check min weight == q performed at extraction time, and (d) describe what to do when the target is infeasible (Min(None)) or has min-weight > q (extraction must report "no matching").

Well-written (warnings)

• Mismatched target schema. Size Overhead lists weight_bound = q, but MinimumWeightDecoding has no such field (pred show MinimumWeightDecoding --json → size_fields: [num_cols, num_rows]). The overhead table should declare num_rows = 3 * universe_size and num_cols = num_triples only.
• Decision vs optimization. The issue body mixes "weight bound K" language from G&J MS7 with the optimization target in this codebase, without explaining the bridge (min weight(x) = q ⇔ matching exists).
• Otherwise readable. Sections, symbols, and the worked example are otherwise consistent (q, m, row/column conventions match the matrix).

Recommendations

• Reframe explicitly as an aggregate Or → Min reduction and add the weight == q check to solution extraction.
• Document the triples non-empty precondition (or add a small preprocessing escape hatch for trivial 3-DM instances).
• After the algorithm is patched, the example is already strong enough for a round-trip test: it has two distinct optimal solutions of weight 2 and several non-optimal feasible/infeasible x values, so it is not a "trivially correct" instance.

Labels

Adding Incomplete. Other failure labels (Useless, Trivial, Wrong, PoorWritten) are not warranted.

[isPANN]

auto-pipeline: parked on OnHold — substantive completeness/type-mismatch. Algorithm panics on legitimate corner cases the source model accepts (q=0 with empty triples → 0×0 matrix rejected by MinimumWeightDecoding::new; any input with empty triples → matrix with zero columns also rejected). Decision-vs-optimization mismatch: G&J MS7 uses bound K=q but the codebase target is the optimization (Min) variant with no K field; the Or-to-Min bridge is not specified. See #916 (comment)

[isPANN]

Issue Quality Check — Rule (Re-check, --force)

Check	Result	Details
Usefulness	Pass	No existing reduction path ThreeDimensionalMatching → MinimumWeightDecoding; novel edge into a decoding target with currently no reduces_from neighbors.
Non-trivial	Pass	Genuine gadget: each triple becomes a length-3q binary column with three 1s; the all-ones syndrome forces a parity cover. Not a relabeling.
Correctness	Pass	Berlekamp–McEliece–van Tilborg, On the inherent intractability of certain coding problems, IEEE TIT 24(3), 1978, is the standard citation for this construction; G&J MS7 quote matches the 1979 edition. The worked example reproduces numerically: brute-forcing all 2^4 = 16 binary x against the 6×4 matrix yields min weight 2 = q, attained by both (1,1,0,0) ↔ {t1,t2} and (0,0,1,1) ↔ {t3,t4} — exactly the two perfect 3-DM matchings.
Completeness	Fail	Algorithm panics on legitimate ThreeDimensionalMatching corner cases (universe_size = 0 and/or triples = []) the source model legally accepts, and the issue silently relies on a K = q weight bound that does not exist on the codebase target. (Previously labeled Incomplete; root causes unchanged in current issue body.)
Well-written	Warn	The Size Overhead table lists weight_bound, which is not a field of MinimumWeightDecoding (size_fields = [num_cols, num_rows]). The decision-vs-optimization mismatch is not addressed.

Overall: 3 passed, 1 failed (Completeness), 1 warning (Well-written)

Compared to the previous Issue Quality Check comment on 2026-05-27: no change. The issue body has not been edited and the underlying constructor panics on the same corner cases. Existing label Incomplete remains correct.

---

Usefulness

$ pred path ThreeDimensionalMatching MinimumWeightDecoding
Error: No reduction path from ThreeDimensionalMatching to MinimumWeightDecoding

pred show MinimumWeightDecoding --json shows reduces_from: [] (only reduces_to: [ILP<i32>]). This rule populates the in-neighborhood of the decoding model and adds an NP-hardness witness inside the library. Pass.

Non-trivial

The construction builds a fresh binary matrix A ∈ {0,1}^{3q × |M|} whose columns are characteristic vectors of triples, and forces the syndrome equation Ax ≡ 1 (mod 2) to encode 3-DM constraints. Solution extraction reads the support of x back as the selected triples. Textbook gadget, not subtype coercion or identity. Pass.

Correctness

• References verified. Berlekamp, McEliece, van Tilborg (1978) is a well-established source for the NP-hardness of nearest-codeword / minimum-weight-codeword decoding via 3-DM. G&J entry [MS7] (p. 226 of the 1979 edition) attributes the result to that paper. Both citations are consistent.
• Worked example reproduces. Reconstructing the 6×4 matrix A from M = {(w1,x1,y1), (w2,x2,y2), (w1,x2,y1), (w2,x1,y2)} and brute-forcing all 16 binary vectors x yields:
  • Minimum feasible weight = 2 = q.
  • Two optimal vectors: (1,1,0,0) selecting {t1,t2} and (0,0,1,1) selecting {t3,t4} — exactly the two perfect 3-DM matchings.
• Aggregate semantics consistent. Over GF(2), each column contributes weight 3 to the total row-sum, and the all-ones syndrome requires 3q odd row-coverages; hence min weight(x) = q ⇔ 3-DM has a perfect matching. As an Or → Min aggregate reduction this is mathematically correct.

Completeness (the failing check)

Literature read

G&J MS7 and Berlekamp–McEliece–van Tilborg 1978 state the reduction for the decision variant of decoding (|x| ≤ K, with K = q). The codebase target MinimumWeightDecoding is the optimization variant (minimize |x| subject to Hx = s); pred show MinimumWeightDecoding --json gives size_fields: [num_cols, num_rows] — no K / weight_bound field exists. The issue does not flag this gap and lists weight_bound = q in the Size Overhead with no target counterpart. The reduction can be salvaged as an aggregate Or → Min rule (min weight = q iff matching exists), but the issue does not say so and does not specify how K = q is enforced in the target.

Codebase corner cases traced by hand

ThreeDimensionalMatching::new(universe_size, triples) accepts triples = [] for any universe_size, and accepts universe_size = 0 with triples = [].

MinimumWeightDecoding::new(matrix, target) panics if the matrix has zero rows or zero columns (verified in src/models/algebraic/minimum_weight_decoding.rs lines 71–83: assert!(!matrix.is_empty(), "Matrix must have at least one row"), assert!(num_cols > 0, "Matrix must have at least one column")).

#	3-DM input	Issue's construction	Outcome
1	universe_size = 0, triples = [] (trivially has the empty matching)	0×0 matrix, syndrome (), K = 0	MinimumWeightDecoding::new panics on "Matrix must have at least one row". Algorithm fails.
2	universe_size = 1, triples = [] (no perfect matching; correct answer is NO)	3×0 matrix (3 rows, 0 columns), syndrome (1,1,1), K = 1	Panics on "Matrix must have at least one column". Algorithm fails. Same failure for any q ≥ 1 with `
3	universe_size = 1, triples = [(0,0,0)] (trivial matching)	3×1 matrix of all-ones, syndrome (1,1,1), K = 1	OK — x = (1) is the unique min-weight solution; extraction recovers {(0,0,0)}.
4	universe_size = 2, triples = [(0,0,0), (0,1,1)] (no perfect matching)	6×2 matrix; brute force shows no x with Ax = 1^6	Target infeasible (Min(None)). Issue's extraction step says only "positions of 1s in x form the matching" — no guidance for the Min(None) or weight > q cases.

Corner cases (1) and (2) break the construction before the target instance is even built. These are legal inputs to the source model with well-defined 3-DM answers.

What the fix needs

At minimum: (a) restrict the source to non-empty triples (or specify how to construct a valid MinimumWeightDecoding instance when |M| = 0), (b) replace weight_bound in the Size Overhead with the actual num_rows/num_cols fields of the target, (c) explicitly frame this as an aggregate (Or → Min) reduction with the bound check min weight == q performed at extraction time, and (d) describe what to do when the target is infeasible (Min(None)) or has min-weight > q (extraction must report "no matching").

Well-written (warnings)

• Mismatched target schema. Size Overhead lists weight_bound = q, but MinimumWeightDecoding has no such field (size_fields = [num_cols, num_rows]). The overhead table should declare num_rows = 3 * universe_size and num_cols = num_triples only.
• Decision vs optimization. The issue mixes "weight bound K" language from G&J MS7 with the optimization target in this codebase, without explaining the bridge (min weight(x) = q ⇔ matching exists).
• Otherwise readable — sections, symbols, and the worked example are internally consistent.

Recommendations

• Reframe explicitly as an aggregate Or → Min reduction; add the weight == q check to solution extraction and document the Min(None) / weight > q cases.
• Document the triples-non-empty / universe_size ≥ 1 precondition (or add a small preprocessing escape hatch for trivial 3-DM instances).
• Once the algorithm is patched, the example is already strong enough for a round-trip test: two distinct optimal solutions of weight 2, plus many non-optimal feasible/infeasible x values.

Labels

Keeping Incomplete. No other failure labels (Useless, Trivial, Wrong, PoorWritten) warranted.

[isPANN]

Revised issue body (rewrite, fix-issue)

Addressed all substantive findings from #issuecomment-4558535308:

1. Sentinel branch added. If T = [] or q = 0, the algorithm now emits a fixed MinimumWeightDecoding(matrix = [[1]], target = [0]) (a 1×1 parity-check with zero syndrome). The unique min-weight codeword is x = (0), which decodes back to the empty triple-subset S = ∅. Calling source.evaluate(∅) returns Or(true) exactly when q = 0 and Or(false) otherwise, so the bridge naturally preserves the source answer on both degenerate inputs (q = 0, T = [] → Or(true); q ≥ 1, T = [] → Or(false)) without panicking in MinimumWeightDecoding::new.
2. Reframed as a witness reduction. The body now explicitly states that the source Value is Or and the target Value is Min<usize>, and that the bridge on the main branch is source.evaluate(matching) == Or(true) ⇔ target.evaluate(codeword) == Min(Some(q)). Witness extraction: decode x to S = { t_j : x_j = 1 }, then return source.evaluate(S) as the recovered source answer. This is uniform across main and sentinel branches.
3. Size Overhead corrected. Dropped the non-existent weight_bound field. The table now lists only the two actual MinimumWeightDecoding size fields:
   • num_rows = 3 * universe_size
   • num_cols = num_triples
4. Decision-vs-optimization bridge stated. The body now explains that the codebase target is the optimization (Min<usize>) variant and that the G&J K = q decision bound is enforced implicitly via the min weight(x) = q check, which is performed by calling source.evaluate(S) on the extracted column subset.
5. Validation Method and Example expanded. Added explicit sentinel-branch tests (q ∈ {0, 1, 2} with T = []), tightened the main-branch closed-loop test description, and added a sentinel example showing both Or(true) (for q = 0) and Or(false) (for q = 1) outcomes.

Other wording (q, m, row/column conventions) was kept consistent with the previously verified worked example. The core algorithm is unchanged; only the corner-case handling, type bridge, and overhead schema were revised.

Ready for a re-check.

[isPANN]

Issue Quality Check — Rule (Re-check, --force)

Check	Result	Details
Usefulness	Pass	Still no existing reduction path ThreeDimensionalMatching → MinimumWeightDecoding; the target's reduces_from is still empty in pred show MinimumWeightDecoding --json.
Non-trivial	Pass	Genuine gadget: each triple becomes a length-3q binary column with three 1s; the all-ones syndrome forces a parity cover. The sentinel branch is a fixed 1×1 instance, not a structural reduction step.
Correctness	Pass	Berlekamp–McEliece–van Tilborg (1978) and G&J MS7 verified to support this construction. The main-branch worked example reproduces numerically (min weight = 2 = q, attained by two optimal x's decoding to the two perfect matchings).
Completeness	Pass	The new sentinel branch + source.evaluate(S) witness-extraction bridge correctly handles all traced corner cases (T = [] for any q; q = 0; q = 1 with single triple; q = 2 with non-trivial matching choice). The aggregate Or → Min semantics are now stated explicitly and the schema-level type mismatch is resolved.
Well-written	Pass	Size Overhead now lists only the actual target size fields (num_rows = 3 * universe_size, num_cols = num_triples); decision-vs-optimization bridge stated; symbols (q, m) consistent across sections.

Overall: 5 passed, 0 failed, 0 warnings

Compared to the previous Issue Quality Check (2026-05-27): the rewritten body resolves both substantive findings (completeness on degenerate inputs + decision-vs-optimization mismatch) and the well-written warning (mismatched target schema). Removing the Incomplete label and adding Good.

---

Usefulness

$ pred path ThreeDimensionalMatching MinimumWeightDecoding
Error: No reduction path from ThreeDimensionalMatching to MinimumWeightDecoding

pred show MinimumWeightDecoding --json still reports reduces_from: [] (only outgoing edge to ILP<i32>). This rule populates the in-neighborhood of the decoding model and adds an NP-hardness witness inside the library. Pass.

Non-trivial

The main branch builds a fresh binary matrix H ∈ {0,1}^{3q × m} whose columns are characteristic vectors of triples, with all-ones syndrome forcing Hx ≡ 1^{3q} (mod 2). Witness extraction reads S = supp(x) and runs source.evaluate(S). Textbook gadget reduction, not a relabeling or subtype coercion. The sentinel branch is bookkeeping (constant-size target for degenerate inputs), not the structural content of the reduction. Pass.

Correctness

• References verified. Berlekamp, McEliece, van Tilborg, On the inherent intractability of certain coding problems, IEEE TIT 24(3), 1978 — standard citation for NP-hardness of minimum-weight-codeword decoding via 3-DM. G&J MS7 (p. 226 of the 1979 edition) attributes the result to the same paper.
• Worked example reproduces. Reconstructing the 6×4 matrix from q = 2, T = [(0,0,0), (1,1,1), (0,1,0), (1,0,1)] and brute-forcing all 16 binary x yields min weight = 2 = q, attained by (1,1,0,0) → {t_0, t_1} and (0,0,1,1) → {t_2, t_3} — exactly the two perfect 3-DM matchings.
• Aggregate semantics consistent. Over GF(2), each column contributes weight 3 to the row-sum total, and the all-ones syndrome demands 3q odd row-coverages. Hence min weight(x) = q ⇔ 3-DM has a perfect matching. Mathematically sound as an Or → Min reduction.

Completeness (the previously failing check, now resolved)

Literature read

G&J MS7 and Berlekamp–McEliece–van Tilborg 1978 state the reduction for the decision variant of decoding (|x| ≤ K, with K = q). The codebase target MinimumWeightDecoding is the optimization variant (minimize |x| subject to Hx = s); the issue now explicitly states the Or → Min bridge — source.evaluate(matching) == Or(true) ⇔ target.evaluate(codeword) == Min(Some(q)) — and uses source.evaluate(S) on the extracted column subset as the defensive verifier on both main and sentinel branches.

Codebase corner-case hand-traces

I re-confirmed the relevant constructor preconditions:

// src/models/algebraic/minimum_weight_decoding.rs L71–82
assert!(!matrix.is_empty(), "Matrix must have at least one row");
assert!(num_cols > 0, "Matrix must have at least one column");

And the source evaluate semantics (src/models/set/three_dimensional_matching.rs L130–164): an empty config with q = 0 gives Or(true); with q ≥ 1 gives Or(false) (selected_count = 0 ≠ q).

Traced corner cases against the new algorithm:

#	3-DM input	Branch	Construction	Outcome
1	q = 0, T = [] (empty matching is the unique perfect matching)	sentinel (T=[] OR q=0)	matrix = [[1]], target = [0]	Unique feasible x = (0), weight 0. Extract S = ∅. source.evaluate([]) with q = 0 → Or(true). Correct.
2	q = 1, T = [] (no perfect matching: universe non-empty)	sentinel (T=[])	matrix = [[1]], target = [0]	Unique feasible x = (0), weight 0. Extract S = ∅. source.evaluate([]) with q = 1 → Or(false) (selected_count 0 ≠ 1). Correct.
3	q = 2, T = [] (no perfect matching)	sentinel (T=[])	matrix = [[1]], target = [0]	Same x = (0), S = ∅, source.evaluate([]) → Or(false). Correct.
4	q = 1, T = [(0,0,0)] (trivial perfect matching)	main	H = [[1],[1],[1]] (3×1 all-ones), syndrome (1,1,1)	Only x = (1) is feasible (x = (0) violates row 0). Weight = 1 = q. Extract S = {(0,0,0)}, source.evaluate([1]) → Or(true). Correct.
5	q = 2, T = [(0,0,0),(1,1,1),(0,1,0),(1,0,1)] (worked example, two distinct optima)	main	6×4 matrix in the body	Brute force: min weight = 2 = q, attained by (1,1,0,0) and (0,0,1,1). Both decode to perfect matchings. Correct.
6	q = 2, T = [(0,0,0),(0,1,1)] (no perfect matching; some Hx = s may still be infeasible)	main	6×2 matrix	Brute force: no x satisfies Hx = 1^6 (column counts can't cover Y={0,1} odd-many times). Target evaluates to Min(None). Witness extraction: any candidate x returned by the solver runs source.evaluate(S); the issue's defensive source.evaluate(S) step naturally returns Or(false) since no S with `

The previously-failing cases (1)–(3) are now routed through the sentinel branch, which never constructs a 0-row or 0-column matrix. The body explicitly acknowledges that the min weight(x) == q bridge does not hold globally on the sentinel branch (e.g., q = 1 with T = [] gives min weight 0 ≠ 1), and that correctness on this branch comes from the source.evaluate(S) witness-extraction step — which is mathematically sound: any S ⊆ T = ∅ must itself be ∅, and source.evaluate(∅) directly answers the 3-DM feasibility question for the (empty) universe.

The aggregate-only nature of the reduction (Value: Or → Min<usize>) is now stated up front, and the K = q decision bound from G&J is enforced implicitly via the source.evaluate(S) verifier at extraction time. The Size Overhead table no longer lists the phantom weight_bound.

Verdict on Check 5

Literature covers all main-branch instances; sentinel branch is a sound polynomial-time gadget for the two degenerate cases the source model accepts; all 6 traced corner cases work correctly. Pass.

Well-written

• Size Overhead schema-correct. Table now lists only num_rows = 3 * universe_size and num_cols = num_triples, matching MinimumWeightDecoding's size_fields = [num_cols, num_rows]. No phantom weight_bound.
• Decision-vs-optimization bridge stated. Body explicitly identifies the source Value as Or, target Value as Min<usize>, and states the bridge source.evaluate(matching) == Or(true) ⇔ target.evaluate(codeword) == Min(Some(q)) for the main branch, with witness extraction via source.evaluate(S).
• Symbol consistency. q = universe_size, m = num_triples, row blocks X, Y, Z of size q each — all internally consistent and consistent with the worked example.
• Algorithm completeness. Both branches (sentinel and main) are spelled out step by step; witness extraction is uniform across branches. Validation Method adds explicit sentinel tests for q ∈ {0, 1, 2} with T = [].

Pass.

Labels

Removing Incomplete (issue rewrite resolved the completeness gap). Adding Good (zero failures, zero warnings on Usefulness/Correctness/Completeness).