feat: add 8 Tier 1a reduction rules (#770)

[zazabap]

Summary

Implements 8 simple, verified Tier 1a reduction rules from Garey & Johnson (issue #770):

#	Source → Target	Technique	Lines
#199	HamiltonianCircuit → HamiltonianPath	Vertex duplication + pendants	~80
#201	KClique → SubgraphIsomorphism	Pattern = K_k	~60
#203	Partition → MultiprocessorScheduling	m=2, D=S/2	~60
#234	HamiltonianPath → IsomorphicSpanningTree	T = P_n	~55
#259	HamiltonianCircuit → BottleneckTravelingSalesman	{1,2}-distances	~80
#464	KClique → ConjunctiveBooleanQuery	k-clique as Boolean CQ	~75
#487	ExactCoverBy3Sets → StaffScheduling	Subset-to-schedule encoding	~60
#753	Satisfiability → NAESatisfiability	Sentinel variable construction	~65

Each rule includes:

• Full ReduceTo implementation with #[reduction(overhead = {...})]
• ReductionResult with extract_solution()
• Canonical example-db spec
• 4-9 unit tests (closed-loop, edge cases, extraction, negative cases)

Fixes #199, Fixes #201, Fixes #203, Fixes #234, Fixes #259, Fixes #464, Fixes #487, Fixes #753

Test plan

• make check passes (fmt + clippy + test)
• CI passes
• All 8 issues auto-close on merge

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 99.02597% with 9 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.82%. Comparing base (a69b719) to head (0033e2a).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/rules/hamiltoniancircuit_hamiltonianpath.rs	94.20%	4 Missing ⚠️
src/rules/graph_helpers.rs	92.10%	3 Missing ⚠️
src/rules/satisfiability_naesatisfiability.rs	97.95%	1 Missing ⚠️
..._tests/rules/partition_multiprocessorscheduling.rs	98.73%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #777      +/-   ##
==========================================
+ Coverage   97.79%   97.82%   +0.02%     
==========================================
  Files         582      599      +17     
  Lines       65454    66337     +883     
==========================================
+ Hits        64012    64893     +881     
- Misses       1442     1444       +2     

☔ 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.

[zazabap]

Agentic Review Report

Structural Check

Rule	Math OK	Overhead OK	Registration	Tests	Example	Issues
HC → HP	✅	⚠️ MINOR	✅	6	✅	num_edges is worst-case upper bound (no deg(0) getter available)
HC → BTSP	✅	✅	✅	4	✅	None
HP → IST	✅	✅	✅	5	✅	None
KClique → SubIso	✅	✅	✅	5	✅	None
KClique → CBQ	✅	✅	✅	5	✅	None
Partition → MPS	✅	⚠️ MINOR	✅	7	✅	Overhead missing num_processors and deadline fields
XC3S → StaffSched	✅	✅	✅	5	✅	None
SAT → NAESAT	✅	✅	✅	9	✅	None

All 8 reductions mathematically verified. Forward/backward correctness confirmed. Solution extraction inverts correctly. Example specs validated with concrete instances.

Minor findings:

• HC→HP: num_edges = "num_edges + num_vertices + 1" is an upper bound (actual = m + deg(0) + 2). No getter for deg(0), so this is the tightest expressible formula.
• Partition→MPS: Only num_tasks declared in overhead. Could add num_processors = "2" and deadline = "total_sum / 2".

---

Quality Check

Design Principles:

• DRY: HC→BTSP extract_solution (~55 lines) and reduce_to (~12 lines) are verbatim copies of HC→TSP. Should be refactored into shared helpers.
• KISS: All 8 rules are appropriately simple for textbook reductions. No over-engineering.
• Cohesion: Each rule is self-contained with its own struct, impl, example, and tests. Good.

Test Quality:

Rule	# Tests	Closed-loop	Edge cases	Quality
HC → BTSP	4	✅	Non-Hamiltonian, manual extraction	Strong
HC → HP	6	✅	No-circuit, reversed path, triangle	Strong
HP → IST	5	✅	Star graph, complete graph, triangle	Strong
KClique → SubIso	6	✅	No clique, k=1, k=2	Strong
KClique → CBQ	5	✅	No clique, k=1	Strong
Partition → MPS	8	✅	Odd sum, single element, equal, two elements	Excellent
SAT → NAESAT	9	✅	Unsat, empty, sentinel T/F, all-solutions	Excellent
XC3S → StaffSched	5	✅	No solution, unique cover, structure	Strong

Issues:

• MEDIUM src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs:26-82 — DRY violation: extract_solution duplicates HC→TSP verbatim
• LOW — Inconsistent import style: some test files use use super::*;, others use explicit imports
• INFO — No empty-graph / k=0 edge case tests for HC→BTSP, KClique→CBQ, KClique→SubIso

---

Agentic Feature Tests

Rule	In catalog	pred show	pred path	pred reduce	Notes
HC → HamiltonianPath	✅	✅	✅	✅	Grows 6→9 vertices
HC → BottleneckTSP	✅	✅	✅	✅	Complete graph, {1,2} weights
HP → IsomorphicSpanningTree	✅	✅	✅	✅	Tree = path graph
KClique → SubgraphIsomorphism	✅	✅	✅	✅	Pattern = K_3
KClique → ConjunctiveBooleanQuery	✅	✅	✅	✅	k² conjuncts
Partition → MultiprocessorScheduling	✅	✅	✅	✅	2 processors, D=S/2
XC3S → StaffScheduling	✅	✅	✅	✅	Schedules mirror subsets
SAT → NAESatisfiability	✅	✅	✅	✅	Sentinel variable added

All 8 rules pass all CLI integration tests. No failures or unexpected behavior.

---

Generated by review-pipeline

[Copilot]

Pull request overview

Adds eight Tier 1a reduction rules (Garey & Johnson) to the reductions registry, along with canonical example-db specs and unit tests to validate closed-loop correctness and solution extraction.

Changes:

• Implement 8 new ReduceTo reductions (SAT→NAE-SAT, Partition→MPS, HC→HP, HC→BTSP, HP→IST, KClique→SubgraphIsomorphism, KClique→CBQ, X3C→StaffScheduling).
• Add focused unit tests per rule (closed-loop, structure checks, extraction, and negative cases).
• Register new rule modules and wire their canonical example specs into src/rules/mod.rs.

Reviewed changes

Copilot reviewed 17 out of 17 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/rules/mod.rs	Registers the new rule modules and includes their canonical example specs in the rule example-db export list.
src/rules/satisfiability_naesatisfiability.rs	Implements SAT→NAE-SAT sentinel-variable reduction + example-db spec + test module hook.
src/rules/partition_multiprocessorscheduling.rs	Implements Partition→MultiprocessorScheduling restriction-style reduction + example-db spec + test hook.
src/rules/kclique_subgraphisomorphism.rs	Implements KClique→SubgraphIsomorphism by using a complete pattern graph K_k + example-db spec + test hook.
src/rules/kclique_conjunctivebooleanquery.rs	Implements KClique→CBQ encoding clique as a Boolean conjunctive query + example-db spec + test hook.
src/rules/hamiltonianpath_isomorphicspanningtree.rs	Implements HamiltonianPath→IsomorphicSpanningTree via T = P_n + example-db spec + test hook.
src/rules/hamiltoniancircuit_hamiltonianpath.rs	Implements HamiltonianCircuit→HamiltonianPath via vertex-duplication + pendant endpoints + example-db spec + test hook.
src/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs	Implements HamiltonianCircuit→BTSP using {1,2}-weights on the complete graph + example-db spec + test hook.
src/rules/exactcoverby3sets_staffscheduling.rs	Implements X3C→StaffScheduling subset-to-schedule encoding + example-db spec + test hook.
src/unit_tests/rules/satisfiability_naesatisfiability.rs	Unit tests for SAT→NAE-SAT (structure, extraction, edge cases).
src/unit_tests/rules/partition_multiprocessorscheduling.rs	Unit tests for Partition→MPS (structure, odd sum, extraction, small cases).
src/unit_tests/rules/kclique_subgraphisomorphism.rs	Unit tests for KClique→SubgraphIsomorphism (yes/no cases, k=1/2/3).
src/unit_tests/rules/kclique_conjunctivebooleanquery.rs	Unit tests for KClique→CBQ (structure, satisfiable/unsatisfiable, extraction, k=1).
src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs	Unit tests for HP→IST (closed-loop, multiple graph families, negative case).
src/unit_tests/rules/hamiltoniancircuit_hamiltonianpath.rs	Unit tests for HC→HP (closed-loop, structure, extraction, negative case).
src/unit_tests/rules/hamiltoniancircuit_bottlenecktravelingsalesman.rs	Unit tests for HC→BTSP (closed-loop, weight structure, bottleneck gap, extraction).
src/unit_tests/rules/exactcoverby3sets_staffscheduling.rs	Unit tests for X3C→StaffScheduling (closed-loop, no-solution, unique-cover, structure).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[zazabap]

Solver Reachability Summary

Source problems (all have existing solver paths — no change needed)

Source	Solver path
HamiltonianCircuit	HC → TSP → ILP/bool
HamiltonianPath	HP → ILP/bool
KClique	KC → ILP/bool
Partition	Partition → Knapsack → ILP/bool
ExactCoverBy3Sets	XC3S → ILP/bool
Satisfiability	SAT → CircuitSAT → ILP/bool

Target problems

Target	Outgoing reductions	ILP solvable?	Notes
HamiltonianPath	→ IST, → ILP/bool	✅	Direct ILP path
BottleneckTravelingSalesman	→ ILP/i32	✅	Uses i32 variant
IsomorphicSpanningTree	→ ILP/bool	✅	Direct ILP path
SubgraphIsomorphism	→ ILP/bool	✅	Direct ILP path
MultiprocessorScheduling	→ ILP/bool	✅	Direct ILP path
NAESatisfiability	→ ILP/bool	✅	Direct ILP path
ConjunctiveBooleanQuery	None	❌	Dead end — no outgoing reductions. Needs CBQ → ILP.
StaffScheduling	None	❌	Dead end — no outgoing reductions. Needs StaffScheduling → ILP.

Action items

Two target problems are sink nodes (no outgoing reductions, unsolvable via ILP). They can still be solved by BruteForce, but ILP reductions would complete the solver coverage:

• ConjunctiveBooleanQuery → ILP
• StaffScheduling → ILP