docs: improve example instances implementation plan#41
Merged
Conversation
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Contributor
Author
|
[action] |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #41 +/- ##
=======================================
Coverage 97.37% 97.37%
=======================================
Files 176 176
Lines 26217 26217
=======================================
Hits 25530 25530
Misses 687 687 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Add an interactive Cytoscape.js-based reduction graph page to the mdBook documentation. The page loads reduction_graph.json, filters to base problem nodes, deduplicates edges, and renders an explorable directed graph with category-colored nodes and two-click shortest-path highlighting. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Plan Execution Summary: JSON Schema & Interactive VizExecuted StatusTasks 1–5 were already completed and merged (PRs #36 and #38). This execution completed the remaining work:
What was done (Task 6)Created interactive Cytoscape.js reduction graph page:
Verification
|
Contributor
Author
|
[action] |
GiggleLiu
commented
Feb 10, 2026
docs/src/reductions/graph.md
Outdated
Contributor
Author
There was a problem hiding this comment.
Remove this file.
docs/src/SUMMARY.md
Outdated
| - [Solvers](./solvers.md) | ||
| - [File I/O](./io.md) | ||
|
|
||
| # Reductions |
Contributor
Author
There was a problem hiding this comment.
Remove the added lines.
Contributor
Author
|
[action] implement first 10 examples. |
Replace trivial P4 path graph (4 vertices, 3 edges, MIS=2) with the Petersen graph (10 vertices, 15 edges, 3-regular, MIS=4) in all four MIS reduction examples: QUBO, ILP, MinimumVertexCover, MaximumSetPacking. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace trivial K3/triangle instances with more interesting graphs: - kcoloring_to_ilp: Petersen graph (10v, 15e) with ILPSolver - kcoloring_to_qubo: house graph (5v, 6e) to keep BruteForce feasible - maxcut_to_spinglass: Petersen graph (10v, 15e) with unit weights Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace trivial 3-set instances with richer 6-set instances over 8 elements in SetPacking (QUBO and ILP) and SetCovering (ILP) examples. The new instances have interesting overlap structure and produce max packing size 2 and min cover size 3. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace trivial 2-3 variable SAT formulas with richer 5-variable instances across 4 SAT reduction examples: - sat_to_mis: 5-var, 7-clause 3-SAT (21 vertices, fast BruteForce) - sat_to_coloring: 5-var, 3 unit clauses (13 vertices; OR-gadgets make multi-literal clauses infeasible for BruteForce on 3-coloring) - sat_to_mds: 5-var, 7-clause 3-SAT (22 vertices, fast BruteForce) - sat_to_ksat: 5-var, 6-clause mixed sizes (1,2,3,3,4,5 literals) to demonstrate both padding and splitting transformations Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Generalize the KSatisfiability-to-QUBO reduction to support K=3 using Rosenberg quadratization (one auxiliary variable per 3-literal clause). Update the example from a trivial 2-SAT/3-variable instance to a 3-SAT instance with 5 variables and 7 clauses, producing a 12-variable QUBO (5 original + 7 auxiliary). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace trivial 3-spin/3-variable instances with 10-variable Petersen graph instances for SpinGlass-QUBO and SpinGlass-MaxCut reductions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Improved Example Instances — Tasks 1–10 CompleteImplemented the first 10 tasks from the improvement plan. All 27 example files across tasks 1–10 have been updated with non-trivial instances. Summary of Changes
Notable Implementation Details
Verification
Remaining (Tasks 11–13)Tasks 11 (CircuitSAT), 12 (Factoring), and 13 (JSON regeneration) are not included in this batch. 🤖 Generated with Claude Code |
Contributor
Author
|
[action] implement the next batch of 10 examples refactor. |
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Batch 3: Tasks 11-13 completedTask 11: CircuitSAT → SpinGlass (
|
GiggleLiu
commented
Feb 11, 2026
| /// Result of reducing KSatisfiability<3> to QUBO. | ||
| #[derive(Debug, Clone)] | ||
| pub struct ReductionK3SatToQUBO { | ||
| target: QUBO<f64>, |
Contributor
Author
There was a problem hiding this comment.
Should not it be 3SAT rather than K3Sat?
| //! - (x_i ∨ ¬x_j): penalty (1-x_i)x_j → Q[j][j]+=1, Q[i][j]-=1 | ||
| //! - (¬x_i ∨ ¬x_j): penalty x_i·x_j → Q[i][j]+=1 | ||
| //! | ||
| //! For K≥3, we use the Rosenberg quadratization to reduce degree-K penalty terms |
Contributor
Author
There was a problem hiding this comment.
Describe this in detail in reductions.typ
There was a problem hiding this comment.
Pull request overview
This PR updates example instances across all 30 reduction examples, replacing trivial test cases with non-trivial ones to generate better demonstration data. The PR includes significant code changes beyond just documentation updates:
Changes:
- Implements new K=3 SAT to QUBO reduction using Rosenberg quadratization with auxiliary variables
- Updates 24 example files to use Petersen graph (10 vertices, 15 edges) instead of trivial graphs (K3, P4, etc.)
- Updates SAT examples to use 5-variable, 7-clause formulas instead of 2-3 variable formulas
- Adds interactive reduction graph visualization documentation
- Switches from BruteForce to ILPSolver where appropriate for performance
Reviewed changes
Copilot reviewed 36 out of 36 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/rules/ksatisfiability_qubo.rs | Implements K=3 SAT to QUBO reduction with Rosenberg quadratization, introduces auxiliary variables, updates extract_solution |
| src/unit_tests/rules/ksatisfiability_qubo.rs | Adds comprehensive tests for 3-SAT reduction including closed-loop, single clause, and all-negated cases |
| src/rules/mod.rs | Exports new ReductionK3SatToQUBO type |
| examples/reduction_spinglass_to_*.rs | Updates SpinGlass examples to use Petersen graph with frustrated ±1 couplings |
| examples/reduction_satisfiability_to_*.rs | Updates SAT examples to use 5-variable, 7-clause 3-SAT formulas |
| examples/reduction_to.rs (graph-based) | Updates graph examples to use Petersen or House graphs depending on performance constraints |
| examples/reduction_*_to_ilp.rs | Switches several examples from BruteForce to ILPSolver for better performance on larger instances |
| examples/reduction_ilp_to_qubo.rs | Replaces 3-variable project selection with 6-variable knapsack problem |
| examples/reduction_factoring_to_*.rs | Updates from factoring 15 (4-bit) to factoring 35 (3-bit) |
| examples/reduction_maximumsetpacking_to_*.rs | Updates from 3 sets to 6 sets with more complex overlap patterns |
| examples/reduction_kcoloring_to_*.rs | Uses House graph (5 vertices) for QUBO to keep BruteForce feasible, uses Petersen for ILP with ILPSolver |
| examples/reduction_satisfiability_to_kcoloring.rs | Uses unit clauses to avoid OR-gadget vertex explosion |
| examples/reduction_circuitsat_to_spinglass.rs | Updates from simple AND gate to 1-bit full adder circuit |
| docs/src/reductions/graph.md | Adds interactive Cytoscape-based reduction graph visualization |
| docs/src/SUMMARY.md | Adds Reduction Graph section to documentation |
| docs/plans/2026-02-10-improve-example-instances-impl.md | Updates plan title to v2 |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+1
to
15
| //! Reduction from KSatisfiability to QUBO (Max-K-SAT). | ||
| //! | ||
| //! Each clause contributes to Q based on literal signs: | ||
| //! For K=2 (quadratic penalty), each clause contributes to Q based on literal signs: | ||
| //! - (x_i ∨ x_j): penalty (1-x_i)(1-x_j) → Q[i][i]-=1, Q[j][j]-=1, Q[i][j]+=1, const+=1 | ||
| //! - (¬x_i ∨ x_j): penalty x_i(1-x_j) → Q[i][i]+=1, Q[i][j]-=1 | ||
| //! - (x_i ∨ ¬x_j): penalty (1-x_i)x_j → Q[j][j]+=1, Q[i][j]-=1 | ||
| //! - (¬x_i ∨ ¬x_j): penalty x_i·x_j → Q[i][j]+=1 | ||
| //! | ||
| //! For K≥3, we use the Rosenberg quadratization to reduce degree-K penalty terms | ||
| //! to quadratic form by introducing auxiliary variables. Each clause of K literals | ||
| //! requires K−2 auxiliary variables. | ||
| //! | ||
| //! CNFClause uses 1-indexed signed integers: positive = variable, negative = negated. | ||
|
|
||
| use crate::models::optimization::QUBO; |
There was a problem hiding this comment.
The PR description states "No code changes; documentation only" in the test plan, but this PR contains significant code changes including:
- New K=3 SAT to QUBO reduction implementation with Rosenberg quadratization
- New unit tests for the 3-SAT reduction
- Modified extract_solution to handle auxiliary variables
- New reduction result type ReductionK3SatToQUBO
- Export updates in mod.rs
The PR description should be updated to accurately reflect that this includes both code changes and documentation updates.
Contributor
Author
|
[fix] |
- Remove interactive reduction graph page (docs/src/reductions/graph.md) - Remove Reductions section from SUMMARY.md - Rename ReductionK3SatToQUBO to Reduction3SATToQUBO - Document 3-SAT→QUBO Rosenberg quadratization in reductions.typ - Update PR description to reflect code changes Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Review Feedback AddressedAll review comments have been fixed in commit 96b1736:
Verification
🤖 Generated with Claude Code |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Test plan
make test— all tests passmake clippy— no warnings🤖 Generated with Claude Code