feat: add 11 medium-confidence reduction rules

[GiggleLiu]

Summary

• Batch implement 11 medium-confidence reduction rules from the reinspected derivation document, using Codex CLI in headless mode
• Each rule includes: ReduceTo impl with #[reduction] overhead, unit tests (closed-loop + edge cases), paper entry in reductions.typ
• 4 rules were rejected as unsound after Codex found concrete counterexamples
• 1 rule was rejected as unimplementable (incomplete construction)

Implemented (11 rules)

Source → Target	Issue	Tests	Reference
MinimumVertexCover → LongestCommonSubsequence	#429	6	Maier 1978
ThreeDimensionalMatching → ThreePartition	#389	6	Garey-Johnson 1975/1979
NAESatisfiability → PartitionIntoPerfectMatchings	#845	7	Creignou SAT-equivalence
SetSplitting → Betweenness	#842	4	Opatrný 1979
KSatisfiability → QuadraticCongruences	#553	3	Manders-Adleman 1978
KSatisfiability → PreemptiveScheduling	#479	4	Ullman 1975
Satisfiability → IntegralFlowWithHomologousArcs	#732	6	Sahni 1974
KSatisfiability → TimetableDesign	#486	4	Even-Itai-Shamir 1976
KSatisfiability → CyclicOrdering	#918	5	Galil-Megiddo 1977
KSatisfiability → OneInThreeSatisfiability	#862	5	Schaefer 1978
KSatisfiability → AcyclicPartition	#247	4	via SubsetSum→Partition chain

Rejected as unsound (4 rules)

Source → Target	Issue	Reason
KSatisfiability → FeasibleRegisterAssignment	#905	Counterexample: unsat 3-CNF admits feasible FRA schedule; GJ reference is from FVS not 3SAT
KSatisfiability → DirectedTwoCommodityIntegralFlow	#368	Model has arc-only capacity; variable gadget needs vertex-capacity blocking
KSatisfiability → MultipleChoiceBranching	#243	MCB validator doesn't enforce root-reachability; unsat formula yields valid MCB witness
KSatisfiability → ConsistencyOfDatabaseFrequencyTables	#468	Construction incomplete/unimplementable — object/attribute semantics under-specified

Also skipped

• [Rule] 3SAT to Precedence Constrained Scheduling #476 (PrecedenceConstrainedScheduling) — issue labeled "Wrong"

Test plan

• cargo test --lib — all tests pass
• Individual rule tests verified after each implementation
• cargo clippy --all-targets --features ilp-highs -- -D warnings — passed
• make paper — passed (Typst builds successfully)
• Full cargo test --features "ilp-highs example-db" --workspace -- --include-ignored — pre-existing model_specs_are_optimal HiGHS test times out locally; CI should handle this

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 97.14435% with 109 lines in your changes missing coverage. Please review.
✅ Project coverage is 98.14%. Comparing base (22c4b05) to head (111f2cd).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/rules/ksatisfiability_timetabledesign.rs	92.47%	44 Missing ⚠️
...c/rules/threedimensionalmatching_threepartition.rs	93.95%	27 Missing ⚠️
src/rules/ksatisfiability_quadraticcongruences.rs	95.66%	17 Missing ⚠️
...naesatisfiability_partitionintoperfectmatchings.rs	98.11%	4 Missing ⚠️
...unit_tests/rules/ksatisfiability_cyclicordering.rs	97.48%	4 Missing ⚠️
src/models/algebraic/quadratic_congruences.rs	96.70%	3 Missing ⚠️
src/rules/setsplitting_betweenness.rs	94.33%	3 Missing ⚠️
src/rules/ksatisfiability_preemptivescheduling.rs	99.27%	2 Missing ⚠️
...c/unit_tests/rules/threedimensionalmatching_ilp.rs	98.33%	2 Missing ⚠️
src/rules/ksatisfiability_acyclicpartition.rs	99.04%	1 Missing ⚠️
... and 2 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1010      +/-   ##
==========================================
- Coverage   98.17%   98.14%   -0.03%     
==========================================
  Files         896      920      +24     
  Lines       91715    95494    +3779     
==========================================
+ Hits        90039    93723    +3684     
- Misses       1676     1771      +95     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.