feat: redundant rule detection via polynomial overhead comparison (#193)

[GiggleLiu]

Summary

• Refactor ILP to generic ILP<V> with VariableDomain trait (bool for binary, i32 for general integer)
• Add analysis module for detecting primitive reduction rules dominated by composite paths
• Uses asymptotic normalization (sum-of-monomials) and monomial-dominance comparison
• Remove genuinely redundant rules; keep false alarms (equal overhead or constant-factor-only) with documented allow-list

Key Changes

ILP type parameter

• ILP<bool> guarantees binary variables at compile time; ILP<i32> for general integer
• 9 reductions updated to target ILP<bool> directly
• New ILP<bool> → ILP<i32> cast reduction
• Factoring → ILP updated with carry bounds as constraints

Redundant rule detection (src/rules/analysis.rs)

• Enumerates all primitive rules, finds composite paths, compares overhead polynomially
• Detects 3 dominated rules (down from 5 after fixes):
  • Factoring → ILP{i32}: false alarm (composite 12x larger, same asymptotic class)
  • KSatisfiability{K3} → QUBO{f64}: genuine (composite saves num_vars QUBO variables), kept for practical value
  • MaxMatching{SimpleGraph,i32} → ILP{bool}: false alarm (composite produces identical ILP via MaxSetPacking)

Rules removed

• MIS → ILP, MIS → QUBO: composite via MVC is better
• MVC → ILP, MVC → QUBO: composite via MIS is better
• MIS{SimpleGraph,One} → MIS{KingsSubgraph,i32}: redundant diagonal variant cast (two-step path through KingsSubgraph/One is equivalent)

MaxSetPacking → ILP improved

• Changed from pairwise constraints (x_i + x_j ≤ 1) to element-based constraints (Σ_{i: e ∈ S_i} x_i ≤ 1)
• Fewer constraints (universe_size vs num_sets²), tighter LP relaxation

SAT → KColoring overhead simplified

• Dropped negative coefficients causing Unknown analysis results
• Simplified to asymptotic upper bound: num_vars + num_literals

Allow-list with variant-qualified keys

• test_find_dominated_rules_returns_known_set uses full variant display strings
• Bidirectional check: no unexpected dominated rules, no stale allow-list entries

Test plan

• Asymptotic normalization tests (exp/log/sqrt identities, additive constants, multivariate)
• Integration test with variant-qualified allow-list
• Duplicate primitive rule check
• All reduction closed-loop tests pass
• Full test suite passes with and without ilp-solver feature
• Paper updated (SetPacking → ILP description, reduction_graph.json regenerated)

Closes #193

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 88.66571% with 158 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.37%. Comparing base (53c13f1) to head (e7b2609).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/expr.rs	78.70%	56 Missing ⚠️
src/rules/analysis.rs	79.69%	53 Missing ⚠️
src/models/algebraic/closest_vector_problem.rs	26.66%	33 Missing ⚠️
src/unit_tests/rules/analysis.rs	93.89%	13 Missing ⚠️
src/rules/sat_ksat.rs	50.00%	3 Missing ⚠️

❌ Your patch status has failed because the patch coverage (88.66%) is below the target coverage (95.00%). You can increase the patch coverage or adjust the target coverage.

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #194      +/-   ##
==========================================
- Coverage   96.90%   96.37%   -0.54%     
==========================================
  Files         202      200       -2     
  Lines       27679    27871     +192     
==========================================
+ Hits        26823    26861      +38     
- Misses        856     1010     +154     

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

[GiggleLiu]

Please clean up all plan files introduced in this pr.

[GiggleLiu]

We still need this to test this reduction (throught path).

[Copilot]

Pull request overview

This PR introduces a new reduction-graph analysis utility to detect primitive rules that are asymptotically dominated by composite paths, and updates the reduction ecosystem (ILP domain typing, rule removals, tests/examples/docs) to align with the new redundancy model.

Changes:

• Add src/rules/analysis.rs (+ unit tests) for dominated-rule detection using asymptotic normalization + monomial dominance.
• Refactor ILP into a typed-domain model (ILP<bool> / ILP<i32>) and update solver + reductions accordingly.
• Remove/route around several direct reductions (e.g., MIS/MVC to QUBO/ILP) and adjust tests, examples, and docs to use reduction paths.

Reviewed changes

Copilot reviewed 95 out of 95 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/suites/reductions.rs	Adjust integration tests to use ReductionGraph paths and remove HyperGraph-based test.
tests/data/qubo/minimumvertexcover_to_qubo.json	Remove ground-truth dataset tied to deleted MVC→QUBO direct reduction.
src/unit_tests/variant.rs	Update variant-param expectations after removing HyperGraph parent relationship.
src/unit_tests/unitdiskmapping_algorithms/common.rs	Refactor MIS solving helpers to build ILP directly with typed ILP API.
src/unit_tests/unitdiskmapping_algorithms/weighted.rs	Update ILP construction to new typed ILP API.
src/unit_tests/topology/hypergraph.rs	Remove HyperGraph unit tests (HyperGraph removed).
src/unit_tests/solvers/ilp/solver.rs	Update ILP solver tests for typed ILP API and remove VarBounds usage.
src/unit_tests/rules/travelingsalesman_ilp.rs	Update TSP→ILP tests to target ILP<bool> and remove bounds assertions.
src/unit_tests/rules/reduction_path_parity.rs	Stop using solve_reduced for factoring; explicitly reduce/solve/extract with typed ILP.
src/unit_tests/rules/qubo_ilp.rs	Update QUBO→ILP tests to target ILP<bool>.
src/unit_tests/rules/minimumvertexcover_qubo.rs	Replace direct MVC→QUBO test with multi-step path-based test.
src/unit_tests/rules/minimumsetcovering_ilp.rs	Update SetCover→ILP tests to target ILP<bool> and remove bounds assertions.
src/unit_tests/rules/minimumdominatingset_ilp.rs	Update MinDomSet→ILP tests to target ILP<bool> and remove bounds assertions.
src/unit_tests/rules/maximumsetpacking_ilp.rs	Update MaxSetPacking→ILP tests to target ILP<bool> and adjust constraint expectations.
src/unit_tests/rules/maximummatching_ilp.rs	Update MaxMatching→ILP tests to target ILP<bool> and remove bounds assertions.
src/unit_tests/rules/maximumindependentset_qubo.rs	Replace direct MIS→QUBO test with multi-step path-based test.
src/unit_tests/rules/maximumindependentset_gridgraph.rs	Remove a weighted gridgraph cast test tied to removed cast/edge behavior.
src/unit_tests/rules/maximumclique_ilp.rs	Update MaxClique→ILP tests to target ILP<bool> and remove bounds assertions.
src/unit_tests/rules/ilp_qubo.rs	Update ILP→QUBO tests to construct ILP<bool> via new API.
src/unit_tests/rules/ilp_bool_ilp_i32.rs	Add tests for new ILP<bool> -> ILP<i32> cast/reduction.
src/unit_tests/reduction_graph.rs	Update expected KSAT→SAT path length due to KN cast registration change.
src/unit_tests/problem_size.rs	Update ILP problem-size test to use new typed ILP API.
src/unit_tests/expr.rs	Add tests for complexity-notation validation and asymptotic_normal_form.
src/topology/mod.rs	Remove HyperGraph from topology module exports/docs.
src/topology/hypergraph.rs	Remove HyperGraph implementation entirely.
src/topology/graph.rs	Remove SimpleGraph→HyperGraph parent/cast relationship.
src/solvers/ilp/solver.rs	Make solver generic over ILP<V> and adjust bounds logic to typed domains.
src/solvers/ilp/mod.rs	Update docs/examples for typed ILP API.
src/rules/travelingsalesman_ilp.rs	Switch TSP target to ILP<bool> and remove VarBounds-based construction.
src/rules/sat_ksat.rs	Keep typed K2/K3 impls but stop registering them as primitive edges (KN covers).
src/rules/sat_coloring.rs	Update SAT→Coloring overhead expressions.
src/rules/qubo_ilp.rs	Switch QUBO→ILP target to ILP<bool> and remove VarBounds.
src/rules/mod.rs	Add analysis module; remove direct MIS/MVC→QUBO modules; add ilp_bool_ilp_i32.
src/rules/minimumvertexcover_qubo.rs	Remove MVC→QUBO direct reduction implementation.
src/rules/minimumvertexcover_ilp.rs	Remove MVC→ILP direct reduction implementation.
src/rules/minimumsetcovering_ilp.rs	Switch SetCover→ILP target to ILP<bool> and remove VarBounds usage.
src/rules/minimumdominatingset_ilp.rs	Switch MinDomSet→ILP target to ILP<bool> and remove VarBounds usage.
src/rules/maximumsetpacking_ilp.rs	Switch MaxSetPacking→ILP target to ILP<bool> and change constraint construction to element-based.
src/rules/maximummatching_ilp.rs	Switch MaxMatching→ILP target to ILP<bool> and remove VarBounds usage.
src/rules/maximumindependentset_qubo.rs	Remove MIS→QUBO direct reduction implementation.
src/rules/maximumindependentset_ilp.rs	Remove MIS→ILP direct reduction implementation.
src/rules/maximumindependentset_gridgraph.rs	Remove weighted gridgraph cast edge/implementation.
src/rules/maximumclique_ilp.rs	Switch MaxClique→ILP target to ILP<bool> and remove VarBounds usage.
src/rules/ilp_qubo.rs	Restrict ILP→QUBO reduction impl to ILP<bool>; update overhead expression.
src/rules/ilp_bool_ilp_i32.rs	Add new reduction/cast ILP<bool> -> ILP<i32>.
src/rules/factoring_ilp.rs	Switch Factoring→ILP to ILP<i32>, change bounds to constraints, update tests/expectations.
src/rules/coloring_ilp.rs	Switch KColoring→ILP target to ILP<bool> and remove VarBounds usage.
src/rules/circuit_ilp.rs	Switch CircuitSAT→ILP target to ILP<bool> and remove VarBounds usage.
src/models/algebraic/mod.rs	Re-export VariableDomain; move VarBounds to CVP module.
src/models/algebraic/ilp.rs	Implement typed-domain ILP model (ILP<V>) and remove embedded VarBounds.
src/models/algebraic/closest_vector_problem.rs	Define VarBounds here after ILP no longer owns it.
src/lib.rs	Re-export asymptotic_normal_form + error type from expr.
scripts/generate_qubo_tests.py	Remove MVC→QUBO dataset generator (direct rule removed).
examples/reduction_*	Update multiple examples to use typed ILP and/or reduction paths.
docs/src/reductions/problem_schemas.json	Remove ILP bounds field from schema JSON.
docs/src/mcp.md	Update reduction-path text for MIS→QUBO now going through SetPacking.
docs/src/getting-started.md	Update “getting started” example to SetPacking→ILP narrative.
docs/src/design.md	Update variant hierarchy documentation after removing HyperGraph.
docs/src/cli.md	Update CLI examples/output to reflect changed paths/edges.
docs/plans/*	Add design docs for redundancy detection, ILP typing, and redundant rule removal.
docs/paper/reductions.typ	Update paper definitions/examples to reflect removed direct rules and new ILP model.
.claude/*	Add skill docs for rule-redundancy checking and update internal docs accordingly.

---

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

[Copilot]

The #[reduction(overhead = ...)] metadata here doesn't match the actual ILP instance constructed below. The implementation creates num_vars = m + n + m*n + (m+n) (or + target_bits when target_bits > m+n) and adds constraints totaling 3*m*n + 4*m + 4*n + 1 for feasible instances, but the overhead is currently set to m*n for both fields. This will skew ReductionGraph path costs and can make the new dominated-rule analysis incorrect. Please update the overhead expressions to reflect the construction (using num_bits_first / num_bits_second, and assuming target_bits <= m+n for feasible instances, or otherwise document/encode the max(m+n, target_bits) behavior).