feat: add QUBO→ILP and CircuitSAT→ILP reductions#85
Conversation
Addresses issue #83 — adds ILP reduction paths for QUBO, SpinGlass, MaxCut, and CircuitSAT. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #85 +/- ##
==========================================
- Coverage 96.35% 96.33% -0.02%
==========================================
Files 193 197 +4
Lines 26722 27037 +315
==========================================
+ Hits 25747 26047 +300
- Misses 975 990 +15 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Implement reduction from QUBO to ILP using McCormick linearization for binary quadratic terms. Diagonal Q_ii terms become linear x_i terms, and each non-zero off-diagonal Q_ij (i<j) introduces an auxiliary variable y_ij with three McCormick constraints enforcing y_ij = x_i * x_j. Closes the ILP path for QUBO, SpinGlass, and MaxCut (issue #83). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Direct 1-step path, more efficient than CircuitSAT→SpinGlass→QUBO→ILP (issue #83). Fix XOR test: CircuitSAT `c = x XOR y` constrains c == (x XOR y) for all variable assignments (4 solutions), not just c=true (2 solutions).
GiggleLiu
left a comment
There was a problem hiding this comment.
- clean up plan files
- update all documents
There was a problem hiding this comment.
Pull request overview
This pull request adds two new reduction rules to enable all problem types to reach ILP, addressing issue #83:
- QUBO → ILP via McCormick linearization of quadratic binary terms
- CircuitSAT → ILP via Tseitin-style gate constraint encoding
Both reductions are feature-gated behind the ilp-solver feature and follow established patterns in the codebase.
Changes:
- Add QUBO→ILP reduction with McCormick linearization for binary products
- Add CircuitSAT→ILP reduction with linear constraint encodings for boolean gates
- Disambiguate
reduce_to()calls in existing CircuitSAT→SpinGlass tests to avoid type inference conflicts - Add comprehensive unit tests for both new reductions
Reviewed changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| src/rules/qubo_ilp.rs | QUBO→ILP reduction implementation using McCormick constraints for quadratic term linearization |
| src/unit_tests/rules/qubo_ilp.rs | Three unit tests covering closed-loop verification, diagonal-only case, and 3-variable case |
| src/rules/circuit_ilp.rs | CircuitSAT→ILP reduction with gate-specific linear constraint encodings (NOT, AND, OR, XOR, Const) |
| src/unit_tests/rules/circuit_ilp.rs | Five unit tests covering AND, OR, XOR, nested expressions, and multi-assignment circuits |
| src/rules/mod.rs | Module registration for both new reductions under ilp-solver feature flag |
| src/unit_tests/rules/circuit_spinglass.rs | Explicit type annotations to disambiguate reduce_to() calls after adding CircuitSAT→ILP |
| docs/plans/2026-02-18-ilp-reduction-paths-impl.md | Implementation plan document with step-by-step instructions |
| docs/plans/2026-02-18-ilp-reduction-paths-design.md | Design document explaining the reduction algorithms and mathematical formulations |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
…reductions - Remove plan files (docs/plans/2026-02-18-ilp-*) - Add reduction examples: reduction_qubo_to_ilp.rs (4-var McCormick) and reduction_circuitsat_to_ilp.rs (full adder gate encoding) - Add reduction-rule entries in paper (reductions.typ) with proofs - Regenerate reduction_graph.json with new edges - Register both examples in tests/suites/examples.rs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Summary
src/rules/qubo_ilp.rs)src/rules/circuit_ilp.rs)ilp-solverDetails
QUBO → ILP: Linearizes quadratic binary terms using McCormick envelope constraints. For each non-zero off-diagonal Q_ij, introduces an auxiliary binary variable y_ij = x_i · x_j with constraints y ≤ x_i, y ≤ x_j, y ≥ x_i + x_j - 1.
CircuitSAT → ILP: Encodes boolean gates as linear constraints over binary variables. NOT, AND, OR, XOR, and Const gates are each translated into tight linear constraint formulations. This provides a direct 1-step path, more efficient than the 3-step CircuitSAT→SpinGlass→QUBO→ILP route.
Test plan
-D warningsreduce_to()calls in existing CircuitSAT→SpinGlass tests🤖 Generated with Claude Code