Fix #1103: ThreeDimensionalMatching to ExactCoverBy3Sets

[isPANN]

Summary

Add the direct witness-preserving reduction from ThreeDimensionalMatching to ExactCoverBy3Sets using a tagged disjoint-union universe.

This PR is stacked on 1075-growth-domain at commit a9067297.

Fixes #1103

[isPANN]

Implementation Summary

Changes

• Added a direct witness-preserving ThreeDimensionalMatching -> ExactCoverBy3Sets reduction using three tagged coordinate blocks, identity solution extraction, and exact overhead metadata.
• Registered the primitive edge and its canonical five-triple example.
• Added eight semantic tests covering closed-loop behavior, target construction and overhead, infeasibility, the empty universe, duplicate triples, unused coordinates, equal numeric coordinates across domains, and identity extraction.
• Added the mandatory paper theorem and fixture-derived tutorial with the corrected explanation of the mutually disjoint cross triples.
• Updated the dominated-rule semantic allowlist because the new path through ExactCoverBy3Sets now dominates the direct ThreeDimensionalMatching -> ILP<bool> route.

Deviations from Plan

• The full test suite revealed the directly caused dominated-rule allowlist change above; this minimal update was added so topology analysis reflects the new graph.
• Canonical example registration follows the repository's current per-rule canonical_rule_example_specs() pattern rather than the older centralized-builder wording.

Open Questions

• None.

Verification

• Mathematical constructor: 109,314 checks passed.
• Independent adversary: 37,507 checks passed; 128 cross-comparison cases, zero disagreements.
• Eight focused reduction tests passed; example-db discovery, graph export, paper build, formatting, clippy, and coverage passed.
• Full test coverage run passed after updating the directly affected topology expectation.

[isPANN]

Agentic Review Report

Structural Check

Structural Review: rule threedimensionalmatching_exactcoverby3sets

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/threedimensionalmatching_exactcoverby3sets.rs exists.
2	#[reduction(...)] macro present	PASS — exact overhead metadata is declared at src/rules/threedimensionalmatching_exactcoverby3sets.rs:30.
3	ReductionResult impl present	PASS — implemented at src/rules/threedimensionalmatching_exactcoverby3sets.rs:17.
4	ReduceTo impl present	PASS — ThreeDimensionalMatching -> ExactCoverBy3Sets is implemented at src/rules/threedimensionalmatching_exactcoverby3sets.rs:35.
5	Test link present	PASS — linked at src/rules/threedimensionalmatching_exactcoverby3sets.rs:73.
6	Test file exists	PASS — src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs exists.
7	Closed-loop test present	PASS — present at src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:7.
8	Registered in rules/mod.rs	PASS — module registration at src/rules/mod.rs:150.
9	Canonical rule example registered	PASS — fixture at src/rules/threedimensionalmatching_exactcoverby3sets.rs:52, aggregated at src/rules/mod.rs:526.
10	Example-db lookup coverage exists	PASS — repository-wide consistency tests passed.
11	Paper reduction-rule entry	PASS — authored at docs/paper/reductions.typ:19170.
12	Blacklisted generated files absent	PASS — the target-branch diff changes only five intended source/test/paper files.

Build Status

• make test: PASS — 5,439 library tests, 75 integration tests, 330 CLI tests, 17 pred-sym tests, 26 macro tests, and 153 doc tests; zero failures.
• make clippy: PASS — all targets with ilp-highs and -D warnings.

Semantic Review

• Reduction construction: OK — (w,x,y) maps to [w, q+x, 2q+y], placing coordinates in three disjoint blocks.
• Correctness: OK — perfect coordinate matching is equivalent in both directions to exact coverage of all three tagged blocks.
• Solution extraction: OK — list order and variable count are preserved, so identity extraction is correct.
• Exact overhead: OK — universe size is exactly 3q; num_subsets and alias num_sets both equal num_triples.
• Example and paper quality: OK — canonical source/target witnesses, corrected cross-pair explanation, both proof directions, and extraction are present.
• Validation completeness: ISSUE — issue [Rule] ThreeDimensionalMatching to ExactCoverBy3Sets #1103 explicitly requests exhausting every q=2 triple family and comparing witness configurations exactly. The committed tests contain fixed q=2/q=3 cases but no exhaustive family/witness-equivalence test (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:7).

Issue Compliance

#	Check	Status
1	Source/target	OK
2	Reduction algorithm	OK
3	Solution extraction	OK
4	Correctness/validation	ISSUE — mathematical implementation is sound, but the issue-mandated exhaustive q=2 test is absent.
5	Overhead expressions	OK
6	Worked example	OK

Summary

• 12/12 structural checks passed.
• 5/6 issue-compliance checks passed.
• Finding: add the requested exhaustive q=2 source/target witness-equivalence test.

---

Quality Check

Quality Review

Design Principles

• DRY: ISSUE — the closed-loop test manually reproduces part of the repository’s satisfaction round-trip pattern instead of using assert_satisfaction_round_trip_from_satisfaction_target, and omits the helper’s independent source solve (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:7).
• KISS: OK — the reduction is a direct coordinate-tagging transformation with identity extraction and no unnecessary abstraction.
• HC/LC: OK — reduction construction, registration, canonical example, tests, and paper documentation remain appropriately separated.

HCI

• Not applicable — the actual stacked diff contains no CLI or MCP files.

Test Quality

• Naive test detection: ISSUE
  • The test named closed_loop brute-forces only the target and evaluates extracted witnesses directly; it does not independently brute-force the source as the shared round-trip helper does (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:7).
  • The duplicate-triple test asserts exact find_all_witnesses enumeration order instead of comparing an unordered set (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:84).
  • Adversarial coverage is otherwise strong: infeasible input, empty universe, duplicates, unused coordinates, cross-domain numeric collisions, tagging, overhead, and identity extraction are covered.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• Replace the partial manual positive closed-loop logic with assert_satisfaction_round_trip_from_satisfaction_target, or explicitly solve both source and target before validating extraction (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:7).

Minor (Nice to Have)

• Compare duplicate-triple witnesses as an unordered set rather than depending on brute-force traversal order (src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs:84).

Summary

• Important — positive closed-loop coverage does not independently solve the source and duplicates part of the shared helper.
• Minor — duplicate-witness coverage is unnecessarily order-sensitive.

---

Agentic Feature Tests

Verdict: pass
Critical issues: 0
Feature: ThreeDimensionalMatching -> ExactCoverBy3Sets
Use case: Discover the rule through documentation and CLI, create and solve the canonical 3DM example, reduce it to X3C, solve the bundle, extract the source witness, and verify it.

Area	Result
Discoverability	PASS
CLI setup/build	PASS
Source example creation	PASS
Source solving	PASS
Reduction bundle creation	PASS
Target solving	PASS
Witness extraction	PASS
Source witness evaluation	PASS
Expected outcome	MET

Commands Exercised

• cargo build -p problemreductions-cli --bin pred --locked
• pred list
• pred show ThreeDimensionalMatching
• pred show ExactCoverBy3Sets
• pred create --example ThreeDimensionalMatching
• pred solve source.json --solver brute-force --json
• pred reduce source.json --to ExactCoverBy3Sets
• pred inspect bundle.json
• pred solve bundle.json --solver brute-force --json
• pred extract bundle.json --config 1,1,1,0,0 --json
• pred evaluate source.json --config 1,1,1,0,0 --json
• Canonical rule-source and rule-target creation via --to ExactCoverBy3Sets and --example-side target.

Result

All commands exited successfully. The canonical source witness [1,1,1,0,0] evaluated to Or(true), the target had universe size 9 with each (w,x,y) mapped to {w,3+x,6+y}, bundle solving returned the identical source witness, and explicit extraction/evaluation succeeded. The generated source and target sides of the canonical rule example were semantically identical after canonical JSON sorting.

Findings

None confirmed. The worktree remained clean. A feature-specific CLI transcript could improve discoverability, but the existing general documentation plus pred list/pred show was sufficient for the complete workflow.

---

Generated by review-pipeline