feat: Implement Factoring → ILP reduction (issue #21)

[GiggleLiu]

Summary

• Implement Factoring → ILP reduction using McCormick linearization with carry propagation
• Add 16 comprehensive tests including closed-loop verification pattern
• Update reduction graph and documentation with code example

Implementation Details

Variables:

• Binary p_i, q_j ∈ {0,1} for factor bits
• Binary z_ij ∈ {0,1} for products p_i × q_j
• Integer c_k ≥ 0 for carries at each bit position

Constraints:

• McCormick: z_ij ≤ p_i, z_ij ≤ q_j, z_ij ≥ p_i + q_j - 1
• Bit equations: Σ_{i+j=k} z_ij + c_{k-1} = N_k + 2·c_k
• No overflow: c_{m+n-1} = 0

Complexity: O(m×n) variables and constraints for m-bit × n-bit factorization.

Test Plan

• Closed-loop tests (factor 6, 15, 35, primes, squares)
• Infeasibility detection (target too large)
• Variable/constraint count formulas verified
• Solution extraction correctness

Closes #21

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 99.35691% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 98.07%. Comparing base (f81fef3) to head (523666e).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
src/rules/factoring_ilp.rs	99.34%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main      #22      +/-   ##
==========================================
+ Coverage   98.04%   98.07%   +0.02%     
==========================================
  Files          59       60       +1     
  Lines       12265    12550     +285     
==========================================
+ Hits        12025    12308     +283     
- Misses        240      242       +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.

[Copilot]

Pull request overview

Implements a new reduction from the specialized Factoring problem to ILP using McCormick linearization plus carry propagation, and updates the reduction graph documentation accordingly.

Changes:

• Add Factoring -> ILP reduction rule with inventory registration and solution extraction.
• Extend the runtime reduction graph (type registry + documented edges) to include ILP as a target for Factoring.
• Update docs (reduction graph diagrams + paper theorem/example + regenerated JSON graph data).

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
src/rules/mod.rs	Registers and re-exports the new factoring_ilp reduction behind the ilp feature.
src/rules/graph.rs	Adds ILP as a registered type and includes a Factoring→ILP edge in the graph.
src/rules/factoring_ilp.rs	New Factoring→ILP reduction implementation (McCormick + carries) with comprehensive tests.
docs/src/reductions/graph.md	Updates the reduction graph diagram to show ILP and the new Factoring→ILP edge.
docs/plans/2026-01-31-factoring-ilp-design.md	Adds a design document for the reduction formulation and test plan.
docs/paper/reductions.typ	Adds a theorem/proof sketch and a closed-loop Rust example for Factoring→ILP.
docs/paper/reduction_graph.json	Regenerates the paper reduction graph data to include Factoring→ILP.

---

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

[Copilot]

The design doc references src/rules/coloring_ilp.rs as an existing pattern, but that file doesn’t exist in this repo (no matches under src/rules). Please update the reference to a real file (e.g., src/rules/vertexcovering_ilp.rs, src/rules/clique_ilp.rs) or remove it to avoid confusing readers.

Suggested change

	- Existing implementation: `src/rules/coloring_ilp.rs` (pattern reference)
	- Existing implementation: `src/rules/vertexcovering_ilp.rs` (pattern reference)

[Copilot]

add_edge!("Factoring" => "ILP") is currently added unconditionally, which makes the reduction graph advertise a Factoring→ILP edge even when the ilp feature is disabled (the actual ReduceTo<ILP> for Factoring impl lives behind that feature). Please gate this edge behind #[cfg(feature = "ilp")] or remove the manual edge and rely solely on the inventory-registered reduction when the feature is enabled.

Suggested change

	// ILP reductions (for solver targets)
	// ILP reductions (for solver targets)
	#[cfg(feature = "ilp")]

[Copilot]

((target >> k) & 1) will panic when k >= 64 (shift overflow on u64). Since k iterates up to num_bit_positions and m + n can exceed 64, this can crash the reduction for larger bit-width settings. Compute N_k with a guard (e.g., treat bits beyond 63 as 0) or cap the modeled bit positions to the representable width of target.

Suggested change

	// RHS is N_k (k-th bit of target)
	let n_k = ((target >> k) & 1) as f64;
	// RHS is N_k (k-th bit of target). For k >= 64, the bit is 0 for u64.
	let n_k = if k < 64 {
	((target >> k) & 1) as f64
	} else {
	0.0
	};

[Copilot]

The reduction sizes are documented/registered as depending on m and n only (inventory overhead: carries = m+n, constraints = 3mn + (m+n) + 1), but the implementation uses num_bit_positions = max(m+n, target_bits) which makes num_vars/constraints depend on target for large targets. This breaks the overhead formulas and diverges from the stated formulation (c_k for k=0..m+n-1, c_{m+n-1}=0). Consider keeping num_bit_positions = m+n and handling target_bits > m+n by emitting an immediately-infeasible ILP (or a single unsatisfiable constraint) instead of adding extra carry positions.

[Copilot]

The example uses ILP / ILPSolver, which are behind the crate’s ilp feature. Consider noting in the paper snippet that consumers must enable the ilp feature (e.g., in Cargo.toml or via --features ilp), otherwise this example won’t compile when copied.

[Copilot]

This regenerated JSON includes large ordering-only changes (nodes/edges reordered) beyond the new Factoring→ILP edge, which will create noisy diffs going forward. Consider making the generator output deterministic (e.g., sort nodes by id and edges by (source,target) before serializing) so future graph regenerations are stable.