docs: polish reductions.typ with theorem labels and cleanup

[GiggleLiu]

Summary

• Added <thm:*> labels to all 21 theorems for cross-referencing
• Cleaned up verbose impl Problem blocks from code examples (keeping just struct definitions)
• Moved table of contents after abstract with pagebreak

Pass 1 of 5 (Implementation Plan)

This PR implements Pass 1 of the reductions.typ polish plan (docs/plans/2026-02-10-polish-reductions-implementation.md).

Theorem Labels Added

• Trivial: is-vc, is-to-setpacking, vc-to-setcovering, matching-to-setpacking, spinglass-qubo
• QUBO: is-to-qubo, vc-to-qubo, coloring-to-qubo, setpacking-to-qubo, ksat-to-qubo, ilp-to-qubo
• Non-trivial: sat-to-is, sat-to-coloring, sat-to-dominatingset, sat-ksat, circuit-to-spinglass, factoring-to-circuit, spinglass-maxcut, coloring-to-ilp, factoring-to-ilp, is-to-gridgraph

Remaining Passes (Future PRs)

• Pass 2: Enhance problem definitions with field mappings
• Pass 3: Expand proofs and add GitHub example links
• Pass 4: Create 28 example files with JSON export
• Pass 5: Final verification

🤖 Generated with Claude Code

[GiggleLiu]

[action]

[codecov]

Codecov Report

❌ Patch coverage is 0% with 49 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.09%. Comparing base (6649410) to head (e59977c).
⚠️ Report is 2 commits behind head on main.

Files with missing lines	Patch %	Lines
src/export.rs	0.00%	49 Missing ⚠️

❌ Your patch check has failed because the patch coverage (0.00%) 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      #31      +/-   ##
==========================================
- Coverage   97.27%   97.09%   -0.19%     
==========================================
  Files         172      173       +1     
  Lines       25778    25827      +49     
==========================================
  Hits        25076    25076              
- Misses        702      751      +49     

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

[github-actions]

Summary of Changes

Paper Enhancements (docs/paper/reductions.typ)

Problem Definitions (Section 2):

• All 15 problem definitions now have field mapping paragraphs explaining the correspondence between mathematical notation and Rust struct fields
• Replaced "Reduces to/from" problem links with "Implemented reductions" referencing specific theorem labels (@thm:...)

Theorem Enhancements (Section 3):

• Added 7 new ILP formulation theorems with proofs: IS→ILP, VC→ILP, Matching→ILP, SetPacking→ILP, SetCovering→ILP, DominatingSet→ILP, Clique→ILP
• Expanded 5 trivial reduction proofs with explicit variable mapping explanations
• Added GitHub example links after all 28 theorem blocks
• Enabled theorem numbering for proper cross-referencing
• Updated summary table with 7 new ILP reduction rows

Fixes:

• Replaced invalid Typst ni symbol with in.rev (∋) in 3 ILP proof formulas

30 Standalone Example Files (examples/reduction_*.rs)

Each file follows a consistent pattern: detailed docstring → create instance → reduce → solve → extract → verify → export JSON.

Category	Files	Examples
Trivial/Complement	6	is_to_vc, vc_to_is, spinglass_to_qubo, qubo_to_spinglass, spinglass_to_maxcut, maxcut_to_spinglass
Graph→Set	3	is_to_setpacking, matching_to_setpacking, vc_to_setcovering
Penalty-method QUBO	6	is_to_qubo, vc_to_qubo, coloring_to_qubo, setpacking_to_qubo, ksatisfiability_to_qubo, ilp_to_qubo
ILP Formulations	9	coloring_to_ilp, factoring_to_ilp, is_to_ilp, vc_to_ilp, matching_to_ilp, setpacking_to_ilp, setcovering_to_ilp, dominatingset_to_ilp, clique_to_ilp
Non-trivial	6	sat_to_is, sat_to_coloring, sat_to_dominatingset, sat_to_ksat, circuit_to_spinglass, factoring_to_circuit

Verification

• ✅ make test — 1512 unit tests + 49 doc tests pass
• ✅ make clippy — zero warnings
• ✅ make paper — Typst compiles successfully
• ✅ All 30 examples compile, run, verify reductions, and export JSON

[Copilot]

Pull request overview

This PR updates the paper documentation (docs/paper/reductions.typ) to support cross-referencing of reduction theorems and aligns the paper with a new set of standalone Rust examples that demonstrate reductions and export JSON artifacts for embedding in the paper.

Changes:

• Added <thm:...> labels to reduction theorems and reorganized front-matter (TOC placement, theorem environment settings).
• Updated problem definitions to include “Implemented reductions” lists pointing at theorem labels, plus code-field mapping paragraphs.
• Added/updated many standalone examples/reduction_*.rs programs that run a reduction, verify extracted solutions, and export docs/paper/examples/*.json.

Reviewed changes

Copilot reviewed 35 out of 36 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
.gitignore	Ignores generated docs/paper/examples/ outputs.
docs/paper/reduction_graph.json	Updates the reduction graph data used by the paper diagram.
docs/paper/reductions.typ	Adds theorem labels, rewrites definition blocks, adds ILP theorem section + links to examples, moves TOC.
docs/plans/2026-02-10-polish-reductions-paper.md	Adds the documentation polish design plan.
docs/plans/2026-02-10-polish-reductions-implementation.md	Adds the detailed multi-pass implementation plan.
examples/export_petersen_mapping.rs	Expands narrative/output for the Petersen unit disk mapping export.
examples/reduction_circuit_to_spinglass.rs	New example: CircuitSAT → SpinGlass + JSON export.
examples/reduction_clique_to_ilp.rs	New example: Clique → ILP + JSON export.
examples/reduction_coloring_to_ilp.rs	New example: Coloring → ILP + JSON export.
examples/reduction_coloring_to_qubo.rs	New example: Coloring → QUBO + JSON export.
examples/reduction_dominatingset_to_ilp.rs	New example: DominatingSet → ILP + JSON export.
examples/reduction_factoring_to_circuit.rs	New example: Factoring → CircuitSAT + JSON export.
examples/reduction_factoring_to_ilp.rs	New example: Factoring → ILP + JSON export.
examples/reduction_ilp_to_qubo.rs	New example: ILP → QUBO + JSON export.
examples/reduction_is_to_ilp.rs	New example: IndependentSet → ILP + JSON export.
examples/reduction_is_to_qubo.rs	New example: IndependentSet → QUBO + JSON export.
examples/reduction_is_to_setpacking.rs	New example: IndependentSet → SetPacking + JSON export.
examples/reduction_is_to_vc.rs	New example: IndependentSet → VertexCovering + JSON export.
examples/reduction_ksatisfiability_to_qubo.rs	New example: KSatisfiability → QUBO + JSON export.
examples/reduction_matching_to_ilp.rs	New example: Matching → ILP + JSON export.
examples/reduction_matching_to_setpacking.rs	New example: Matching → SetPacking + JSON export.
examples/reduction_maxcut_to_spinglass.rs	New example: MaxCut → SpinGlass + JSON export.
examples/reduction_qubo_to_spinglass.rs	New example: QUBO → SpinGlass + JSON export.
examples/reduction_sat_to_coloring.rs	New example: SAT → Coloring + JSON export.
examples/reduction_sat_to_dominatingset.rs	New example: SAT → DominatingSet + JSON export.
examples/reduction_sat_to_is.rs	New example: SAT → IndependentSet + JSON export.
examples/reduction_sat_to_ksat.rs	New example: SAT → kSAT + JSON export.
examples/reduction_setcovering_to_ilp.rs	New example: SetCovering → ILP + JSON export.
examples/reduction_setpacking_to_ilp.rs	New example: SetPacking → ILP + JSON export.
examples/reduction_setpacking_to_qubo.rs	New example: SetPacking → QUBO + JSON export.
examples/reduction_spinglass_to_maxcut.rs	New example: SpinGlass → MaxCut + JSON export.
examples/reduction_spinglass_to_qubo.rs	New example: SpinGlass → QUBO + JSON export.
examples/reduction_vc_to_ilp.rs	New example: VertexCovering → ILP + JSON export.
examples/reduction_vc_to_is.rs	New example: VertexCovering → IndependentSet + JSON export.
examples/reduction_vc_to_qubo.rs	New example: VertexCovering → QUBO + JSON export.
examples/reduction_vc_to_setcovering.rs	New example: VertexCovering → SetCovering + JSON export.

---

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

[Copilot]

This theorem cites @def:independent-set in the Problems list, but it’s about Clique and the paper currently doesn’t define Clique. Either add a Clique definition (e.g., <def:clique>) and reference it here, or adjust the Problems list to point at the correct problem definition(s) to avoid broken/incorrect cross-references.

Suggested change

	#theorem[
	*(Clique $arrow.r$ ILP)* Maximum clique reduces to binary ILP with $|V|$ variables and $O(|overline(E)|)$ constraints. [_Problems:_ @def:independent-set, @def:ilp.]
	#definition[
	*(Clique).* Given a graph $G = (V, E)$ and an integer $k$, the *Clique* problem asks whether there exists a subset $K subseteq V$ of size at least $k$ such that every pair of distinct vertices in $K$ is adjacent, i.e., $(u, v) in E$ for all distinct $u, v in K$.
	] <def:clique>
	#theorem[
	*(Clique $arrow.r$ ILP)* Maximum clique reduces to binary ILP with $|V|$ variables and $O(|overline(E)|)$ constraints. [_Problems:_ @def:clique, @def:ilp.]

[Copilot]

The console output prints "Camera positions" / "cameras" for a Vertex Cover example, which is misleading and looks like leftover wording from a different example. Rename this to something VC-specific (e.g., selected vertices / cover vertices) to avoid confusing readers and keep the example aligned with the problem domain.

[Copilot]

The “Implemented reductions” list includes SetPacking→IS but links to @thm:is-to-setpacking, whose theorem statement is written as IS→Set Packing. Either add/label a separate theorem for SetPacking→IS (since the codebase implements it), or update this list/the theorem title to clearly indicate the reduction is bidirectional so the reference is accurate.

Suggested change

	_Implemented reductions:_ IS→VC (@thm:is-vc), IS→SetPacking (@thm:is-to-setpacking), IS→QUBO (@thm:is-to-qubo), IS→ILP (@thm:is-to-ilp), IS→GridGraph IS (@thm:is-to-gridgraph), VC→IS (@thm:is-vc), SAT→IS (@thm:sat-to-is), SetPacking→IS (@thm:is-to-setpacking).
	_Implemented reductions:_ IS→VC (@thm:is-vc), IS↔SetPacking (@thm:is-to-setpacking), IS→QUBO (@thm:is-to-qubo), IS→ILP (@thm:is-to-ilp), IS→GridGraph IS (@thm:is-to-gridgraph), VC→IS (@thm:is-vc), SAT→IS (@thm:sat-to-is).

[Copilot]

This “Implemented reductions” list references SetPacking→IS using @thm:is-to-setpacking, but the theorem is presented as IS→Set Packing. Since the library implements both directions, consider changing the theorem heading to a bidirectional arrow and/or renaming the label to reflect both directions, or introduce a separate theorem/label for SetPacking→IS.

Suggested change

	_Implemented reductions:_ SetPacking→IS (@thm:is-to-setpacking), SetPacking→QUBO (@thm:setpacking-to-qubo), SetPacking→ILP (@thm:setpacking-to-ilp), IS→SetPacking (@thm:is-to-setpacking), Matching→SetPacking (@thm:matching-to-setpacking).
	_Implemented reductions:_ IS↔SetPacking (@thm:is-to-setpacking), SetPacking→QUBO (@thm:setpacking-to-qubo), SetPacking→ILP (@thm:setpacking-to-ilp), Matching→SetPacking (@thm:matching-to-setpacking).

[Copilot]

The SetPacking→ILP formulation here uses per-universe-element constraints (∑_{sets containing u} x_i ≤ 1). However, the implemented reduction in src/rules/setpacking_ilp.rs generates constraints for each overlapping set pair (x_i + x_j ≤ 1). Please update the paper’s ILP formulation to match the actual implementation (or adjust the implementation) so readers don’t get an incorrect constraint structure/complexity.

Suggested change

	*(SetPacking $arrow.r$ ILP)* Set packing reduces to binary ILP with $|cal(S)|$ variables and $|U|$ constraints. [_Problems:_ @def:set-packing, @def:ilp.]
	] <thm:setpacking-to-ilp>
	#proof[
	_Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $sum_(S_i in.rev u) x_i <= 1$ for each $u in U$. Objective: maximize $sum_i w_i x_i$. _Solution extraction:_ $cal(P) = {S_i : x_i = 1}$.
	*(SetPacking $arrow.r$ ILP)* Set packing reduces to binary ILP with $|cal(S)|$ variables and at most $|cal(S)|^2$ constraints. [_Problems:_ @def:set-packing, @def:ilp.]
	] <thm:setpacking-to-ilp>
	#proof[
	_Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $x_i + x_j <= 1$ for each overlapping pair $S_i, S_j in cal(S)$ with $S_i cap S_j != emptyset$. Objective: maximize $sum_i w_i x_i$. _Solution extraction:_ $cal(P) = {S_i : x_i = 1}$.

[GiggleLiu]

[fix] Address the 5 Copilot review comments: fix Clique definition, fix VC example wording, fix bidirectional reduction references, and fix SetPacking→ILP formulation to match implementation.

[GiggleLiu]

[fix] Address the 5 Copilot review comments.

[GiggleLiu]

[fix] Address the 5 Copilot review comments.

[GiggleLiu]

[fix] Address the 5 Copilot review comments.

[github-actions]

Review Comments Addressed

All 5 Copilot review comments have been fixed in commit 065f842:

1. Clique definition missing — Added <def:clique> definition block and updated Clique→ILP theorem to reference @def:clique instead of @def:independent-set.

2. "Camera positions/cameras" in VC example — Changed to "Cover vertices/vertices" in examples/reduction_vc_to_qubo.rs to match the Vertex Cover domain.

3. IS "Implemented reductions" list — Changed IS→SetPacking + SetPacking→IS to single IS↔SetPacking with bidirectional arrow since both directions are implemented.

4. SetPacking "Implemented reductions" list — Same bidirectional fix: IS↔SetPacking replaces separate directional entries.

5. SetPacking→ILP formulation mismatch — Updated theorem and proof to match the actual implementation: constraints are x_i + x_j ≤ 1 for each overlapping pair (not per-universe-element), with bound updated to O(|S|²) in both the theorem statement and summary table.

Also fixed: Typst deprecation warning (sect → inter).

CI Note

The CI failure is a credentials issue (No credentials available) in the PR Automation workflow, not related to code changes. All code verification passes locally:

• make test — 1512 unit tests + 49 doc tests pass
• make clippy — zero warnings
• make paper — compiles cleanly with no warnings

[Copilot]

Pull request overview

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

---

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

[Copilot]

instance-vars doesn’t consider common keys like num_variables (used by CircuitSAT examples) and treats Factoring’s num_bits_first as the variable count (should be num_bits_first + num_bits_second). This makes the “with N variables” and ratio calculations inaccurate for several examples; consider checking num_variables early and handling Factoring as num_bits_first + num_bits_second.

Suggested change

	if "num_vertices" in inst { inst.num_vertices }
	else if "num_vars" in inst { inst.num_vars }
	else if "num_sets" in inst { inst.num_sets }
	else if "num_spins" in inst { inst.num_spins }
	else if "num_gates" in inst { inst.num_gates }
	if "num_variables" in inst { inst.num_variables }
	else if "num_vertices" in inst { inst.num_vertices }
	else if "num_vars" in inst { inst.num_vars }
	else if "num_sets" in inst { inst.num_sets }
	else if "num_spins" in inst { inst.num_spins }
	else if "num_gates" in inst { inst.num_gates }
	else if "num_bits_first" in inst and "num_bits_second" in inst { inst.num_bits_first + inst.num_bits_second }

[Copilot]

reduction-example computes tgt-vars / src-vars without guarding against src-vars == 0. If an instance schema is missing a recognized size field (or a typo occurs), Typst will error on division by zero during compilation. Consider rendering a fallback (e.g., "—") when src-vars <= 0.

Suggested change

	*Overhead:* #calc.round(tgt-vars / src-vars, digits: 1)x variable growth
	*Overhead:* #if src-vars > 0 and tgt-vars > 0 { #calc.round(tgt-vars / src-vars, digits: 1)x variable growth } else { — }

[Copilot]

The text says “IS↔SetPacking (@thm:is-to-setpacking)” but the referenced theorem in this document only states IS→SetPacking. Either add a separate theorem/label for SetPacking→IS (the intersection-graph reduction), or change the wording here to the one direction that’s actually documented.

Suggested change

	_Implemented reductions:_ IS→VC (@thm:is-vc), IS↔SetPacking (@thm:is-to-setpacking), IS→QUBO (@thm:is-to-qubo), IS→ILP (@thm:is-to-ilp), IS→GridGraph IS (@thm:is-to-gridgraph), VC→IS (@thm:is-vc), SAT→IS (@thm:sat-to-is).
	_Implemented reductions:_ IS→VC (@thm:is-vc), IS→SetPacking (@thm:is-to-setpacking), IS→QUBO (@thm:is-to-qubo), IS→ILP (@thm:is-to-ilp), IS→GridGraph IS (@thm:is-to-gridgraph), VC→IS (@thm:is-vc), SAT→IS (@thm:sat-to-is).

[Copilot]

The theorem label <thm:is-vc> is inconsistent with the rest of the file’s <thm:source-to-target> naming (e.g., <thm:is-to-setpacking>, <thm:vc-to-qubo>). To keep cross-references predictable (and aligned with the plan docs), consider renaming it to <thm:is-to-vc> (and/or adding <thm:vc-to-is>), updating the corresponding @thm: references.

Suggested change

	] <thm:is-vc>
	] <thm:is-to-vc>

[GiggleLiu]

[fix]

[github-actions]

Fixes Applied (63e948f)

CI Fix: codecov/patch (0% → ~100% on src/export.rs)

• Added 17 unit tests in src/unit_tests/export.rs covering all public functions:
  overhead_to_json, lookup_overhead, lookup_overhead_or_empty, variant_to_map, write_example, and serialization of ProblemSide, ReductionData, ResultData

Review Comments Addressed

1. instance-vars function — Added num_variables check first (for CircuitSAT), and Factoring now computes num_bits_first + num_bits_second instead of just num_bits_first

2. Division-by-zero guard — reduction-example now renders "—" when src-vars <= 0 instead of dividing by zero

3. Consistent theorem labels — Renamed <thm:is-vc> → <thm:is-to-vc> to match the <thm:source-to-target> convention used throughout the paper

4. Unidirectional IS→SetPacking — Changed IS↔SetPacking to IS→SetPacking in all "Implemented reductions" lists since the theorem only documents the IS→SetPacking direction

5. Updated all cross-references — All @thm:is-vc references updated to @thm:is-to-vc in IS and VC definition blocks

Verification

• make test — all tests pass (including 17 new export tests)
• make clippy — zero warnings
• make paper — Typst compiles cleanly

[GiggleLiu]

[debug]