Detect and report primitive rules dominated by composite paths

[GiggleLiu]

Problem

Some primitive reduction rules have overhead that is equal to (or could be worse than) a composite path through other rules. These rules are not strictly necessary from an overhead perspective.

Analysis

Using pred path --all to enumerate all paths for each direct edge and comparing overheads, we found 6 genuinely redundant primitive rules (plus 3 trivial cast-composed duplicates):

Genuinely redundant (composite path through different problem types)

#	Primitive Rule	Best Composite Path	Overhead
1	KColoring → QUBO	KColoring → ILP → QUBO	num_vars = num_vertices^2 (equal)
2	MIS → ILP	MIS → MVC → ILP	num_vars=n, num_constraints=m (equal)
3	MIS → QUBO	MIS → ILP → QUBO or MIS → MVC → QUBO	num_vars=n (equal)
4	MaxSetPacking → ILP	SetPacking → MIS → ILP	num_vars=n, num_constraints=n^2 (equal)
5	MVC → ILP	MVC → MinSetCovering → ILP or MVC → MIS → ILP	num_vars=n, num_constraints=m (equal)
6	MVC → QUBO	MVC → ILP → QUBO or MVC → MIS → QUBO	num_vars=n (equal)

Cast-composed (trivially equal via zero-cost variant casts)

#	Primitive Rule	Composite Path
7	KSatisfiability/K2 → Satisfiability	K2 → KN (cast) → Satisfiability
8	KSatisfiability/K3 → Satisfiability	K3 → KN (cast) → Satisfiability
9	MIS/One → MIS/KingsSubgraph/i32	One→i32 (cast) → KingsSubgraph/i32

Note

"Equal overhead" does not mean these rules should be removed — direct rules are valuable for:

• Simpler solution extraction (fewer intermediate steps)
• Educational/documentation clarity
• Direct encoding may be numerically better in practice

But having an automated check helps us:

1. Avoid adding new rules that are strictly dominated
2. Understand the structure of the reduction graph
3. Make informed decisions about which rules to keep

Proposed Solution

Create a Rust utility (not a CLI subcommand) that:

1. Enumerates all primitive edges from the ReductionGraph
2. For each edge, finds all alternative composite paths (using existing find_all_paths)
3. Composes overheads along each path (using existing ReductionOverhead::compose)
4. Compares overhead expressions by asymptotic order: log < polynomial < exponential, and within polynomial by degree
5. Reports any primitive rule where a composite path has equal or smaller overhead

Key infrastructure already available

• ReductionGraph::find_all_paths() — path enumeration
• ReductionOverhead::compose() — overhead composition via Expr::substitute
• Expr::is_polynomial() — classification
• Expr::eval() — numeric evaluation for comparison

Comparison approach

Compare overhead expressions from a computational complexity perspective:

• Classify growth rate: O(log n) < O(n^k) < O(c^n) < O(n^n)
• Within polynomial: compare degree
• Use numeric evaluation at multiple test points as a fallback

[GiggleLiu]

After checking the current graph against the metadata/trust constraints, I think the removal set should be conservative rather than removing all 6 rules from the original analysis.

Proposed removal set

• Remove MinimumVertexCover -> ILP; canonical replacement: MinimumVertexCover -> MaximumIndependentSet -> ILP.
• Remove MinimumVertexCover -> QUBO; canonical replacement: MinimumVertexCover -> MaximumIndependentSet -> QUBO.
• Remove MaximumSetPacking -> ILP; canonical replacement: MaximumSetPacking -> MaximumIndependentSet -> ILP.
• Stop registering KSatisfiability<K2> -> Satisfiability and KSatisfiability<K3> -> Satisfiability as primitive graph edges; keep KN -> SAT registered and route K2/K3 through KN.

Rules I would explicitly keep

• Keep MaximumIndependentSet -> ILP as the canonical graph/set -> ILP entry point.
• Keep MaximumIndependentSet -> QUBO as the canonical graph -> QUBO entry point.
• Keep KColoring -> QUBO. Its only reported shortcut goes through KColoring -> ILP -> QUBO, and ILP -> QUBO is not currently trustworthy for symbolic shortcut/removal decisions because slack growth is not captured by the exposed symbolic metadata.

Concrete phased plan

1. Remove duplicate KSAT graph registrations first. Keep typed impls if tests/direct use still want them, but stop registering K2 -> SAT / K3 -> SAT as primitive edges.
2. Remove MinimumVertexCover -> QUBO and update its example/tests/paper entry to either a chained-path example or no dedicated direct-rule example.
3. Remove MinimumVertexCover -> ILP and update the matching example/tests/paper entry.
4. Remove MaximumSetPacking -> ILP and update the matching example/tests/paper entry.

Acceptance criteria

• Removed primitive rules disappear from the reduction graph.
• The affected source/target pairs still have composed paths.
• Examples, tests, and paper entries no longer reference deleted primitive rules.
• KColoring -> QUBO remains until ILP -> QUBO metadata is rich enough to make that shortcut comparison trustworthy.

I also wrote this up as a local concrete plan in docs/plans/2026-03-09-redundant-rule-removal-plan.md.

[GiggleLiu]

Redundant Rule Detection Results

The src/rules/analysis.rs utility has been implemented and detects the following dominated rules in the current reduction graph:

Dominated Rules (5)

#	Primitive Rule	Best Composite Path	Fields Compared
1	Factoring → ILP	Factoring → CircuitSAT → ILP{bool} → ILP{i32}	overhead composition
2	KSatisfiability → QUBO	KSat{K3} → KSat{KN} → SAT → CircuitSAT → SpinGlass{SG,i32} → SpinGlass{SG,f64} → QUBO{f64}	overhead composition
3	MIS → ILP	MIS{SG,i32} → MVC{SG,i32} → MinSetCovering{i32} → ILP{bool}	overhead composition
4	MIS → MIS (variant cast)	MIS{SG,One} → MIS{KS,One} → MIS{KS,i32}	overhead composition
5	MIS → QUBO	MIS{SG,i32} → MaxSetPacking{i32} → MaxSetPacking{f64} → QUBO{f64}	overhead composition

Unknown Comparisons (4)

All 4 unknowns are KSatisfiability → QUBO paths with expressions that contain exp() or other non-polynomial terms that the analysis cannot compare soundly.

Changes from Issue Analysis

Compared to the original issue's 6 genuinely redundant rules:

• KColoring → QUBO: was removed in a prior PR (not in current graph)
• MaxSetPacking → ILP: was removed in the ILP refactor (this branch)
• MVC → ILP: was removed in the ILP refactor (this branch)
• MVC → QUBO: was removed in the ILP refactor (this branch)
• MIS → ILP, MIS → QUBO: still present (kept intentionally — direct encodings are simpler)
• Factoring → ILP: newly detected (composite through CircuitSAT is equal or better)
• KSat → QUBO: newly detected (long chain through SAT → CircuitSAT → SpinGlass)

Implementation

The analysis utility is in src/rules/analysis.rs with tests in src/unit_tests/rules/analysis.rs. It uses polynomial normalization and monomial-dominance comparison to soundly detect dominated rules, returning Unknown for non-polynomial expressions.

The test test_find_dominated_rules_returns_known_set uses a bidirectional allow-list to guard against both unexpected new redundancies and stale entries.