Commit 3ead548
docs: Add reduction classification and detailed survey (#9)
* docs: Add reduction classification and detailed survey
- 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>
* fix: Correct citation for Factoring→CircuitSAT reduction
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>
* docs: Polish writing to NeurIPS academic standard
- 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>
* docs: Combine detailed constructions with theorem/proof structure
- 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>
* docs: Improve summary table with overhead column and gray highlighting
- 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>
* docs: Add notation section and improve symbol introductions
- 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>
* docs: Verify facts and fix references
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>
* test: Improve test coverage for ReductionGraph module
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>
* fix: Fix clippy warnings and improve test coverage
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>
* fix: Correct Factoring→CircuitSAT citation and remove unused refs
- 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>
* test: Add coverage tests for ReductionGraph layout
- 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: Simplify layout code to remove dead branches
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>
* refactor: Remove unused iteration limit in BFS layout
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>
* refactor: Move layout computation from Rust to Typst
- 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>
* docs: Clean up Typst layout with explicit positions
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>
* docs: Optimize graph layout with compact node positions
- 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>
* fix: Unify SpinGlass types in ReductionGraph visualization
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>
* refactor: Use type-erased names for ReductionGraph topology
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>
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>1 parent c64ac3f commit 3ead548
15 files changed
Lines changed: 4309 additions & 162 deletions
File tree
- docs
- paper
- src
- problems
- reductions
- examples
- src/rules
- tests
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
10 | 10 | | |
11 | 11 | | |
12 | 12 | | |
13 | | - | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
14 | 16 | | |
15 | 17 | | |
16 | 18 | | |
| |||
35 | 37 | | |
36 | 38 | | |
37 | 39 | | |
38 | | - | |
| 40 | + | |
39 | 41 | | |
40 | | - | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
41 | 52 | | |
42 | 53 | | |
43 | 54 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
5 | 5 | | |
6 | 6 | | |
7 | 7 | | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
8 | 11 | | |
9 | 12 | | |
10 | 13 | | |
11 | 14 | | |
12 | 15 | | |
13 | | - | |
| 16 | + | |
14 | 17 | | |
15 | 18 | | |
16 | 19 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| 110 | + | |
| 111 | + | |
| 112 | + | |
| 113 | + | |
| 114 | + | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
0 commit comments