-
Notifications
You must be signed in to change notification settings - Fork 0
docs: Add reduction classification and detailed survey #9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #9 +/- ##
==========================================
+ Coverage 97.94% 97.97% +0.03%
==========================================
Files 55 55
Lines 11373 11659 +286
==========================================
+ Hits 11139 11423 +284
- Misses 234 236 +2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
945816a to
2adf82d
Compare
- Add Typst document (docs/paper/reductions.typ) with: - Formal problem definitions - Reduction theorems with proofs - Classification of reductions as trivial vs non-trivial - Detailed survey of 7 non-trivial reductions with references - Auto-generated reduction graph from JSON - Add JSON export for reduction graph: - ReductionGraphJson, NodeJson, EdgeJson structs in graph.rs - Automatic layered layout algorithm - export_graph example to generate JSON - Update mdBook documentation: - Add Mermaid diagram to reductions/graph.md - Expand available.md with all 17 reductions and citations - Add CircuitSAT and Factoring to satisfiability.md - Add references.bib with academic citations 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
2adf82d to
80b986b
Compare
Remove incorrect Shor 1994 reference (quantum algorithm) and add note that this is a folklore result using classical array multiplier circuits. The construction is standard in hardware verification and has no single canonical academic reference. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Tighten prose with concise mathematical definitions - Use consistent formal notation throughout - Improve theorem statements with compact formatting - Restructure sections for better flow - Use proper figure references (@fig:reduction-graph) - Condense detailed constructions while preserving rigor 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Merge Section 5 (Detailed Constructions) into Section 3 (Reductions) - Each theorem now includes full constructive proof - Wrap tables in figures with captions (tab:gadgets, tab:summary) - Add summary table with all reductions and references - Fix deprecated `sect` to `inter` for set intersection 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Remove Type column, use gray background for trivial reductions - Add Overhead column showing reduction complexity - Update caption to explain gray row meaning 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add Notation subsection defining graph notation G=(V,E), complement, cardinality, negation, literals, clauses, CNF, and abbreviations - Expand definition titles to include abbreviations (IS, VC) - Clarify SAT definition with explicit mention of clauses and literals - Improve Spin Glass definition with Hamiltonian explanation - Clarify Circuit-SAT gate types and Factoring bit representation - Add introductory sentence for graph problems section 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Reference verification: - Karp 1972: Verified for SAT→IS (Karp's 21 NP-complete problems) - Garey & Johnson 1979: Verified for SAT→Coloring, SAT→DominatingSet - Cook 1971: Verified for Cook-Levin theorem - Whitfield 2012: Verified for ground-state spin logic gate gadgets - Lucas 2014: Verified for comprehensive Ising formulations of NP problems - Barahona 1982: Verified for Ising/MaxCut NP-hardness Fixes: - Remove nguyen2023 from CircuitSAT→SpinGlass (paper is about tensor network inference, not circuit reductions) - Add lucas2014 to SpinGlass↔MaxCut summary table reference 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add comprehensive tests for: - categorize_type() function with all problem categories - simplify_type_name() function - SAT-based reductions (SAT→IS, SAT→Coloring, SAT→DominatingSet) - Circuit reductions (Factoring→CircuitSAT→SpinGlass path) - Optimization reductions (SpinGlass↔QUBO, MaxCut↔SpinGlass) - k-SAT reductions (SAT↔3-SAT bidirectional) - JSON layout positions validation - All categories presence in JSON output - Edge cases for ReductionPath (empty, single node) - Default trait implementation - File I/O for to_json_file() Test count increased from 11 to 23 tests for the graph module. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pull request overview
This PR adds comprehensive documentation for problem reductions, including a formal Typst mathematical document with proofs, academic citations, and automated visualization capabilities. The changes classify reductions as trivial (6) vs non-trivial (7) and provide detailed academic references.
Changes:
- Added JSON export functionality to
ReductionGraphwith automatic layered layout computation using a simplified Sugiyama algorithm - Created Typst mathematical document (
docs/paper/reductions.typ) with formal problem definitions, reduction theorems, and constructive proofs - Expanded mdBook documentation with Mermaid diagrams, academic citations, and detailed reduction explanations
- Added build automation for generating the reduction graph JSON and compiling the Typst paper
Reviewed changes
Copilot reviewed 13 out of 14 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| src/rules/mod.rs | Exports new JSON-related types (NodeJson, EdgeJson, ReductionGraphJson) |
| src/rules/graph.rs | Implements JSON export, bidirectional edge detection, and layered graph layout algorithm |
| examples/export_graph.rs | Example program to export reduction graph to JSON file |
| docs/src/reductions/index.md | Updated with additional reduction mappings |
| docs/src/reductions/graph.md | Added Mermaid flowchart diagram and expanded API documentation |
| docs/src/reductions/available.md | Comprehensive documentation with academic citations for all reductions |
| docs/src/problems/satisfiability.md | Expanded with formal definitions, complexity notes, and reduction examples |
| docs/paper/references.bib | BibTeX bibliography with 8 academic references |
| docs/paper/reductions.typ | Typst document with formal mathematical definitions and proofs |
| docs/paper/reduction_graph.json | Auto-generated JSON representation of reduction graph |
| book.toml | Added Mermaid preprocessor and JavaScript configuration |
| Makefile | Added targets for mdbook, paper compilation, and documentation building |
| mermaid-init.js | JavaScript for Mermaid theme handling in mdBook |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
docs/paper/references.bib
Outdated
|
|
||
| @article{nguyen2023, | ||
| author = {Manh-Tien Nguyen and Jin-Guo Liu and others}, | ||
| title = {Tensor network message passing}, | ||
| journal = {PRX Quantum}, | ||
| volume = {4}, | ||
| pages = {010316}, | ||
| year = {2023} | ||
| } |
Copilot
AI
Jan 25, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The nguyen2023 reference is defined in the bibliography but is never cited in the Typst document (reductions.typ). This is an unused reference that should either be removed or cited in the document if it's relevant to the content.
| @article{nguyen2023, | |
| author = {Manh-Tien Nguyen and Jin-Guo Liu and others}, | |
| title = {Tensor network message passing}, | |
| journal = {PRX Quantum}, | |
| volume = {4}, | |
| pages = {010316}, | |
| year = {2023} | |
| } |
docs/paper/references.bib
Outdated
| @article{nguyen2023, | ||
| author = {Manh-Tien Nguyen and Jin-Guo Liu and others}, | ||
| title = {Tensor network message passing}, | ||
| journal = {PRX Quantum}, | ||
| volume = {4}, | ||
| pages = {010316}, | ||
| year = {2023} | ||
| } |
Copilot
AI
Jan 25, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The Gavril 1972 reference is cited in the mdBook documentation (docs/src/reductions/available.md) but is missing from the BibTeX file (references.bib). To maintain consistency and academic rigor, this reference should be added to the bibliography.
The citation should be:
@Article{gavril1972,
author = {Fănică Gavril},
title = {Algorithms for Minimum Coloring, Maximum Clique, Minimum Covering by Cliques, and Maximum Independent Set of a Chordal Graph},
journal = {SIAM Journal on Computing},
volume = {1},
number = {2},
pages = {180--187},
year = {1972}
}
src/rules/graph.rs
Outdated
| // Step 5: Assign positions (compact layout) | ||
| let y_spacing = 1.0; |
Copilot
AI
Jan 25, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The layout computation at line 429 calculates total_width as (nodes.len() as f64 - 1.0) * x_spacing, which will result in a negative value when nodes.len() is 0 (an empty layer). While this edge case is unlikely in practice since layers are created from non-empty groups, it would be more robust to handle this case explicitly or add a comment indicating that empty layers cannot occur. The calculation would be more defensive as: let total_width = nodes.len().saturating_sub(1) as f64 * x_spacing;
| edit-url-template = "https://github.com/liujinguo/problemreductions/edit/main/{path}" | ||
| additional-css = [] | ||
| additional-js = [] | ||
| additional-js = ["mermaid.min.js", "mermaid-init.js"] |
Copilot
AI
Jan 25, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The book.toml configuration references "mermaid.min.js" in the additional-js array (line 16), but this file does not appear to exist in the repository. The mdbook-mermaid preprocessor typically provides the necessary Mermaid JavaScript automatically, so including mermaid.min.js here is likely redundant and may cause errors if the file is missing. Consider removing "mermaid.min.js" from the additional-js array and relying on the preprocessor to inject the necessary scripts, or ensure the file is properly included if it's needed for a specific reason.
| additional-js = ["mermaid.min.js", "mermaid-init.js"] | |
| additional-js = ["mermaid-init.js"] |
docs/src/reductions/available.md
Outdated
|
|
||
| Constructs a multiplier circuit that computes p * q and constrains the output to equal the target number N. A satisfying assignment reveals the factors. | ||
|
|
||
| **Citation**: Shor, P. W. (1994). "Algorithms for quantum computation: discrete logarithms and factoring". Proceedings of the 35th Annual Symposium on Foundations of Computer Science. pp. 124-134. |
Copilot
AI
Jan 25, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The citation for the Factoring to CircuitSAT reduction attributes the multiplier circuit construction to Shor 1994. However, Shor's paper focuses on quantum algorithms for factoring, not the classical reduction from factoring to CircuitSAT via multiplier circuits. This reduction is actually folklore in computational complexity theory and predates Shor's work. The Typst document correctly labels this as "Folklore" in the summary table. This citation should either be removed or replaced with a more appropriate reference, or the comment should clarify that Shor's work is related but not the original source of this particular reduction.
Clippy fixes: - Replace `.len() > 0` with `!.is_empty()` in JSON validation tests Additional tests for edge case coverage: - test_has_direct_reduction_unregistered_types - test_find_paths_unregistered_source - test_find_paths_unregistered_target - test_find_shortest_path_no_path - test_json_node_positions_all_finite - test_categorize_circuit_as_specialized Test count increased from 23 to 29 for the graph module. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Change Shor 1994 to Folklore for Factoring→CircuitSAT reduction (Shor's paper is about quantum algorithms, not classical circuits) - Remove unused shor1994 and nguyen2023 from references.bib The Factoring→CircuitSAT reduction uses standard array multiplier circuits, a well-known technique in hardware verification with no single canonical academic reference. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add test_layout_layer_ordering to verify layer hierarchy - Add test_multiple_nodes_per_layer_spacing for x-coordinate spacing - Add test_edge_bidirectionality_detection for edge direction detection - Add test_simplify_type_name_edge_cases for edge case handling These tests improve patch coverage for the layout computation code. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Refactor compute_layered_layout to use direct name-based checks instead of categorize_type, eliminating unreachable code branches that caused coverage gaps. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
The iteration limit was defensive code that never executed since the BFS traverses a finite DAG. Removing it improves code coverage. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Remove x, y position fields from NodeJson struct - Remove compute_layered_layout function from Rust - Remove position-related tests - Add manual node-positions dictionary in Typst for layered layout - JSON now exports only topology (id, label, category, edges) This simplifies the Rust code and delegates visualization concerns to the presentation layer (Typst). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Fletcher doesn't support auto positioning for arbitrary nodes. Keep manual layered positions in Typst dictionary for clarity. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Use node ID for position lookup (handles duplicate labels like SpinGlass) - Two-branch layout: SAT (left) + Physics (right) - Connected nodes placed close together - Clear hierarchical flow from top to bottom 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Register only SpinGlass<f64> in the graph to avoid duplicate nodes with identical labels. Update edges and tests accordingly: - MaxCut<i32> -> SpinGlass<f64> - CircuitSAT<i32> -> SpinGlass<f64> The actual reduction implementations remain generic and work with any compatible weight type. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Change ReductionGraph to use base type names (e.g., "SpinGlass" instead of "SpinGlass<i32>") for graph topology. This allows finding reduction paths regardless of weight type parameters. Changes: - Graph nodes now store base type names, not TypeId - Multiple concrete types (e.g., MaxCut<i32>, MaxCut<f64>) map to same node - Add find_paths_by_name() and has_direct_reduction_by_name() methods - Update JSON export to use simplified names - Update Typst positions to match new node IDs This design separates topology (which problems reduce to which) from type-specific implementation details. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Summary
docs/paper/reductions.typ) with formal problem definitions, reduction theorems, and proofsClassification
Trivial Reductions
Non-Trivial Reductions
Files Changed
docs/paper/reductions.typ- Typst document with math definitionsdocs/paper/references.bib- Academic bibliographydocs/paper/reduction_graph.json- Auto-generated graph datasrc/rules/graph.rs- JSON export and layout algorithmexamples/export_graph.rs- Example to generate JSONdocs/src/reductions/*.md- Updated mdBook pagesTest plan
cargo run --example export_graph🤖 Generated with Claude Code