feat: batch implement 17 reduction rules with 14 new models#999
Merged
feat: batch implement 17 reduction rules with 14 new models#999
Conversation
Implements the classical padding reduction from Garey & Johnson (SP12-SP13). Handles all three cases: Σ=2T (no padding), Σ>2T (same-side extraction), and Σ<2T (opposite-side extraction). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…868) Adds the NonTautology (DNF falsifiability) model with Value=Or, and the De Morgan negation reduction from Satisfiability. Each CNF clause becomes a DNF disjunct with flipped literal signs; solution extraction is identity. Includes CLI/MCP support for NonTautology creation and example-db hooks. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ques rule (#844) Adds the PartitionIntoCliques graph model (Value=Or, partitions vertices into K cliques) and the complement-graph reduction from KColoring. Color classes in G become cliques in the complement graph. Includes CLI support, example-db entries, paper documentation, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds the Kernel model for directed graphs (Value=Or, independent + absorbing vertex set) and Chvátal's 1973 reduction from KSatisfiability<K3>. Variable digons encode truth assignments; directed 3-cycles with connection arcs enforce clause satisfaction via the absorption property. Includes CLI support, example-db entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…#911) Adds DegreeConstrainedSpanningTree graph model (Value=Or, edge-selection configs checked for spanning tree + degree bound) and the identity reduction from HamiltonianPath with K=2. A degree-2 spanning tree is exactly a Hamiltonian path. Includes CLI support, example-db entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds the SetSplitting (hypergraph 2-colorability) model with Value=Or, and the reduction from NAESatisfiability. Uses two elements per variable (positive/negative literal) with pairing subsets to enforce complementary assignment, plus one subset per clause to enforce non-monochromatic NAE. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds SubsetProduct model (Value=Or, binary subset selection with product check) and the prime-encoding reduction from ExactCoverBy3Sets. Each universe element gets a distinct prime; each 3-set maps to the product of its elements' primes. By FTA, subset product equals universe product iff the selected sets form an exact cover. Includes CLI support and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…569) Adds IntegerExpressionMembership (pick-one-per-position sum check with Value=Or) and the shift-encoding reduction from SubsetSum. Each element a_i creates choice set {1, a_i+1}; target K = B + n. Picking a_i+1 means "include element"; sum equals K iff selected elements sum to B. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…E rule (#860) Adds MWSLE algebraic model (Value=Or, binary variables with linear equation check + sparsity bound) and the incidence-matrix reduction from ExactCoverBy3Sets. One variable per 3-set, one equation per universe element, bound K = |U|/3. Exact cover iff equation system has K-sparse solution. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds SimultaneousIncongruences algebraic model (Value=Or, find x in [1..N] satisfying all x mod m_i != r_i) and the CRT-based reduction from KSatisfiability<K3>. Each variable gets a distinct odd prime, residues 1/2 encode true/false, other residues are forbidden, and each clause adds one CRT-derived forbidden residue. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…MTTW rule (#471) Adds SequencingToMinimizeTardyTaskWeight model (Value=Min<u64>, Lehmer-coded permutation schedules) and the common-deadline reduction from Partition. Each element becomes a task with length=weight=size and deadline=B/2. On-time tasks decode one partition half. Includes CLI support and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds OpenShopScheduling model (Value=Min<u64>, Lehmer-coded permutation schedules with active-schedule decoder) and the Gonzalez-Sahni 1976 reduction from Partition. Uses 3 machines with a special Q-job; makespan ≤3Q iff balanced partition exists. Includes CLI support and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Implements the Garey-Johnson-Stockmeyer 1976 reduction. Variable edges with weight M=2m+1 force complementary partition; clause triangles with unit weights contribute exactly 2 cut edges per NAE-satisfied clause. Max cut ≥ nM+2m iff NAE-satisfiable. Includes paper entry, canonical example, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds IsomorphicSpanningTree graph model (Value=Or, permutation-based isomorphism check) and the identity reduction from HamiltonianPath with tree T=P_n. A spanning tree isomorphic to a path is exactly a Hamiltonian path. Includes CLI support, updated ILP rule, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds AlgebraicEquationsOverGF2 model (Value=Or, polynomial system over GF(2) with XOR/AND evaluation) and the Fraenkel-Yesha 1977 reduction from ExactCoverBy3Sets. Linear equations enforce odd-cover per element; pairwise product equations forbid double-cover. Together they force exactly-one cover. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds ProductionPlanning model (Value=Or, lot-sizing with setup/production/ inventory costs and a total cost bound) and the Lenstra-Rinnooy Kan-Florian 1978 reduction from Partition. Element items map to production periods; a terminal demand period consumes S/2; balanced partition iff feasible production plan within cost bound. Includes CLI support, paper entries, and tests. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
# Conflicts: # docs/paper/reductions.typ # problemreductions-cli/src/cli.rs # problemreductions-cli/src/commands/create.rs # problemreductions-cli/src/problem_name.rs # src/lib.rs # src/models/algebraic/algebraic_equations_over_gf2.rs # src/models/algebraic/minimum_weight_solution_to_linear_equations.rs # src/models/algebraic/mod.rs # src/models/algebraic/simultaneous_incongruences.rs # src/models/formula/mod.rs # src/models/formula/non_tautology.rs # src/models/graph/degree_constrained_spanning_tree.rs # src/models/graph/kernel.rs # src/models/graph/mod.rs # src/models/graph/partition_into_cliques.rs # src/models/misc/mod.rs # src/models/misc/open_shop_scheduling.rs # src/models/misc/production_planning.rs # src/models/misc/sequencing_to_minimize_tardy_task_weight.rs # src/models/misc/subset_product.rs # src/models/mod.rs # src/models/set/mod.rs # src/models/set/set_splitting.rs # src/rules/hamiltonianpath_isomorphicspanningtree.rs # src/rules/mod.rs # src/rules/naesatisfiability_maxcut.rs # src/unit_tests/models/algebraic/algebraic_equations_over_gf2.rs # src/unit_tests/models/algebraic/minimum_weight_solution_to_linear_equations.rs # src/unit_tests/models/algebraic/simultaneous_incongruences.rs # src/unit_tests/models/formula/non_tautology.rs # src/unit_tests/models/graph/degree_constrained_spanning_tree.rs # src/unit_tests/models/graph/kernel.rs # src/unit_tests/models/graph/partition_into_cliques.rs # src/unit_tests/models/misc/open_shop_scheduling.rs # src/unit_tests/models/misc/production_planning.rs # src/unit_tests/models/misc/sequencing_to_minimize_tardy_task_weight.rs # src/unit_tests/models/misc/subset_product.rs # src/unit_tests/models/set/set_splitting.rs # src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs # src/unit_tests/rules/naesatisfiability_maxcut.rs
…ule (#359) Copy graph with unit edge weights and same s/t vertices. A Hamiltonian s-t path has n-1 edges = maximum possible simple path length. Solution extraction walks selected edges from source to reconstruct the vertex permutation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #999 +/- ##
==========================================
+ Coverage 98.12% 98.15% +0.03%
==========================================
Files 858 896 +38
Lines 89004 91150 +2146
==========================================
+ Hits 87338 89472 +2134
- Misses 1666 1678 +12 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
These were working files from the batch implementation session, not intended for the repository. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds guidance to consult GitHub issues and derivation documents as primary sources for mathematical content, rather than inventing proofs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…mands Each reduction-rule entry now includes: - load-example data bindings and example: true parameter - Complexity citation (@garey1979, @karp1972, etc.) - Worked example with pred-commands() reproducibility block - Step-by-step verification using fixture data Fixed entry #13 (NAE-SAT → MaxCut): proper @citation. Fixed entry #18 (GraphPartitioning → MaxCut): completed proof replacing $= dots$ placeholder with full derivation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The inventory-based registry resolution is non-deterministic across platforms. On CI, "GraphPartitioning" was resolving to "MaxCut" due to registration order, causing test_create_graph_partitioning to fail. Add explicit case-insensitive resolution, matching the pattern used for other ambiguous problem names. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…phPartitioning) - KSatisfiability → Kernel: corrected arc count to 2n+6m, rewrote proof to allow clause vertices in kernel matching the actual code - NAESatisfiability → MaxCut: corrected M = m+1 (was 2m+1), fixed example - GraphPartitioning → MaxCut: completed balance proof via P=|E|+1 penalty All examples now use load-example() fixture data with pred-commands(). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…step verification Expanded worked examples for: NAE-SAT→SetSplitting, X3C→SubsetProduct, SubsetSum→IntegerExprMembership, X3C→MWSLE, 3SAT→SimultaneousIncongruences, Partition→SeqMinTardyTaskWeight, Partition→OpenShopScheduling, X3C→AlgEqOverGF2, Partition→ProductionPlanning. Each example now shows construction with actual numbers from load-example() fixtures and step-by-step witness verification. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
1 participant
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
Batch implementation of 17 reduction rules (16 from the original high-confidence batch + #359 after merge) and 14 new problem models. Three rules (#379, #380) are blocked pending a Decision wrapper model (tracked in #998).
All passing
make check(fmt + clippy + tests).Implemented Rules
Blocked Rules
Tracked in #998.
Additional Context
Ga >= 1validationTest plan
make checkpasses (fmt + clippy + 4814+ tests)🤖 Generated with Claude Code