* feat: add SubsetSum → Partition reduction rule (#973) 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> * feat: add NonTautology model and Satisfiability → NonTautology rule (#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> * feat: add PartitionIntoCliques model and KColoring → PartitionIntoCliques 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> * feat: add Kernel model and 3SAT → Kernel reduction rule (#882) 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> * feat: add DegreeConstrainedSpanningTree model and HamPath → DCST rule (#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> * feat: add SetSplitting model and NAE-SAT → SetSplitting rule (#382) 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> * feat: add SubsetProduct model and X3C → SubsetProduct rule (#388) 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> * feat: add IntegerExpressionMembership model and SubsetSum → IEM rule (#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> * feat: add MinimumWeightSolutionToLinearEquations model and X3C → MWSLE 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> * feat: add SimultaneousIncongruences model and 3SAT → SI rule (#554) 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> * feat: add SequencingToMinimizeTardyTaskWeight model and Partition → SMTTW 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> * feat: add OpenShopScheduling model and Partition → OSS rule (#481) 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> * feat: add NAESatisfiability → MaxCut reduction rule (#166) 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> * feat: add IsomorphicSpanningTree model and HamPath → IST rule (#912) 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> * feat: add AlgebraicEquationsOverGF2 model and X3C → AEGF2 rule (#859) 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> * feat: add ProductionPlanning model and Partition → PP rule (#488) 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> * feat: add HamiltonianPathBetweenTwoVertices → LongestPath reduction rule (#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> * chore: remove stray prompt.md and implementation_log.md 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> * fix: address PR #999 review issues * update rules note * docs: add Source Material section to write-rule-in-paper skill 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> * docs: augment 18 paper entries with examples, citations, and pred-commands 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> * fix: add explicit GraphPartitioning name resolution for CI determinism 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> * fix: align 3 paper entries with implemented code (Kernel, MaxCut, GraphPartitioning) - 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> * docs: expand 9 paper examples with concrete fixture data and step-by-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> --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Convert a problem to QUBO problem #18

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions