diff --git a/.claude/skills/write-rule-in-paper/SKILL.md b/.claude/skills/write-rule-in-paper/SKILL.md index c10e52e43..0d9755b1b 100644 --- a/.claude/skills/write-rule-in-paper/SKILL.md +++ b/.claude/skills/write-rule-in-paper/SKILL.md @@ -21,6 +21,15 @@ Before using this skill, ensure: - If the canonical example changed, fixtures are regenerated (`make regenerate-fixtures`) - The reduction graph and schemas are up to date (`cargo run --example export_graph && cargo run --example export_schemas`) +## Source Material + +For mathematical content (theorems, proofs, examples), consult these sources in priority order: +1. **GitHub issue** for the rule (`gh issue view `): contains the verified reduction algorithm, correctness proof, size overhead, and worked examples written during issue creation +2. **Derivation documents** (if available): e.g., `~/Downloads/reduction_derivations_*.typ` — these contain batch-verified proofs with explicit theorem/proof blocks +3. **The implementation** (`src/rules/_.rs`): the code is the ground truth for the construction + +Do NOT invent proofs — always cross-check against the issue and derivation sources. The issue body typically has: Reduction Algorithm, Correctness (forward/backward), Size Overhead, Example, and References sections that map directly to the paper entry structure. + ## Step 1: Load Example Data ```typst diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 3ff1ba9d8..98fd3fbce 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -86,6 +86,7 @@ "MinimumVertexCover": [Minimum Vertex Cover], "MaxCut": [Max-Cut], "GeneralizedHex": [Generalized Hex], + "GraphPartitioning": [Graph Partitioning], "HamiltonianCircuit": [Hamiltonian Circuit], "BiconnectivityAugmentation": [Biconnectivity Augmentation], "HamiltonianPath": [Hamiltonian Path], @@ -707,6 +708,13 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| ] ] } +#problem-def("GraphPartitioning")[ + Given an undirected graph $G = (V, E)$ with $|V| = n$ (even), find a partition of $V$ into two disjoint sets $A$ and $B$ with $|A| = |B| = n\/2$ minimizing the number of crossing edges $|{(u,v) in E : u in A, v in B}|$. +][ +Graph Partitioning (Minimum Bisection, Garey & Johnson ND14) is the special case of Minimum Cut Into Bounded Sets with unit weights, $B = n\/2$, and no designated $s, t$ vertices. The problem is NP-hard even on 3-regular graphs @garey1976. + +The best known exact algorithm is brute-force enumeration over all balanced partitions in $O^*(2^n)$ time#footnote[No algorithm improving on brute-force enumeration is known for general Graph Partitioning.]. +] #problem-def("MinimumCutIntoBoundedSets")[ Given an undirected graph $G = (V, E)$ with edge weights $w: E -> ZZ^+$, designated vertices $s, t in V$, and a positive integer $B <= |V|$, find a partition of $V$ into disjoint sets $V_1$ and $V_2$ such that $s in V_1$, $t in V_2$, $|V_1| <= B$, $|V_2| <= B$, that minimizes the total cut weight $ sum_({u,v} in E: u in V_1, v in V_2) w({u,v}). $ @@ -13036,5 +13044,758 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ First $n$ variables (sign variables) give the source configuration. ] +// ── Batch of 18 reduction rules from derivation document ── + +// 1. SubsetSum → Partition (#973) +#let ss_part = load-example("SubsetSum", "Partition") +#let ss_part_sol = ss_part.solutions.at(0) +#reduction-rule("SubsetSum", "Partition", + example: true, + example-caption: [#subsetsum-num-elements(ss_part.source.instance) elements, target $T = #ss_part.source.instance.target$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ss_part.source) + " -o subsetsum.json", + "pred reduce subsetsum.json --to " + target-spec(ss_part) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate subsetsum.json --config " + ss_part_sol.source_config.map(str).join(","), + ) + + #{ + let sizes = ss_part.source.instance.sizes.map(s => int(s)) + let sigma = sizes.sum() + let T = int(ss_part.source.instance.target) + let d = calc.abs(sigma - 2 * T) + [ + *Step 1 -- Source instance.* Subset Sum with sizes $(#sizes.map(str).join(", "))$ and target $T = #T$. Total $Sigma = #sigma$. + + *Step 2 -- Compute padding.* $Sigma = #sigma$, $2T = #(2 * T)$. Since $Sigma < 2T$, we have $d = 2T - Sigma = #d$. The Partition instance is $S union {d} = (#ss_part.target.instance.sizes.map(str).join(", "))$ with #ss_part.target.instance.sizes.len() elements. + + *Step 3 -- Verify a solution.* Source config $(#ss_part_sol.source_config.map(str).join(", "))$: selected elements $= {#ss_part_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(sizes.at(i))).join(", ")}$ sum to $#T = T$ #sym.checkmark. Target config $(#ss_part_sol.target_config.map(str).join(", "))$: side-0 sum $= #ss_part_sol.target_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => ss_part.target.instance.sizes.at(i)).sum()$, side-1 sum $= #ss_part_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => ss_part.target.instance.sizes.at(i)).sum()$ -- balanced #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. Other valid subsets summing to $T$ may exist. + ], +)[ + This $O(n)$ reduction @garey1979 computes padding $d = |Sigma - 2T|$ and appends at most one element. A subset of $S$ sums to $T$ if and only if the padded multiset admits a balanced partition. +][ + _Construction._ Let $(S, T)$ be a Subset Sum instance with $n$ elements and $Sigma = sum_(i=1)^n s_i$. Compute $d = |Sigma - 2T|$. If $d = 0$, output Partition instance $S$. If $d > 0$, output $S union {d}$ (one extra element). Let $Sigma'$ denote the total of the Partition instance and $H = Sigma' \/ 2$. + + _Correctness._ There are three cases. + + *Case 1* ($Sigma = 2T$, $d = 0$): $H = T$. ($arrow.r.double$) A subset summing to $T = H$ is one half of a balanced partition. ($arrow.l.double$) A balanced partition yields a subset summing to $H = T$. + + *Case 2* ($Sigma > 2T$, $d = Sigma - 2T$): $Sigma' = 2(Sigma - T)$, $H = Sigma - T$. ($arrow.r.double$) If $A' subset.eq S$ sums to $T$, then $A' union {d}$ sums to $T + (Sigma - 2T) = H$. ($arrow.l.double$) In any balanced partition, the side containing $d$ has $S$-elements summing to $H - d = T$. + + *Case 3* ($Sigma < 2T$, $d = 2T - Sigma$): $Sigma' = 2T$, $H = T$. ($arrow.r.double$) A subset summing to $T = H$ gives one side directly. ($arrow.l.double$) The side opposite $d$ has $S$-elements summing to $H = T$. + + If $T > Sigma$, then $d > Sigma' \/ 2$, so a single element exceeds the half-sum and the Partition instance is infeasible. + + _Solution extraction._ Given a Partition solution $c in {0,1}^m$: if $d = 0$, return $c[0..n]$. If $Sigma > 2T$, the $S$-elements on the same side as the padding form the subset summing to $T$. If $Sigma < 2T$, the $S$-elements on the opposite side from the padding form the subset summing to $T$. +] + +// 2. Satisfiability → NonTautology (#868) +#let sat_nt = load-example("Satisfiability", "NonTautology") +#let sat_nt_sol = sat_nt.solutions.at(0) +#reduction-rule("Satisfiability", "NonTautology", + example: true, + example-caption: [$n = #sat_nt.source.instance.num_vars$ variables, $m = #sat-num-clauses(sat_nt.source.instance)$ clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(sat_nt.source) + " -o sat.json", + "pred reduce sat.json --to " + target-spec(sat_nt) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate sat.json --config " + sat_nt_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* CNF with $n = #sat_nt.source.instance.num_vars$ variables and $m = #sat-num-clauses(sat_nt.source.instance)$ clauses. + + *Step 2 -- Apply De Morgan.* Each clause $C_j = (l_1 or dots or l_k)$ becomes disjunct $D_j = (overline(l_1) and dots and overline(l_k))$. The Non-Tautology instance has #sat_nt.target.instance.disjuncts.len() disjuncts over #sat_nt.target.instance.num_vars variables. + + *Step 3 -- Verify a solution.* Source config $(#sat_nt_sol.source_config.map(str).join(", "))$ satisfies the CNF. Target config $(#sat_nt_sol.target_config.map(str).join(", "))$ falsifies the DNF (same assignment). Variables are identical #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n + m)$ reduction @garey1979 negates a CNF formula via De Morgan's laws to obtain a DNF formula $E = not phi$. The formula $phi$ is satisfiable if and only if $E$ is not a tautology. Variables, their count, and polarity are preserved; each clause becomes a disjunct of negated literals. +][ + _Construction._ Let $phi = C_1 and dots and C_m$ be a CNF formula over $n$ variables. For each clause $C_j = (l_1 or dots or l_k)$, form the disjunct $D_j = (overline(l_1) and dots and overline(l_k))$ where $overline(l)$ is the complement of literal $l$. The Non-Tautology instance is the DNF formula $E = D_1 or dots or D_m$. + + _Correctness._ ($arrow.r.double$) If $alpha models phi$, then $alpha$ makes every clause true, so $alpha models not E$ (since $E = not phi$), and $E$ has a falsifying assignment. ($arrow.l.double$) If $beta$ falsifies $E$, then $beta tack.r.not not phi$, so $beta models phi$ and $phi$ is satisfiable. + + _Solution extraction._ The falsifying assignment for $E$ is directly the satisfying assignment for $phi$ -- no transformation needed since the variables are identical. +] + +// 3. KColoring → PartitionIntoCliques (#844) +#let kc_pic = load-example("KColoring", "PartitionIntoCliques") +#let kc_pic_sol = kc_pic.solutions.at(0) +#reduction-rule("KColoring", "PartitionIntoCliques", + example: true, + example-caption: [$n = #graph-num-vertices(kc_pic.source.instance)$ vertices, $k = #kc_pic.source.instance.num_colors$ colors], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(kc_pic.source) + " -o kcoloring.json", + "pred reduce kcoloring.json --to " + target-spec(kc_pic) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate kcoloring.json --config " + kc_pic_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* Graph $G$ with $n = #graph-num-vertices(kc_pic.source.instance)$ vertices, $|E| = #graph-num-edges(kc_pic.source.instance)$ edges, $k = #kc_pic.source.instance.num_colors$ colors. + + *Step 2 -- Complement graph.* $overline(G)$ has the same $n = #graph-num-vertices(kc_pic.target.instance)$ vertices and $|overline(E)| = #graph-num-edges(kc_pic.target.instance)$ edges. Clique bound $K' = #kc_pic.target.instance.num_cliques$. + + *Step 3 -- Verify a solution.* Source coloring $(#kc_pic_sol.source_config.map(str).join(", "))$. Target partition $(#kc_pic_sol.target_config.map(str).join(", "))$ -- each color class is a clique in $overline(G)$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n^2)$ reduction @karp1972 computes the complement graph $overline(G)$ and sets the clique bound $K' = K$. A proper $K$-coloring of $G$ exists if and only if $overline(G)$ can be partitioned into at most $K'$ cliques, because color classes (independent sets in $G$) correspond to cliques in $overline(G)$. +][ + _Construction._ Given $K$-Coloring instance $(G = (V, E), K)$, compute $overline(G) = (V, overline(E))$ where $overline(E) = {{u, v} : u != v, {u,v} in.not E}$. Set $K' = K$. Output Partition Into Cliques instance $(overline(G), K')$. + + _Correctness._ ($arrow.r.double$) If $c : V -> {0, dots, K-1}$ is a proper coloring, define $V_i = {v : c(v) = i}$. For $u, v in V_i$, $c(u) = c(v)$ implies ${u,v} in.not E$, so ${u,v} in overline(E)$, making $V_i$ a clique in $overline(G)$. The $K$ color classes partition $V$ into at most $K' = K$ cliques. ($arrow.l.double$) If $V_0, dots, V_(k-1)$ is a partition of $overline(G)$ into $k <= K'$ cliques, then each $V_i$ is an independent set in $G$. Assigning color $i$ to all vertices in $V_i$ gives a proper $k$-coloring of $G$. + + _Solution extraction._ Given a partition $V_0, dots, V_(k-1)$ into cliques, assign color $i$ to every vertex in $V_i$. +] + +// 4. KSatisfiability → Kernel (#882) +#let ksat_ker = load-example("KSatisfiability", "Kernel") +#let ksat_ker_sol = ksat_ker.solutions.at(0) +#reduction-rule("KSatisfiability", "Kernel", + example: true, + example-caption: [$n = #ksat_ker.source.instance.num_vars$ variables, $m = #sat-num-clauses(ksat_ker.source.instance)$ clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ksat_ker.source) + " -o ksat.json", + "pred reduce ksat.json --to " + target-spec(ksat_ker) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate ksat.json --config " + ksat_ker_sol.source_config.map(str).join(","), + ) + + #{ + let n = ksat_ker.source.instance.num_vars + let m = sat-num-clauses(ksat_ker.source.instance) + let selected = ksat_ker_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) + let literal-selected = selected.filter(v => v < 2 * n) + let clause-selected = selected.filter(v => v >= 2 * n) + let second-clause-base = 2 * n + 3 + let last-literal-vertex = literal-selected.at(literal-selected.len() - 1) + [ + *Step 1 -- Source instance.* 3-SAT with $n = #n$ variables and $m = #m$ clauses. The canonical satisfying assignment is $(#ksat_ker_sol.source_config.map(str).join(", "))$. + + *Step 2 -- Construct the digraph.* Variable gadgets contribute $2n = #(2 * n)$ literal vertices and $2n = #(2 * n)$ digon arcs. Clause gadgets contribute $3m = #(3 * m)$ clause vertices, $3m = #(3 * m)$ cycle arcs, and $3m = #(3 * m)$ literal arcs. Total: $#ksat_ker.target.instance.graph.num_vertices$ vertices and $#ksat_ker.target.instance.graph.arcs.len()$ arcs $= 2n + 6m$. + + *Step 3 -- Verify the canonical witness.* The target kernel selects literal vertices ${#literal-selected.map(str).join(", ")}$ and clause vertices ${#clause-selected.map(str).join(", ")}$. Here ${#literal-selected.map(str).join(", ")}$ encode $(x_1, x_2, x_3) = (#ksat_ker_sol.source_config.map(str).join(", "))$, and the extra clause vertex $#(second-clause-base + 1)$ is needed in the second clause gadget: vertex $#second-clause-base$ is absorbed by arc $(#second-clause-base, #(second-clause-base + 1))$, while vertex $#(second-clause-base + 2)$ is absorbed by its literal arc to vertex $#last-literal-vertex$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n + m)$ reduction @garey1979 constructs a directed graph with $2n + 3m$ vertices and $2n + 6m$ arcs. Each variable contributes a digon on its positive and negative literal vertices, and each 3-clause contributes a directed 3-cycle whose three clause vertices point to the corresponding literal vertices. The implemented kernels may contain clause vertices as well as literal vertices. +][ + _Construction._ Let $phi = C_1 and dots and C_m$ be a 3-SAT instance on variables $x_1, dots, x_n$. For each variable $x_i$, create two literal vertices $p_i$ and $n_i$ with arcs $(p_i, n_i)$ and $(n_i, p_i)$. For each clause $C_j = (ell_(j,0) or ell_(j,1) or ell_(j,2))$, create clause vertices $c_(j,0), c_(j,1), c_(j,2)$ with cycle arcs $(c_(j,0), c_(j,1))$, $(c_(j,1), c_(j,2))$, and $(c_(j,2), c_(j,0))$. Add one literal arc $(c_(j,t), v(ell_(j,t)))$ from each clause vertex to the literal vertex representing its own literal. Thus each clause contributes 3 cycle arcs and 3 literal arcs, for a total of $2n + 6m$ arcs. + + _Correctness._ ($arrow.r.double$) Let $alpha$ be a satisfying assignment. Put into $K$ exactly one literal vertex from each digon: $p_i$ if $alpha(x_i) = "true"$ and $n_i$ otherwise. For each clause $C_j$, additionally put $c_(j,t)$ into $K$ exactly when $ell_(j,t)$ is false and $ell_(j,(t+1) mod 3)$ is true. This never creates an arc inside $K$: each selected clause vertex points to a false literal vertex, and two adjacent clause vertices cannot both satisfy the selection rule. Every unselected literal vertex is absorbed by its digon partner. For an unselected clause vertex $c_(j,t)$, either $ell_(j,t)$ is true, so its literal arc hits the selected literal vertex, or $ell_(j,t)$ is false. In the latter case $c_(j,t)$ was not selected, so $ell_(j,(t+1) mod 3)$ is also false; because the clause is satisfied, $ell_(j,(t+2) mod 3)$ is true, hence $c_(j,(t+1) mod 3)$ was selected and absorbs $c_(j,t)$ along the cycle. + + ($arrow.l.double$) Let $K$ be a kernel of the constructed digraph. In each variable digon, at most one literal vertex can lie in $K$ by independence, and at least one must lie in $K$ to absorb the other endpoint; so each digon contributes exactly one selected literal vertex. Set $alpha(x_i) = "true"$ iff $p_i in K$. Now fix a clause gadget with cycle $(c_(j,0), c_(j,1), c_(j,2))$. If none of its three literal vertices were selected, then the only possible absorbers for $c_(j,0), c_(j,1), c_(j,2)$ would be the cycle successors. Independence allows at most one clause vertex in $K$, but one selected vertex on a directed 3-cycle cannot absorb the other two, contradiction. Therefore every clause has at least one selected literal vertex, so $alpha$ satisfies every clause. + + _Solution extraction._ Read only the positive literal vertices: $alpha(x_i) = 1$ iff the even-indexed vertex for $x_i$ is in the kernel. Any selected clause vertices are ignored during extraction. +] + +// 5. HamiltonianPath → DegreeConstrainedSpanningTree (#911) +#let hp_dcst = load-example("HamiltonianPath", "DegreeConstrainedSpanningTree") +#let hp_dcst_sol = hp_dcst.solutions.at(0) +#reduction-rule("HamiltonianPath", "DegreeConstrainedSpanningTree", + example: true, + example-caption: [$n = #graph-num-vertices(hp_dcst.source.instance)$ vertices, $K = 2$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(hp_dcst.source) + " -o hampath.json", + "pred reduce hampath.json --to " + target-spec(hp_dcst) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate hampath.json --config " + hp_dcst_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* Graph $G$ with $n = #graph-num-vertices(hp_dcst.source.instance)$ vertices and $|E| = #graph-num-edges(hp_dcst.source.instance)$ edges. + + *Step 2 -- Identity reduction.* Target graph is identical: $n = #graph-num-vertices(hp_dcst.target.instance)$ vertices, $|E| = #graph-num-edges(hp_dcst.target.instance)$ edges, degree bound $K = #hp_dcst.target.instance.max_degree$. + + *Step 3 -- Verify a solution.* Hamiltonian path visits vertices in order $(#hp_dcst_sol.source_config.map(str).join(", "))$. The corresponding spanning tree selects #hp_dcst_sol.target_config.filter(x => x == 1).len() edges (all with max degree $<= 2$) #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n + m)$ reduction @garey1979 passes the graph through unchanged and sets the degree bound $K = 2$. A Hamiltonian path is a spanning tree with maximum degree 2 (a path), and conversely any degree-2 spanning tree is a Hamiltonian path. The reduction is size-preserving. +][ + _Construction._ Given Hamiltonian Path instance $G = (V, E)$, output Degree-Constrained Spanning Tree instance $(G, K = 2)$. + + _Correctness._ ($arrow.r.double$) A Hamiltonian path $v_0, v_1, dots, v_(n-1)$ uses $n - 1$ edges spanning all vertices. Interior vertices have degree 2, endpoints have degree 1, so max degree $<= 2 = K$. ($arrow.l.double$) A spanning tree with max degree $<= 2$ has no branching (a branch point requires degree $>= 3$). A connected acyclic graph without branching is a simple path. Since the tree spans all $n$ vertices, it is a Hamiltonian path. + + _Solution extraction._ Collect the selected edges, find an endpoint (degree 1 vertex), walk the path to produce the vertex permutation. +] + +// 6. NAESatisfiability → SetSplitting (#382) +#let nae_ss = load-example("NAESatisfiability", "SetSplitting") +#let nae_ss_sol = nae_ss.solutions.at(0) +#reduction-rule("NAESatisfiability", "SetSplitting", + example: true, + example-caption: [$n = #nae_ss.source.instance.num_vars$ variables, $m = #sat-num-clauses(nae_ss.source.instance)$ clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(nae_ss.source) + " -o naesat.json", + "pred reduce naesat.json --to " + target-spec(nae_ss) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate naesat.json --config " + nae_ss_sol.source_config.map(str).join(","), + ) + + #{ + let colors = nae_ss_sol.target_config + [ + *Step 1 -- Source instance.* The fixture has clauses $C_1 = (x_1 or overline(x_2) or x_3)$ and $C_2 = (overline(x_1) or x_2 or overline(x_3))$. The canonical NAE assignment is $(#nae_ss_sol.source_config.map(str).join(", "))$, so the two clauses evaluate to $(1, 0, 1)$ and $(0, 1, 0)$ respectively. + + *Step 2 -- Build the universe and complementarity subsets.* The reduction creates $U = {0, dots, #(nae_ss.target.instance.universe_size - 1)}$ with positive literals on $\{0, 1, 2\}$ and negative literals on $\{3, 4, 5\}$. The first three target subsets are $R_1 = {#nae_ss.target.instance.subsets.at(0).map(str).join(", ")}$, $R_2 = {#nae_ss.target.instance.subsets.at(1).map(str).join(", ")}$, and $R_3 = {#nae_ss.target.instance.subsets.at(2).map(str).join(", ")}$. + + *Step 3 -- Encode the clauses as set-splitting constraints.* Clause $C_1$ becomes $T_1 = {#nae_ss.target.instance.subsets.at(3).map(str).join(", ")}$, and clause $C_2$ becomes $T_2 = {#nae_ss.target.instance.subsets.at(4).map(str).join(", ")}$. Under the target coloring $(#colors.map(str).join(", "))$, $T_1$ receives colors $(#colors.at(0), #colors.at(4), #colors.at(2))$ and $T_2$ receives $(#colors.at(3), #colors.at(1), #colors.at(5))$, so both subsets are non-monochromatic. + + *Step 4 -- Verify the witness pair.* Every complementarity pair has opposite colors: $(0, 3)$ gives $(#colors.at(0), #colors.at(3))$, $(1, 4)$ gives $(#colors.at(1), #colors.at(4))$, and $(2, 5)$ gives $(#colors.at(2), #colors.at(5))$. Reading the positive-literal colors $(#colors.at(0), #colors.at(1), #colors.at(2))$ recovers the source assignment $(#nae_ss_sol.source_config.map(str).join(", "))$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n + m)$ reduction @garey1979 maps each variable $x_(i+1)$ to two universe elements ($2i$ for positive, $2i+1$ for negative literal). Complementarity subsets ${2i, 2i+1}$ force opposite colors, and each clause becomes a subset of the corresponding literal elements. A NAE-satisfying assignment exists if and only if the Set Splitting instance admits a valid 2-coloring. +][ + _Construction._ Given NAE-SAT with $n$ variables and $m$ clauses, define universe $U = {0, 1, dots, 2n - 1}$. For each variable $x_(i+1)$, create complementarity subset $R_i = {2i, 2i+1}$. For each clause $C_j$, create subset $T_j$ containing element $2(k-1)$ for positive literal $x_k$ and $2(k-1)+1$ for negative literal $overline(x)_k$. Total: $|U| = 2n$, $n + m$ subsets. + + _Correctness._ ($arrow.r.double$) A NAE-satisfying assignment $alpha$ induces 2-coloring $chi(2i) = alpha(x_(i+1))$, $chi(2i+1) = 1 - alpha(x_(i+1))$. Complementarity subsets are non-monochromatic by construction. Clause subsets are non-monochromatic because NAE ensures both true and false literals. ($arrow.l.double$) A valid 2-coloring with $chi(2i) != chi(2i+1)$ (forced by $R_i$) defines $alpha(x_(i+1)) = chi(2i)$. Non-monochromaticity of clause subsets ensures both true and false literals in each clause. + + _Solution extraction._ Set $alpha(x_(i+1)) = chi(2i)$ for $i = 0, dots, n-1$. +] + +// 7. ExactCoverBy3Sets → SubsetProduct (#388) +#let x3c_sp = load-example("ExactCoverBy3Sets", "SubsetProduct") +#let x3c_sp_sol = x3c_sp.solutions.at(0) +#reduction-rule("ExactCoverBy3Sets", "SubsetProduct", + example: true, + example-caption: [$|U| = #x3c_sp.source.instance.universe_size$, $|cal(C)| = #x3c_sp.source.instance.subsets.len()$ subsets], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(x3c_sp.source) + " -o x3c.json", + "pred reduce x3c.json --to " + target-spec(x3c_sp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate x3c.json --config " + x3c_sp_sol.source_config.map(str).join(","), + ) + + #{ + let sizes = x3c_sp.target.instance.sizes + [ + *Step 1 -- Source instance.* The fixture has $U = {0, dots, #(x3c_sp.source.instance.universe_size - 1)}$ and three 3-sets: $C_0 = {#x3c_sp.source.instance.subsets.at(0).map(str).join(", ")}$, $C_1 = {#x3c_sp.source.instance.subsets.at(1).map(str).join(", ")}$, and $C_2 = {#x3c_sp.source.instance.subsets.at(2).map(str).join(", ")}$. The witness $(#x3c_sp_sol.source_config.map(str).join(", "))$ selects $C_0$ and $C_1$. + + *Step 2 -- Recover the prime assignment from the concrete products.* The target numbers are $s_0 = #sizes.at(0) = 2 dot 3 dot 5$, $s_1 = #sizes.at(1) = 7 dot 11 dot 13$, and $s_2 = #sizes.at(2) = 2 dot 7 dot 11$. Thus the six universe elements are concretely labeled by the primes $(2, 3, 5, 7, 11, 13)$. + + *Step 3 -- Form the Subset Product instance.* The target product is $B = #x3c_sp.target.instance.target = 2 dot 3 dot 5 dot 7 dot 11 dot 13$. Selecting the first two source subsets therefore means selecting target numbers $(#sizes.at(0), #sizes.at(1))$. + + *Step 4 -- Verify the witness pair.* The selected sets $C_0$ and $C_1$ are disjoint and cover all six elements exactly once, and on the target side $#sizes.at(0) dot #sizes.at(1) = #x3c_sp.target.instance.target$ while $#sizes.at(2)$ is omitted. Because the configuration is unchanged, the target witness $(#x3c_sp_sol.target_config.map(str).join(", "))$ extracts back to the same exact cover #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(q^2 log q)$ reduction @garey1979 assigns the first $3q$ primes to universe elements. Each 3-element subset $C_j = {a, b, c}$ maps to $s_j = p_a dot p_b dot p_c$. The target product is $B = product_(i=0)^(3q-1) p_i$. By unique factorization, a sub-product equals $B$ if and only if the selected subsets form an exact cover. +][ + _Construction._ Let $(X, cal(C))$ be an X3C instance with $|X| = 3q$ and $cal(C) = {C_1, dots, C_n}$. Assign primes $p_0 = 2, p_1 = 3, dots, p_(3q-1)$. For each $C_j = {a, b, c}$, set $s_j = p_a dot p_b dot p_c$. Set target $B = product_(i=0)^(3q-1) p_i$. + + _Correctness._ ($arrow.r.double$) An exact cover ${C_(j_1), dots, C_(j_q)}$ partitions $X$, so $product s_(j_ell) = product_(i=0)^(3q-1) p_i = B$. ($arrow.l.double$) If $product_(j : x_j = 1) s_j = B$, unique factorization forces each prime to appear exactly once, so the selected subsets are pairwise disjoint and cover all elements. + + _Solution extraction._ The X3C configuration equals the Subset Product configuration: select subset $j$ iff $x_j = 1$. +] + +// 8. SubsetSum → IntegerExpressionMembership (#569) +#let ss_iem = load-example("SubsetSum", "IntegerExpressionMembership") +#let ss_iem_sol = ss_iem.solutions.at(0) +#reduction-rule("SubsetSum", "IntegerExpressionMembership", + example: true, + example-caption: [#subsetsum-num-elements(ss_iem.source.instance) elements, target $B = #ss_iem.source.instance.target$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ss_iem.source) + " -o subsetsum.json", + "pred reduce subsetsum.json --to " + target-spec(ss_iem) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate subsetsum.json --config " + ss_iem_sol.source_config.map(str).join(","), + ) + + #{ + let sizes = ss_iem.source.instance.sizes + [ + *Step 1 -- Source instance.* The Subset Sum fixture has sizes $(#sizes.join(", "))$ and target $B = #ss_iem.source.instance.target$. The canonical source configuration $(#ss_iem_sol.source_config.map(str).join(", "))$ selects the second and third items, so the source sum is $5 + 6 = #ss_iem.source.instance.target$. + + *Step 2 -- Build the choice sets inside the expression.* Each source item contributes one union node $(1 union (s_i + 1))$, so the concrete choices are $(1 union 2)$, $(1 union 6)$, $(1 union 7)$, and $(1 union 9)$. With $n = #ss_iem_sol.target_config.len()$ union nodes, the target is shifted to $K = B + n = #ss_iem.target.instance.target$. + + *Step 3 -- Follow the canonical branch choices.* The target configuration $(#ss_iem_sol.target_config.map(str).join(", "))$ means left, right, right, left, so the chosen branch values are $1$, $6$, $7$, and $1$. + + *Step 4 -- Verify the equality.* The target-side sum is $1 + 6 + 7 + 1 = #ss_iem.target.instance.target$, exactly matching $K$. The right branches occur in the same two positions as the chosen source elements, so extracting the target witness returns the original Subset Sum solution #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n)$ reduction @stockmeyer1973 builds for each element $s_i$ a union node $(1 union (s_i + 1))$, then chains all unions via Minkowski sum. Set target $K = B + n$. Selecting $s_i + 1$ (right branch) encodes including element $i$ in the subset. The expression tree has $4n - 1$ nodes. +][ + _Construction._ Given Subset Sum instance $(S = {s_1, dots, s_n}, B)$, for each $s_i$ construct choice expression $c_i = (1 union (s_i + 1))$. Build the overall expression $e = c_1 + c_2 + dots + c_n$ (Minkowski sum chain). Set target $K = B + n$. + + _Correctness._ ($arrow.r.double$) If $A' subset.eq S$ sums to $B$, choose $d_i = s_i + 1$ for $s_i in A'$ and $d_i = 1$ otherwise. Then $sum d_i = B + |A'| + (n - |A'|) = B + n = K$. ($arrow.l.double$) If $sum d_i = K$ with $d_i in {1, s_i + 1}$, let $A' = {s_i : d_i = s_i + 1}$. Then $sum d_i = sum_(s_i in A') s_i + n$, so $sum_(s_i in A') s_i = B$. + + _Solution extraction._ The Subset Sum configuration is the Integer Expression Membership configuration: $x_i = 1$ (right branch) means element $i$ is selected. +] + +// 9. ExactCoverBy3Sets → MinimumWeightSolutionToLinearEquations (#860) +#let x3c_mwle = load-example("ExactCoverBy3Sets", "MinimumWeightSolutionToLinearEquations") +#let x3c_mwle_sol = x3c_mwle.solutions.at(0) +#reduction-rule("ExactCoverBy3Sets", "MinimumWeightSolutionToLinearEquations", + example: true, + example-caption: [$|U| = #x3c_mwle.source.instance.universe_size$, $|cal(C)| = #x3c_mwle.source.instance.subsets.len()$ subsets], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(x3c_mwle.source) + " -o x3c.json", + "pred reduce x3c.json --to " + target-spec(x3c_mwle) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate x3c.json --config " + x3c_mwle_sol.source_config.map(str).join(","), + ) + + #{ + let rows = x3c_mwle.target.instance.matrix + let y = x3c_mwle_sol.target_config + let q = x3c_mwle.source.instance.universe_size / 3 + [ + *Step 1 -- Source instance.* The X3C fixture has subsets $C_0 = {#x3c_mwle.source.instance.subsets.at(0).map(str).join(", ")}$, $C_1 = {#x3c_mwle.source.instance.subsets.at(1).map(str).join(", ")}$, and $C_2 = {#x3c_mwle.source.instance.subsets.at(2).map(str).join(", ")}$ over a universe of size $#x3c_mwle.source.instance.universe_size$, so $q = #q$. + + *Step 2 -- Build the incidence matrix.* The three columns correspond to $C_0$, $C_1$, and $C_2$. The six rows are $r_0 = (#rows.at(0).map(str).join(", "))$, $r_1 = (#rows.at(1).map(str).join(", "))$, $r_2 = (#rows.at(2).map(str).join(", "))$, $r_3 = (#rows.at(3).map(str).join(", "))$, $r_4 = (#rows.at(4).map(str).join(", "))$, and $r_5 = (#rows.at(5).map(str).join(", "))$, with right-hand side $b = (#x3c_mwle.target.instance.rhs.map(str).join(", "))$. + + *Step 3 -- Check the linear equations on the witness.* With $y = (#y.map(str).join(", "))$, the row products are $r_0 dot y = 1$, $r_1 dot y = 1$, $r_2 dot y = 1$, $r_3 dot y = 1$, $r_4 dot y = 1$, and $r_5 dot y = 1$. Hence $A y = b$ for the stored target witness. + + *Step 4 -- Check weight and extraction.* The vector $y$ has #y.filter(x => x != 0).len() nonzero entries, exactly the required $q = #q$. Those two nonzero positions select $C_0$ and $C_1$, so the target witness encodes the same exact cover as the source configuration $(#x3c_mwle_sol.source_config.map(str).join(", "))$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(q n)$ reduction @garey1979 builds the $3q times n$ incidence matrix $A$ where $A_(i,j) = 1$ iff element $u_i in C_j$. Set right-hand side $b = (1, dots, 1)^top$ and weight bound $K = q = |X|\/3$. An exact cover corresponds to a binary solution of weight exactly $q$. +][ + _Construction._ Let $(X, cal(C))$ be an X3C instance with $|X| = 3q$ and $cal(C) = {C_1, dots, C_n}$. Define $n$ variables $y_1, dots, y_n$. Build matrix $A in {0,1}^(3q times n)$ with $A_(i,j) = 1$ iff $u_i in C_j$. Each column has exactly 3 ones. Set $b = bold(1) in ZZ^(3q)$ and $K = q$. + + _Correctness._ ($arrow.r.double$) An exact cover selects $q$ sets, each covering 3 elements with no overlap, giving $A y = b$ with $y in {0,1}^n$ and weight $q = K$. ($arrow.l.double$) If $y$ has at most $K = q$ nonzero entries and $A y = b$, summing all equations gives $3 sum_j y_j = 3q$, so $sum y_j = q$. With $|"support"| <= q$ and each column contributing 3 incidences, every row is hit by exactly one selected column, forcing each nonzero $y_j = 1$. The selected sets form an exact cover. + + _Solution extraction._ Select subset $j$ iff $y_j != 0$. +] + +// 10. KSatisfiability → SimultaneousIncongruences (#554) +#let ksat_si = load-example("KSatisfiability", "SimultaneousIncongruences") +#let ksat_si_sol = ksat_si.solutions.at(0) +#reduction-rule("KSatisfiability", "SimultaneousIncongruences", + example: true, + example-caption: [$n = #ksat_si.source.instance.num_vars$ variables, $m = #sat-num-clauses(ksat_si.source.instance)$ clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ksat_si.source) + " -o ksat.json", + "pred reduce ksat.json --to " + target-spec(ksat_si) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate ksat.json --config " + ksat_si_sol.source_config.map(str).join(","), + ) + + #{ + let pairs = ksat_si.target.instance.pairs + let x = ksat_si_sol.target_config.at(0) + [ + *Step 1 -- Source instance.* The two clauses are $C_1 = (x_1 or x_2 or x_2)$ and $C_2 = (overline(x_1) or x_2 or x_2)$. The canonical satisfying assignment is $(#ksat_si_sol.source_config.map(str).join(", "))$. + + *Step 2 -- Assign primes and variable residue constraints.* With two variables, the reduction uses primes $3$ and $5$. The variable-generated forbidden pairs are $(#pairs.at(0).at(0), #pairs.at(0).at(1))$, $(#pairs.at(1).at(0), #pairs.at(1).at(1))$, $(#pairs.at(2).at(0), #pairs.at(2).at(1))$, and $(#pairs.at(3).at(0), #pairs.at(3).at(1))$, leaving only residues $1$ and $2$ modulo $3$ and modulo $5$. + + *Step 3 -- Encode the clauses by CRT.* Clause $C_1$ is false only when $(x_1, x_2) = (0, 0)$, i.e.\ residues $(2 mod 3, 2 mod 5)$, which yields the forbidden pair $(#pairs.at(4).at(0), #pairs.at(4).at(1))$. Clause $C_2$ is false only when $(x_1, x_2) = (1, 0)$, i.e.\ residues $(1 mod 3, 2 mod 5)$, which yields $(#pairs.at(5).at(0), #pairs.at(5).at(1))$. + + *Step 4 -- Verify the target witness.* The stored integer is $x = #x$. It satisfies $x equiv 1 mod 3$ and $x equiv 1 mod 5$, so it decodes to the source assignment $(1, 1)$. It also avoids all six forbidden classes: $1 not equiv 0 mod 3$, $1 not equiv 0, 3, 4 mod 5$, and $1 not equiv 2, 7 mod 15$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n^2 + m)$ reduction @stockmeyer1973 assigns each variable $x_i$ a distinct prime $p_i >= 5$, encoding TRUE as residue 1 and FALSE as residue 2 modulo $p_i$. All other residues are forbidden. Each clause is encoded via CRT as a single forbidden residue class modulo the product of its variables' primes. A satisfying assignment exists iff some integer avoids all forbidden classes. +][ + _Construction._ Given 3-SAT with $n$ variables and $m$ clauses, assign primes $p_1, dots, p_n >= 5$. For each variable $x_i$, forbid residues ${0, 3, 4, dots, p_i - 1}$ modulo $p_i$, leaving only ${1, 2}$. For each clause $C_j$ over variables $x_(i_1), x_(i_2), x_(i_3)$, compute the falsifying residue $r_k in {1, 2}$ for each literal and use CRT to find $R_j$ with $R_j equiv r_k mod p_(i_k)$ for $k = 1,2,3$. Forbid $R_j$ modulo $M_j = p_(i_1) p_(i_2) p_(i_3)$. + + _Correctness._ ($arrow.r.double$) A satisfying assignment $tau$ defines residues $r_i in {1,2}$ per variable. By CRT, some integer $x$ has these residues. It avoids all variable-forbidden classes and all clause-forbidden classes (since at least one literal is true, the residue triple differs from the falsifying triple). ($arrow.l.double$) Any feasible $x$ has $x mod p_i in {1,2}$ for all $i$. Define $tau(x_i) = "TRUE"$ if residue 1, FALSE if 2. If a clause were false, $x$ would match its forbidden CRT class -- contradiction. + + _Solution extraction._ Set $tau(x_i) = "TRUE"$ if $x mod p_i = 1$, FALSE if $x mod p_i = 2$. +] + +// 11. Partition → SequencingToMinimizeTardyTaskWeight (#471) +#let part_stw = load-example("Partition", "SequencingToMinimizeTardyTaskWeight") +#let part_stw_sol = part_stw.solutions.at(0) +#reduction-rule("Partition", "SequencingToMinimizeTardyTaskWeight", + example: true, + example-caption: [#part_stw.source.instance.sizes.len() elements, total $= #part_stw.source.instance.sizes.sum()$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(part_stw.source) + " -o partition.json", + "pred reduce partition.json --to " + target-spec(part_stw) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate partition.json --config " + part_stw_sol.source_config.map(str).join(","), + ) + + #{ + let lengths = part_stw.target.instance.lengths + let weights = part_stw.target.instance.weights + let deadline = part_stw.target.instance.deadlines.at(0) + let on-time-sum = part_stw_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => part_stw.source.instance.sizes.at(i)).sum() + let tardy-sum = part_stw_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => part_stw.source.instance.sizes.at(i)).sum() + [ + *Step 1 -- Source instance.* The Partition fixture has sizes $(#part_stw.source.instance.sizes.map(str).join(", "))$ with total $#part_stw.source.instance.sizes.sum()$, so the target deadline is $T = #deadline$. The canonical source vector $(#part_stw_sol.source_config.map(str).join(", "))$ splits the multiset into sums $#on-time-sum$ and $#tardy-sum$. + + *Step 2 -- Build the task table.* #table( + columns: (auto, auto, auto, auto), + inset: 4pt, + align: left, + table.header([*task*], [*$l_j$*], [*$w_j$*], [*$d_j$*]), + [$t_0$], [#lengths.at(0)], [#weights.at(0)], [#deadline], + [$t_1$], [#lengths.at(1)], [#weights.at(1)], [#deadline], + [$t_2$], [#lengths.at(2)], [#weights.at(2)], [#deadline], + [$t_3$], [#lengths.at(3)], [#weights.at(3)], [#deadline], + [$t_4$], [#lengths.at(4)], [#weights.at(4)], [#deadline], + [$t_5$], [#lengths.at(5)], [#weights.at(5)], [#deadline], + ) + + *Step 3 -- Follow the canonical schedule.* The target permutation $(#part_stw_sol.target_config.map(str).join(", "))$ schedules tasks in the order $t_1, t_2, t_4, t_5, t_0, t_3$. The completion times are $1, 2, 4, 5, 8, 10$, so $t_1, t_2, t_4, t_5$ are on time and $t_0, t_3$ are tardy. + + *Step 4 -- Compute tardy weight and recover the partition.* Because weights equal lengths here, the tardy weight is $w_0 + w_3 = 3 + 2 = #deadline$, and the on-time tasks have total size $#on-time-sum$ while the tardy tasks have total size #tardy-sum. Extracting the schedule therefore returns the balanced partition $(#part_stw_sol.source_config.map(str).join(", "))$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n)$ reduction @karp1972 maps each element $a_i$ to a task with length $l(t_i) = a_i$, weight $w(t_i) = a_i$, and common deadline $T = B\/2$. The tardiness bound is $K = T$. Tasks scheduled before $T$ are on-time; those after are tardy. A balanced partition exists iff total tardy weight can be at most $K$. +][ + _Construction._ Given Partition instance $A = {a_1, dots, a_n}$ with total $B$. If $B$ is odd, output a trivially infeasible instance (all deadlines 0, $K = 0$). If $B$ is even, set $T = B\/2$. For each $a_i$, create task $t_i$ with $l(t_i) = w(t_i) = a_i$ and deadline $d(t_i) = T$. Set bound $K = T$. + + _Correctness._ ($arrow.r.double$) A balanced partition $A', A''$ with sums $T$ each: schedule $A'$ first (on-time, total time $T$), then $A''$ (tardy, weight $T = K$). ($arrow.l.double$) If tardy weight $<= K = T$, then on-time tasks fit before $T$ and sum to $<= T$, while tardy tasks have weight $B - sum_("on-time") <= T$, forcing on-time sum $= T$. This yields a balanced partition. + + _Solution extraction._ On-time tasks (completing by $T$) form one partition half ($x_i = 0$), tardy tasks the other ($x_i = 1$). +] + +// 12. Partition → OpenShopScheduling (#481) +#let part_oss = load-example("Partition", "OpenShopScheduling") +#let part_oss_sol = part_oss.solutions.at(0) +#reduction-rule("Partition", "OpenShopScheduling", + example: true, + example-caption: [#part_oss.source.instance.sizes.len() elements, $m = #part_oss.target.instance.num_machines$ machines], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(part_oss.source) + " -o partition.json", + "pred reduce partition.json --to " + target-spec(part_oss) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate partition.json --config " + part_oss_sol.source_config.map(str).join(","), + ) + + #{ + let q = part_oss.source.instance.sizes.sum() / 2 + let p = part_oss.target.instance.processing_times + let left-sum = part_oss_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => part_oss.source.instance.sizes.at(i)).sum() + let right-sum = part_oss_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => part_oss.source.instance.sizes.at(i)).sum() + [ + *Step 1 -- Source instance.* The Partition fixture has sizes $(#part_oss.source.instance.sizes.map(str).join(", "))$, total $#part_oss.source.instance.sizes.sum()$, and half-sum $Q = #q$. The canonical source vector $(#part_oss_sol.source_config.map(str).join(", "))$ gives subset sums $#left-sum$ and $#right-sum$. + + *Step 2 -- Build the open-shop job table.* #table( + columns: (auto, auto, auto, auto), + inset: 4pt, + align: left, + table.header([*job*], [*$p_{j,1}$*], [*$p_{j,2}$*], [*$p_{j,3}$*]), + [$J_0$], [#p.at(0).at(0)], [#p.at(0).at(1)], [#p.at(0).at(2)], + [$J_1$], [#p.at(1).at(0)], [#p.at(1).at(1)], [#p.at(1).at(2)], + [$J_2$], [#p.at(2).at(0)], [#p.at(2).at(1)], [#p.at(2).at(2)], + [$J_3$], [#p.at(3).at(0)], [#p.at(3).at(1)], [#p.at(3).at(2)], + ) The first three jobs come from the partition elements, and the special job $J_3$ has processing time $Q = #q$ on every machine. + + *Step 3 -- Decode the canonical machine orders.* The target configuration $(#part_oss_sol.target_config.map(str).join(", "))$ splits into $M_1 = (0, 1, 2, 3)$, $M_2 = (0, 1, 2, 3)$, and $M_3 = (2, 3, 0, 1)$. On machine $M_3$, job $J_2$ occupies $[0, 3)$ and the special job $J_3$ starts exactly at time $Q = 3$, so the prefix before the special job contains precisely job $J_2$. + + *Step 4 -- Verify extraction and makespan.* Because only $J_2$ finishes on $M_3$ by time $Q$, the extracted source vector is $(#part_oss_sol.source_config.map(str).join(", "))$, i.e.\ subset sum #right-sum versus #left-sum. Evaluating the stored machine orders gives a concrete makespan of $12$, so the `load-example()` fixture shows both the machine assignment and the middle-machine split used for extraction #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(k)$ reduction @gonzalez1976 creates $k + 1$ jobs on 3 machines: $k$ element jobs with $p_(j,i) = a_j$ on all machines, plus one special job with $p = Q = S\/2$. The target makespan is $3Q$. A balanced partition exists iff the open shop can achieve makespan $<= 3Q$. +][ + _Construction._ Given Partition instance $A = {a_1, dots, a_k}$ with total $S$ and $Q = S\/2$. Set $m = 3$ machines. For each $a_j$, create element job $J_j$ with $p_(j,1) = p_(j,2) = p_(j,3) = a_j$. Create special job $J_(k+1)$ with $p_(k+1,i) = Q$ on all machines. Deadline $D = 3Q$. + + _Correctness._ ($arrow.r.double$) With a balanced partition $I_1, I_2$, schedule the special job consecutively on machines 1, 2, 3 during $[0,Q), [Q,2Q), [2Q,3Q)$. Use a rotated assignment for $I_1$ and $I_2$ jobs to fill the remaining idle blocks, each of length $Q$. ($arrow.l.double$) With makespan $<= 3Q$, the special job alone needs $3Q$ elapsed time, so it tiles $[0,3Q)$ exactly. On each machine, element jobs fill two idle blocks of length $Q$ each. The jobs in one block sum to $Q$, giving a balanced partition. + + _Solution extraction._ Identify the special job's position on machine 1. Element jobs in one idle block form a subset summing to $Q$. +] + +// 13. NAESatisfiability → MaxCut (#166) +#let nae_mc = load-example("NAESatisfiability", "MaxCut") +#let nae_mc_sol = nae_mc.solutions.at(0) +#reduction-rule("NAESatisfiability", "MaxCut", + example: true, + example-caption: [$n = #nae_mc.source.instance.num_vars$ variables, $m = #sat-num-clauses(nae_mc.source.instance)$ clauses, $M = #(sat-num-clauses(nae_mc.source.instance) + 1)$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(nae_mc.source) + " -o naesat.json", + "pred reduce naesat.json --to " + target-spec(nae_mc) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate naesat.json --config " + nae_mc_sol.source_config.map(str).join(","), + ) + + #{ + let n = nae_mc.source.instance.num_vars + let m = sat-num-clauses(nae_mc.source.instance) + let big-m = m + 1 + let clause-edge-count = graph-num-edges(nae_mc.target.instance) - n + let cut-value = n * big-m + 2 * m + [ + *Step 1 -- Source instance.* NAE-SAT with $n = #n$ variables and $m = #m$ clauses. The implementation uses forcing weight $M = m + 1 = #big-m$. + + *Step 2 -- Construct the weighted graph.* Variable gadgets contribute #n heavy edges of weight $M$. Because the canonical fixture has 3 literals per clause, each clause contributes one unit-weight triangle, so the target has #clause-edge-count unit-weight clause edges and $#graph-num-edges(nae_mc.target.instance)$ edges total on $#graph-num-vertices(nae_mc.target.instance)$ vertices. + + *Step 3 -- Verify the canonical witness.* Source assignment $(#nae_mc_sol.source_config.map(str).join(", "))$ induces target cut $(#nae_mc_sol.target_config.map(str).join(", "))$. All #n heavy edges are cut, and each of the #m clause triangles has a 1-2 split contributing 2, so the total cut weight is $#cut-value$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This implemented reduction sets $M = m + 1$, creates two literal vertices per variable, and adds one unit-weight edge for every literal pair inside a clause. When every clause has 3 literals, each clause gadget is a triangle, so the construction is the usual NAE-SAT-to-Max-Cut graph on $2n$ vertices with $n + 3m$ edges. +][ + _Construction._ Let $phi$ have $n$ variables and $m$ clauses, and set $M = m + 1$. For each variable $x_i$, create a positive literal vertex $p_i = 2i$ and a negative literal vertex $n_i = 2i + 1$, joined by one weight-$M$ edge. For each clause $C_j$, add a unit-weight edge between every pair of literal vertices appearing in $C_j$. In particular, if every clause has three literals, each clause becomes a unit-weight triangle. + + _Correctness._ Assume from here on that each clause has exactly three literals, matching the canonical fixture. Then every clause gadget is a triangle. + + ($arrow.r.double$) Let $alpha$ be a NAE-satisfying assignment. Put $p_i$ and $n_i$ on opposite sides of the cut according to $alpha$, so every variable edge is cut and contributes $M$. In each clause triangle, at least one literal is true and at least one is false, so the three vertices split $1$-$2$ across the cut and contribute exactly 2. Therefore the cut weight is $n M + 2m = n (m + 1) + 2m$. + + ($arrow.l.double$) Suppose a cut has weight at least $n (m + 1) + 2m$. The $m$ clause triangles contribute at most $2m$ in total, so the variable edges must contribute at least $n (m + 1)$. Since each variable edge contributes at most $M = m + 1$, all $n$ variable edges are cut. Thus $p_i$ and $n_i$ lie on opposite sides for every variable, and the cut defines a consistent Boolean assignment by reading the side of $p_i$. The remaining $2m$ weight must come from the clause triangles, so each triangle contributes exactly 2 and therefore has vertices on both sides of the cut. Hence every clause contains both a true and a false literal, and the extracted assignment NAE-satisfies $phi$. Because a satisfying instance attains $n (m + 1) + 2m$, every optimal cut of the target has this form. + + _Solution extraction._ Read the positive literal vertices: $x_i = 1$ iff vertex $2i$ lies on side 1 of the cut. +] + +// 14. HamiltonianPath → IsomorphicSpanningTree (#912) +#let hp_ist = load-example("HamiltonianPath", "IsomorphicSpanningTree") +#let hp_ist_sol = hp_ist.solutions.at(0) +#reduction-rule("HamiltonianPath", "IsomorphicSpanningTree", + example: true, + example-caption: [$n = #graph-num-vertices(hp_ist.source.instance)$ vertices, target tree $P_n$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(hp_ist.source) + " -o hampath.json", + "pred reduce hampath.json --to " + target-spec(hp_ist) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate hampath.json --config " + hp_ist_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* Graph $G$ with $n = #graph-num-vertices(hp_ist.source.instance)$ vertices and $|E| = #graph-num-edges(hp_ist.source.instance)$ edges. + + *Step 2 -- Identity reduction.* Target host graph is identical. Target tree $T = P_#graph-num-vertices(hp_ist.target.instance)$ with #hp_ist.target.instance.tree.edges.len() edges. + + *Step 3 -- Verify a solution.* Hamiltonian path visits vertices in order $(#hp_ist_sol.source_config.map(str).join(", "))$. The isomorphism maps $P_n$ to this path in $G$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n)$ reduction @garey1979 passes the graph through unchanged and sets the target tree $T = P_n$ (the path on $n$ vertices). A Hamiltonian path in $G$ is exactly a spanning tree isomorphic to $P_n$: both are connected, acyclic, span all vertices, and have maximum degree 2. The reduction is size-preserving. +][ + _Construction._ Given $G = (V, E)$ with $|V| = n$, set the host graph to $G$ and the target tree to $T = P_n = ({t_0, dots, t_(n-1)}, {{t_i, t_(i+1)} : 0 <= i <= n-2})$. + + _Correctness._ ($arrow.r.double$) A Hamiltonian path $v_(pi(0)), dots, v_(pi(n-1))$ gives edges ${v_(pi(i)), v_(pi(i+1))}$ forming a spanning subgraph isomorphic to $P_n$ via $phi(t_i) = v_(pi(i))$. ($arrow.l.double$) A spanning tree of $G$ isomorphic to $P_n$ is a path on all $n$ vertices (since $P_n$ has max degree 2 and is connected). The isomorphism $phi$ gives the Hamiltonian path $phi(t_0), dots, phi(t_(n-1))$. + + _Solution extraction._ The isomorphism $phi$ directly yields the Hamiltonian path as the sequence $phi(t_0), phi(t_1), dots, phi(t_(n-1))$. +] + +// 15. ExactCoverBy3Sets → AlgebraicEquationsOverGF2 (#859) +#let x3c_gf2 = load-example("ExactCoverBy3Sets", "AlgebraicEquationsOverGF2") +#let x3c_gf2_sol = x3c_gf2.solutions.at(0) +#reduction-rule("ExactCoverBy3Sets", "AlgebraicEquationsOverGF2", + example: true, + example-caption: [$|U| = #x3c_gf2.source.instance.universe_size$, $|cal(C)| = #x3c_gf2.source.instance.subsets.len()$ subsets], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(x3c_gf2.source) + " -o x3c.json", + "pred reduce x3c.json --to " + target-spec(x3c_gf2) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate x3c.json --config " + x3c_gf2_sol.source_config.map(str).join(","), + ) + + #{ + let x = x3c_gf2_sol.target_config + [ + *Step 1 -- Source instance.* The X3C fixture uses subsets $C_0 = {#x3c_gf2.source.instance.subsets.at(0).map(str).join(", ")}$, $C_1 = {#x3c_gf2.source.instance.subsets.at(1).map(str).join(", ")}$, and $C_2 = {#x3c_gf2.source.instance.subsets.at(2).map(str).join(", ")}$ over a universe of size $#x3c_gf2.source.instance.universe_size$. + + *Step 2 -- Build the GF(2) system.* The target has $#x3c_gf2.target.instance.num_variables$ variables and #x3c_gf2.target.instance.equations.len() equations. Grouping the JSON equations by element gives: + for element 0, $x_0 + x_2 + 1 = 0$ and $x_0 x_2 = 0$; + for elements 1 and 2, $x_0 + 1 = 0$; + for elements 3 and 4, $x_1 + x_2 + 1 = 0$ and $x_1 x_2 = 0$; + for element 5, $x_1 + 1 = 0$. + + *Step 3 -- Evaluate the canonical target witness.* The target assignment is $x = (#x.map(str).join(", ")) = (1, 1, 0)$. Substituting gives $1 + 0 + 1 = 0$ mod 2, $1 dot 0 = 0$, and $1 + 1 = 0$ mod 2, which are exactly the three polynomial patterns appearing in the fixture. + + *Step 4 -- Verify the witness pair.* The two 1-entries in $x$ select $C_0$ and $C_1$, while $x_2 = 0$ omits $C_2$. Thus the target witness encodes the same exact cover as the source configuration $(#x3c_gf2_sol.source_config.map(str).join(", "))$ #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(q n^2)$ reduction @garey1979 assigns one binary variable $x_j$ per subset. For each universe element $u_i$, a linear equation $sum_(j in S_i) x_j + 1 = 0$ (mod 2) enforces odd coverage, and pairwise products $x_j x_k = 0$ (mod 2) forbid double coverage. Together these force exactly-once covering. +][ + _Construction._ Let $(X, cal(C))$ be an X3C instance with $|X| = 3q$ and $cal(C) = {C_1, dots, C_n}$. Define $n$ variables over GF(2). For each element $u_i$, let $S_i = {j : u_i in C_j}$. Add linear constraint $sum_(j in S_i) x_j + 1 = 0$ (mod 2) and pairwise constraints $x_j dot x_k = 0$ (mod 2) for all $j < k in S_i$. Total: at most $3q + sum_i binom(|S_i|, 2)$ equations. + + _Correctness._ ($arrow.r.double$) An exact cover sets $x_j = 1$ for exactly $q$ selected sets. Each element has exactly one covering set, so $sum_(j in S_i) x_j = 1 equiv 1$ (mod 2), satisfying the linear constraint. All pairwise products vanish since at most one $x_j = 1$ per $S_i$. ($arrow.l.double$) The linear constraint forces an odd number of selected sets per element. The pairwise constraints forbid selecting two sets covering the same element. Together: exactly one set per element. Since each set has 3 elements and all $3q$ are covered, exactly $q$ sets are selected. + + _Solution extraction._ The X3C configuration equals the GF(2) configuration: select subset $j$ iff $x_j = 1$. +] + +// 16. Partition → ProductionPlanning (#488) +#let part_pp = load-example("Partition", "ProductionPlanning") +#let part_pp_sol = part_pp.solutions.at(0) +#reduction-rule("Partition", "ProductionPlanning", + example: true, + example-caption: [#part_pp.source.instance.sizes.len() elements, total $= #part_pp.source.instance.sizes.sum()$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(part_pp.source) + " -o partition.json", + "pred reduce partition.json --to " + target-spec(part_pp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate partition.json --config " + part_pp_sol.source_config.map(str).join(","), + ) + + #{ + let left-sum = part_pp_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => part_pp.source.instance.sizes.at(i)).sum() + let right-sum = part_pp_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => part_pp.source.instance.sizes.at(i)).sum() + let prod = part_pp_sol.target_config + [ + *Step 1 -- Source instance.* The Partition fixture has sizes $(#part_pp.source.instance.sizes.map(str).join(", "))$ with total $#part_pp.source.instance.sizes.sum()$, so $Q = #(part_pp.source.instance.sizes.sum() / 2)$. The canonical source vector $(#part_pp_sol.source_config.map(str).join(", "))$ splits the instance into sums $#left-sum$ and $#right-sum$. + + *Step 2 -- Build the period table.* #table( + columns: (auto, auto, auto, auto, auto), + inset: 4pt, + align: left, + table.header([*period*], [*$c_t$*], [*$b_t$*], [*$r_t$*], [*$x_t$*]), + [$P_0$], [#part_pp.target.instance.capacities.at(0)], [#part_pp.target.instance.setup_costs.at(0)], [#part_pp.target.instance.demands.at(0)], [#prod.at(0)], + [$P_1$], [#part_pp.target.instance.capacities.at(1)], [#part_pp.target.instance.setup_costs.at(1)], [#part_pp.target.instance.demands.at(1)], [#prod.at(1)], + [$P_2$], [#part_pp.target.instance.capacities.at(2)], [#part_pp.target.instance.setup_costs.at(2)], [#part_pp.target.instance.demands.at(2)], [#prod.at(2)], + [$P_3$], [#part_pp.target.instance.capacities.at(3)], [#part_pp.target.instance.setup_costs.at(3)], [#part_pp.target.instance.demands.at(3)], [#prod.at(3)], + [$P_4$], [#part_pp.target.instance.capacities.at(4)], [#part_pp.target.instance.setup_costs.at(4)], [#part_pp.target.instance.demands.at(4)], [#prod.at(4)], + [$P_5$], [#part_pp.target.instance.capacities.at(5)], [#part_pp.target.instance.setup_costs.at(5)], [#part_pp.target.instance.demands.at(5)], [#prod.at(5)], + ) The first five periods encode the partition elements, and the last period carries the demand of $10$ units. + + *Step 3 -- Track cumulative production and inventory.* The stored plan $(#prod.map(str).join(", "))$ gives cumulative production $0, 0, 0, 4, 10, 10$ against cumulative demand $0, 0, 0, 0, 0, 10$. Hence the inventory levels are $0, 0, 0, 4, 10, 0$, so every prefix remains feasible. + + *Step 4 -- Check the cost and recover the partition.* Only periods $P_3$ and $P_4$ are active, so the total cost is just the setup cost $4 + 6 = #part_pp.target.instance.cost_bound$; production and inventory costs are all zero in the fixture. The active periods therefore recover the source vector $(#part_pp_sol.source_config.map(str).join(", "))$, selecting the subset of size #right-sum #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n)$ reduction @florianLenstraRinnooyKan1980 maps each element $a_i$ to a production period with capacity $c_i = a_i$ and setup cost $b_i = a_i$ (zero production and inventory costs). One demand period requires $Q = S\/2$ units with no production capacity. The cost bound is $B = Q$. Activating a subset summing to $Q$ exactly meets demand at cost $Q = B$. +][ + _Construction._ Given Partition instance $A = {a_1, dots, a_n}$ with total $S$ and $Q = S\/2$. If $S$ is odd, output a trivially infeasible instance. Otherwise create $n + 1$ periods: for each $a_i$, period $i$ has $r_i = 0, c_i = a_i, b_i = a_i, p_i = h_i = 0$; demand period $n+1$ has $r_(n+1) = Q, c_(n+1) = 0, b_(n+1) = p_(n+1) = h_(n+1) = 0$. Cost bound $B = Q$. + + _Correctness._ ($arrow.r.double$) A balanced partition $A'$ with sum $Q$ activates those periods: total production $= Q$ meets demand, inventory levels stay non-negative, and total cost $= sum_(i in A') a_i = Q = B$. ($arrow.l.double$) Any feasible plan has setup cost $sum_(i in J) a_i <= Q$ (where $J$ is the set of active periods) and must produce at least $Q$ units. Since $x_i <= c_i = a_i$, total production $<= sum_(i in J) a_i$. These force $sum_(i in J) a_i = Q$, yielding a balanced partition. + + _Solution extraction._ Active element periods ($x_i > 0$) form one partition half. +] + +// 17. HamiltonianPathBetweenTwoVertices → LongestPath (#359) +#let hpbtv_lp = load-example("HamiltonianPathBetweenTwoVertices", "LongestPath") +#let hpbtv_lp_sol = hpbtv_lp.solutions.at(0) +#reduction-rule("HamiltonianPathBetweenTwoVertices", "LongestPath", + example: true, + example-caption: [$n = #graph-num-vertices(hpbtv_lp.source.instance)$ vertices, $s = #hpbtv_lp.source.instance.source_vertex$, $t = #hpbtv_lp.source.instance.target_vertex$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(hpbtv_lp.source) + " -o hampath2v.json", + "pred reduce hampath2v.json --to " + target-spec(hpbtv_lp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate hampath2v.json --config " + hpbtv_lp_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* Graph $G$ with $n = #graph-num-vertices(hpbtv_lp.source.instance)$ vertices, $|E| = #graph-num-edges(hpbtv_lp.source.instance)$ edges, $s = #hpbtv_lp.source.instance.source_vertex$, $t = #hpbtv_lp.source.instance.target_vertex$. + + *Step 2 -- Identity reduction.* Target graph is identical with unit edge lengths. $K = n - 1 = #(graph-num-vertices(hpbtv_lp.source.instance) - 1)$, same $s$ and $t$. + + *Step 3 -- Verify a solution.* Source Hamiltonian path visits vertices $(#hpbtv_lp_sol.source_config.map(str).join(", "))$ from $s = #hpbtv_lp.source.instance.source_vertex$ to $t = #hpbtv_lp.source.instance.target_vertex$. Target selects #hpbtv_lp_sol.target_config.filter(x => x == 1).len() edges, total length $= n - 1 = K$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n + m)$ reduction @garey1979 passes the graph through with unit edge lengths, same source $s$ and target $t$, and bound $K = n - 1$. A Hamiltonian $s$-$t$ path uses exactly $n - 1$ edges, which is the maximum possible for a simple path on $n$ vertices. The reduction is size-preserving. +][ + _Construction._ Given $(G = (V, E), s, t)$ with $n = |V|$, set $G' = G$, $ell(e) = 1$ for all $e in E$, $s' = s$, $t' = t$, and $K = n - 1$. + + _Correctness._ ($arrow.r.double$) A Hamiltonian $s$-$t$ path has $n - 1$ edges of length 1 each, giving total length $n - 1 = K$. ($arrow.l.double$) A simple $s'$-$t'$ path of length $>= K = n - 1$ has $>= n - 1$ edges. Since a simple path on $n$ vertices can have at most $n - 1$ edges, it has exactly $n - 1$ edges and visits all vertices -- it is a Hamiltonian $s$-$t$ path. + + _Solution extraction._ From the edge-selection vector, trace the path from $s$ following selected edges to reconstruct the vertex permutation. +] + +// 18. GraphPartitioning → MaxCut (from main codebase) +#let gp_mc = load-example("GraphPartitioning", "MaxCut") +#let gp_mc_sol = gp_mc.solutions.at(0) +#reduction-rule("GraphPartitioning", "MaxCut", + example: true, + example-caption: [$n = #graph-num-vertices(gp_mc.source.instance)$ vertices, $|E| = #graph-num-edges(gp_mc.source.instance)$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(gp_mc.source) + " -o graphpart.json", + "pred reduce graphpart.json --to " + target-spec(gp_mc) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate graphpart.json --config " + gp_mc_sol.source_config.map(str).join(","), + ) + + #{ + let n = graph-num-vertices(gp_mc.source.instance) + let m = graph-num-edges(gp_mc.source.instance) + let penalty = m + 1 + let side-a = gp_mc_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => i) + let side-b = gp_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) + let source-cut = gp_mc.source.instance.graph.edges.filter(e => gp_mc_sol.source_config.at(e.at(0)) != gp_mc_sol.source_config.at(e.at(1))).len() + let target-weight = gp_mc.target.instance.graph.edges.enumerate().filter(((i, e)) => gp_mc_sol.target_config.at(e.at(0)) != gp_mc_sol.target_config.at(e.at(1))).map(((i, e)) => gp_mc.target.instance.edge_weights.at(i)).sum() + let unbalanced-pairs = (n / 2 - 1) * (n / 2 + 1) + let unbalanced-upper = penalty * unbalanced-pairs + [ + *Step 1 -- Source instance.* Graph $G$ has $n = #n$ vertices and $|E| = #m$ edges, so the code uses penalty $P = |E| + 1 = #penalty$. + + *Step 2 -- Build the weighted complete graph.* The target has $#graph-num-vertices(gp_mc.target.instance)$ vertices and $#graph-num-edges(gp_mc.target.instance)$ edges. Original edges receive weight $P - 1 = #(penalty - 1)$, while non-edges receive weight $P = #penalty$. + + *Step 3 -- Verify the canonical witness.* The balanced partition $(#gp_mc_sol.source_config.map(str).join(", "))$ gives sides $A = {#side-a.map(str).join(", ")}$ and $B = {#side-b.map(str).join(", ")}$ with $#(side-a.len() * side-b.len())$ crossing pairs. It cuts #source-cut source edges, so the identical Max-Cut partition has weight $#target-weight = #penalty dot #(side-a.len() * side-b.len()) - #source-cut$. Any unbalanced $2$-$4$ split has at most #unbalanced-pairs crossing pairs and therefore weight at most $#unbalanced-upper < #target-weight$, so the optimum is forced to be balanced #sym.checkmark. + ] + } + + *Multiplicity:* The fixture stores one canonical witness. + ], +)[ + This $O(n^2)$ reduction @garey1979 builds a weighted complete graph on the same vertices, with weight $P - 1$ on original edges and weight $P$ on non-edges, where $P = |E| + 1$. For any partition $(A, B)$, the target cut weight is $P |A| |B| - |E(A, B)|$, so the factor $P$ first forces balance and then the $- |E(A, B)|$ term minimizes the number of source edges crossing the bisection. +][ + _Construction._ Let $G = (V, E)$ be a Graph Partitioning instance with $|V| = n$ even, and let $P = |E| + 1$. Build the complete graph $K_n$ on the same vertex set. For each pair $u != v$, set + $w(u,v) = P - 1$ if ${u,v} in E$ and $w(u,v) = P$ otherwise. + The target Max-Cut instance therefore has $n$ vertices and $n(n-1)\/2$ weighted edges. + + _Correctness._ For any partition $(A, B)$ of $V$, let $c(A, B) = |E(A, B)|$ be the number of source edges crossing from $A$ to $B$. Among the $|A| |B|$ crossing pairs, exactly $c(A, B)$ are edges of $G$ and the remaining $|A| |B| - c(A, B)$ are non-edges. Hence the target cut weight is + $ + c(A, B) (P - 1) + (|A| |B| - c(A, B)) P + = P |A| |B| - c(A, B). + $ + + ($arrow.r.double$) If $(A, B)$ is a balanced partition of $G$ with $|A| = |B| = n\/2$ and cut size $c(A, B)$, then the same partition in the target graph has weight $P n^2 \/ 4 - c(A, B)$. + + ($arrow.l.double$) Any unbalanced partition of an even-sized vertex set satisfies $|A| |B| <= n^2 \/ 4 - 1$, so its target weight is at most $P (n^2 \/ 4 - 1)$. On the other hand, any balanced partition has weight at least $P n^2 \/ 4 - |E| > P (n^2 \/ 4 - 1)$ because $P = |E| + 1$. Therefore no optimal Max-Cut can be unbalanced: every optimum must satisfy $|A| = |B| = n\/2$. Once balance is forced, the term $P |A| |B| = P n^2 \/ 4$ is constant, so maximizing target weight is exactly the same as minimizing $c(A, B)$. Thus optimal Max-Cut solutions are precisely minimum bisections of $G$. + + _Solution extraction._ The Max-Cut partition vector is already a valid Graph Partitioning witness, so extraction is the identity map. +] + #pagebreak() #bibliography("references.bib", style: "ieee") diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index d36a5e617..f1b54917e 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -220,9 +220,11 @@ Flags by problem type: LongestPath --graph, --edge-lengths, --source-vertex, --target-vertex HamiltonianPathBetweenTwoVertices --graph, --source-vertex, --target-vertex ShortestWeightConstrainedPath --graph, --edge-lengths, --edge-weights, --source-vertex, --target-vertex, --weight-bound + GraphPartitioning --graph, --num-partitions MaximalIS --graph, --weights SAT, NAESAT --num-vars, --clauses KSAT --num-vars, --clauses [--k] + NonTautology --num-vars, --disjuncts QUBO --matrix SpinGlass --graph, --couplings, --fields KColoring --graph, --k @@ -370,6 +372,7 @@ Examples: pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 --example-side target pred create MIS --graph 0-1,1-2,2-3 --weights 1,1,1 pred create SAT --num-vars 3 --clauses \"1,2;-1,3\" + pred create NonTautology --num-vars 3 --disjuncts \"1,2,3;-1,-2,-3\" pred create QUBO --matrix \"1,0.5;0.5,2\" pred create CapacityAssignment --capacities 1,2,3 --cost-matrix \"1,3,6;2,4,7;1,2,5\" --delay-matrix \"8,4,1;7,3,1;6,3,1\" --cost-budget 10 --delay-budget 12 pred create ProductionPlanning --num-periods 6 --demands 5,3,7,2,8,5 --capacities 12,12,12,12,12,12 --setup-costs 10,10,10,10,10,10 --production-costs 1,1,1,1,1,1 --inventory-costs 1,1,1,1,1,1 --cost-bound 80 @@ -474,6 +477,9 @@ pub struct CreateArgs { /// Clauses for SAT problems (semicolon-separated, e.g., "1,2;-1,3") #[arg(long)] pub clauses: Option, + /// Disjuncts for NonTautology (semicolon-separated, e.g., "1,2;-1,3") + #[arg(long)] + pub disjuncts: Option, /// Number of variables (for SAT/KSAT) #[arg(long)] pub num_vars: Option, @@ -484,6 +490,9 @@ pub struct CreateArgs { /// Shared integer parameter (use `pred create ` for the problem-specific meaning) #[arg(long)] pub k: Option, + /// Number of partitions for GraphPartitioning (currently must be 2) + #[arg(long)] + pub num_partitions: Option, /// Generate a random instance (graph-based problems only) #[arg(long)] pub random: bool, diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 1bfd40cab..5cbb0e948 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -16,9 +16,9 @@ use problemreductions::models::algebraic::{ }; use problemreductions::models::formula::Quantifier; use problemreductions::models::graph::{ - DirectedHamiltonianPath, DisjointConnectingPaths, GeneralizedHex, HamiltonianCircuit, - HamiltonianPath, HamiltonianPathBetweenTwoVertices, IntegralFlowBundles, Kernel, - LengthBoundedDisjointPaths, LongestCircuit, LongestPath, MinimumCutIntoBoundedSets, + DirectedHamiltonianPath, DisjointConnectingPaths, GeneralizedHex, GraphPartitioning, + HamiltonianCircuit, HamiltonianPath, HamiltonianPathBetweenTwoVertices, IntegralFlowBundles, + Kernel, LengthBoundedDisjointPaths, LongestCircuit, LongestPath, MinimumCutIntoBoundedSets, MinimumDummyActivitiesPert, MinimumGeometricConnectedDominatingSet, MinimumMaximalMatching, MinimumMultiwayCut, MixedChinesePostman, MultipleChoiceBranching, PathConstrainedNetworkFlow, RootedTreeArrangement, SteinerTree, SteinerTreeInGraphs, StrongConnectivityAugmentation, @@ -90,9 +90,11 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool { && args.couplings.is_none() && args.fields.is_none() && args.clauses.is_none() + && args.disjuncts.is_none() && args.num_vars.is_none() && args.matrix.is_none() && args.k.is_none() + && args.num_partitions.is_none() && args.target.is_none() && args.m.is_none() && args.n.is_none() @@ -657,6 +659,7 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "HamiltonianPathBetweenTwoVertices" => { "--graph 0-1,0-3,1-2,1-4,2-5,3-4,4-5,2-3 --source-vertex 0 --target-vertex 5" } + "GraphPartitioning" => "--graph 0-1,1-2,2-3,3-0 --num-partitions 2", "LongestPath" => { "--graph 0-1,0-2,1-3,2-3,2-4,3-5,4-5,4-6,5-6,1-6 --edge-lengths 3,2,4,1,5,2,3,2,4,1 --source-vertex 0 --target-vertex 6" } @@ -707,7 +710,7 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "KSatisfiability" => "--num-vars 3 --clauses \"1,2,3;-1,2,-3\" --k 3", "Maximum2Satisfiability" => "--num-vars 4 --clauses \"1,2;1,-2;-1,3;-1,-3;2,4;-3,-4;3,4\"", "NonTautology" => { - "--num-vars 3 --clauses \"1,2,3;-1,-2,-3\"" + "--num-vars 3 --disjuncts \"1,2,3;-1,-2,-3\"" } "OneInThreeSatisfiability" => { "--num-vars 4 --clauses \"1,2,3;-1,3,4;2,-3,-4\"" @@ -1092,6 +1095,7 @@ fn help_flag_hint( ("MinimumCodeGenerationParallelAssignments", "assignments") => { "semicolon-separated target:reads entries: \"0:1,2;1:0;2:3;3:1,2\"" } + ("NonTautology", "disjuncts") => "semicolon-separated disjuncts: \"1,2,3;-1,-2,-3\"", ("TimetableDesign", "craftsman_avail") | ("TimetableDesign", "task_avail") => { "semicolon-separated 0/1 rows: \"1,1,0;0,1,1\"" } @@ -1212,6 +1216,12 @@ fn print_problem_help(canonical: &str, graph_type: Option<&str>) -> Result<()> { eprintln!(" --{:<16} {} ({})", flag_name, field.description, hint); } } + if canonical == "GraphPartitioning" { + eprintln!( + " --{:<16} Number of partitions in the balanced partitioning model (must be 2) (integer)", + "num-partitions" + ); + } } else { bail!("{}", crate::problem_name::unknown_problem_error(canonical)); } @@ -1762,6 +1772,23 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { ) } + "GraphPartitioning" => { + let usage = "pred create GraphPartitioning --graph 0-1,1-2,2-3,3-0 --num-partitions 2"; + let (graph, _) = + parse_graph(args).map_err(|e| anyhow::anyhow!("{e}\n\nUsage: {usage}"))?; + let num_partitions = args.num_partitions.ok_or_else(|| { + anyhow::anyhow!("GraphPartitioning requires --num-partitions\n\nUsage: {usage}") + })?; + anyhow::ensure!( + num_partitions == 2, + "GraphPartitioning currently models balanced bipartition only, so --num-partitions must be 2 (got {num_partitions})" + ); + ( + ser(GraphPartitioning::new(graph))?, + resolved_variant.clone(), + ) + } + // LongestPath "LongestPath" => { let usage = "pred create LongestPath --graph 0-1,0-2,1-3,2-3,2-4,3-5,4-5,4-6,5-6,1-6 --edge-lengths 3,2,4,1,5,2,3,2,4,1 --source-vertex 0 --target-vertex 6"; @@ -2397,13 +2424,11 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { let num_vars = args.num_vars.ok_or_else(|| { anyhow::anyhow!( "NonTautology requires --num-vars\n\n\ - Usage: pred create NonTautology --num-vars 3 --clauses \"1,2,3;-1,-2,-3\"" + Usage: pred create NonTautology --num-vars 3 --disjuncts \"1,2,3;-1,-2,-3\"" ) })?; - let clauses = parse_clauses(args)?; - let disjuncts: Vec> = clauses.into_iter().map(|c| c.literals).collect(); ( - ser(NonTautology::new(num_vars, disjuncts))?, + ser(NonTautology::new(num_vars, parse_disjuncts(args)?))?, resolved_variant.clone(), ) } @@ -7360,6 +7385,28 @@ fn parse_clauses(args: &CreateArgs) -> Result> { .collect() } +fn parse_disjuncts(args: &CreateArgs) -> Result>> { + let disjuncts_str = args + .disjuncts + .as_deref() + .or(args.clauses.as_deref()) + .ok_or_else(|| { + anyhow::anyhow!("NonTautology requires --disjuncts (e.g., \"1,2,3;-1,-2,-3\")") + })?; + + disjuncts_str + .split(';') + .map(|disjunct| { + disjunct + .trim() + .split(',') + .map(|s| s.trim().parse::()) + .collect::, _>>() + .map_err(anyhow::Error::from) + }) + .collect() +} + /// Parse `--sets` as semicolon-separated sets of comma-separated usize. /// E.g., "0,1;1,2;0,2" fn parse_sets(args: &CreateArgs) -> Result>> { @@ -9901,9 +9948,11 @@ mod tests { couplings: None, fields: None, clauses: None, + disjuncts: None, num_vars: None, matrix: None, k: None, + num_partitions: None, random: false, source_vertex: None, target_vertex: None, @@ -10843,6 +10892,85 @@ mod tests { assert!(err.contains("bound >= 1")); } + #[test] + fn test_create_graph_partitioning_with_num_partitions() { + use crate::dispatch::ProblemJsonOutput; + use problemreductions::models::graph::GraphPartitioning; + use problemreductions::topology::SimpleGraph; + + let cli = Cli::try_parse_from([ + "pred", + "create", + "GraphPartitioning", + "--graph", + "0-1,1-2,2-3,3-0", + "--num-partitions", + "2", + ]) + .unwrap(); + let args = match cli.command { + Commands::Create(args) => args, + _ => unreachable!(), + }; + + let output_path = temp_output_path("graph-partitioning-create"); + let out = OutputConfig { + output: Some(output_path.clone()), + quiet: true, + json: false, + auto_json: false, + }; + + create(&args, &out).unwrap(); + + let json = fs::read_to_string(&output_path).unwrap(); + let created: ProblemJsonOutput = serde_json::from_str(&json).unwrap(); + assert_eq!(created.problem_type, "GraphPartitioning"); + let problem: GraphPartitioning = serde_json::from_value(created.data).unwrap(); + assert_eq!(problem.num_vertices(), 4); + + let _ = fs::remove_file(output_path); + } + + #[test] + fn test_create_nontautology_with_disjuncts_flag() { + use crate::dispatch::ProblemJsonOutput; + use problemreductions::models::formula::NonTautology; + + let cli = Cli::try_parse_from([ + "pred", + "create", + "NonTautology", + "--num-vars", + "3", + "--disjuncts", + "1,2,3;-1,-2,-3", + ]) + .unwrap(); + let args = match cli.command { + Commands::Create(args) => args, + _ => unreachable!(), + }; + + let output_path = temp_output_path("non-tautology-create"); + let out = OutputConfig { + output: Some(output_path.clone()), + quiet: true, + json: false, + auto_json: false, + }; + + create(&args, &out).unwrap(); + + let json = fs::read_to_string(&output_path).unwrap(); + let created: ProblemJsonOutput = serde_json::from_str(&json).unwrap(); + assert_eq!(created.problem_type, "NonTautology"); + let problem: NonTautology = serde_json::from_value(created.data).unwrap(); + assert_eq!(problem.disjuncts(), &[vec![1, 2, 3], vec![-1, -2, -3]]); + + let _ = fs::remove_file(output_path); + } + #[test] fn test_create_consecutive_ones_matrix_augmentation_json() { use crate::dispatch::ProblemJsonOutput; diff --git a/problemreductions-cli/src/mcp/tools.rs b/problemreductions-cli/src/mcp/tools.rs index 5ed86c63e..e6a5df56e 100644 --- a/problemreductions-cli/src/mcp/tools.rs +++ b/problemreductions-cli/src/mcp/tools.rs @@ -1,6 +1,6 @@ use crate::util; use problemreductions::models::algebraic::QUBO; -use problemreductions::models::formula::{CNFClause, Satisfiability}; +use problemreductions::models::formula::{CNFClause, NonTautology, Satisfiability}; use problemreductions::models::graph::{ KClique, LongestCircuit, MaxCut, MaximumClique, MaximumIndependentSet, MaximumMatching, MinimumDominatingSet, MinimumSumMulticenter, MinimumVertexCover, SpinGlass, TravelingSalesman, @@ -70,7 +70,7 @@ pub struct CreateProblemParams { )] pub problem_type: String, #[schemars( - description = "Problem parameters as JSON object. Graph problems: {\"edges\": \"0-1,1-2\", \"weights\": \"1,2,3\"}. SAT: {\"num_vars\": 3, \"clauses\": \"1,2;-1,3\"}. QUBO: {\"matrix\": \"1,0.5;0.5,2\"}. KColoring: {\"edges\": \"0-1,1-2\", \"k\": 3}. KClique: {\"edges\": \"0-1,0-2,1-3,2-3,2-4,3-4\", \"k\": 3}. Factoring: {\"target\": 15, \"bits_m\": 4, \"bits_n\": 4}. Random graph: {\"random\": true, \"num_vertices\": 10, \"edge_prob\": 0.3}. Geometry graphs (use with MIS/KingsSubgraph etc.): {\"positions\": \"0,0;1,0;1,1\"}. UnitDiskGraph: {\"positions\": \"0.0,0.0;1.0,0.0\", \"radius\": 1.5}" + description = "Problem parameters as JSON object. Graph problems: {\"edges\": \"0-1,1-2\", \"weights\": \"1,2,3\"}. SAT: {\"num_vars\": 3, \"clauses\": \"1,2;-1,3\"}. NonTautology: {\"num_vars\": 2, \"disjuncts\": \"1,2;-1,-2\"}. QUBO: {\"matrix\": \"1,0.5;0.5,2\"}. KColoring: {\"edges\": \"0-1,1-2\", \"k\": 3}. KClique: {\"edges\": \"0-1,0-2,1-3,2-3,2-4,3-4\", \"k\": 3}. Factoring: {\"target\": 15, \"bits_m\": 4, \"bits_n\": 4}. Random graph: {\"random\": true, \"num_vertices\": 10, \"edge_prob\": 0.3}. Geometry graphs (use with MIS/KingsSubgraph etc.): {\"positions\": \"0,0;1,0;1,1\"}. UnitDiskGraph: {\"positions\": \"0.0,0.0;1.0,0.0\", \"radius\": 1.5}" )] pub params: serde_json::Value, } @@ -406,20 +406,8 @@ impl McpServer { if edge_lengths.iter().any(|&length| length <= 0) { anyhow::bail!("LongestCircuit edge lengths must be positive (> 0)"); } - let bound = params - .get("bound") - .and_then(|v| v.as_i64()) - .ok_or_else(|| anyhow::anyhow!("LongestCircuit requires 'bound'"))?; - let bound = i32::try_from(bound) - .map_err(|_| anyhow::anyhow!("LongestCircuit bound must fit in i32"))?; - if bound <= 0 { - anyhow::bail!("LongestCircuit bound must be positive (> 0)"); - } let variant = variant_map(&[("graph", "SimpleGraph"), ("weight", "i32")]); - ( - ser(LongestCircuit::new(graph, edge_lengths, bound))?, - variant, - ) + (ser(LongestCircuit::new(graph, edge_lengths))?, variant) } "KColoring" => { @@ -451,6 +439,16 @@ impl McpServer { let variant = BTreeMap::new(); (ser(Satisfiability::new(num_vars, clauses))?, variant) } + "NonTautology" => { + let num_vars = params + .get("num_vars") + .and_then(|v| v.as_u64()) + .map(|v| v as usize) + .ok_or_else(|| anyhow::anyhow!("NonTautology requires 'num_vars'"))?; + let disjuncts = parse_disjuncts_from_params(params)?; + let variant = BTreeMap::new(); + (ser(NonTautology::new(num_vars, disjuncts))?, variant) + } "KSatisfiability" => { let num_vars = params .get("num_vars") @@ -625,20 +623,8 @@ impl McpServer { } let graph = util::create_random_graph(num_vertices, edge_prob, seed); let edge_lengths = vec![1i32; graph.num_edges()]; - let bound = params - .get("bound") - .and_then(|v| v.as_i64()) - .unwrap_or(num_vertices.max(3) as i64); - let bound = i32::try_from(bound) - .map_err(|_| anyhow::anyhow!("LongestCircuit bound must fit in i32"))?; - if bound <= 0 { - anyhow::bail!("LongestCircuit bound must be positive (> 0)"); - } let variant = variant_map(&[("graph", "SimpleGraph"), ("weight", "i32")]); - ( - ser(LongestCircuit::new(graph, edge_lengths, bound))?, - variant, - ) + (ser(LongestCircuit::new(graph, edge_lengths))?, variant) } "SpinGlass" => { let edge_prob = params @@ -1436,6 +1422,28 @@ fn parse_clauses_from_params(params: &serde_json::Value) -> anyhow::Result anyhow::Result>> { + let disjuncts_str = params + .get("disjuncts") + .and_then(|v| v.as_str()) + .ok_or_else(|| { + anyhow::anyhow!("NonTautology requires 'disjuncts' parameter (e.g., \"1,2;-1,3\")") + })?; + + disjuncts_str + .split(';') + .map(|disjunct| { + disjunct + .trim() + .split(',') + .map(|s| s.trim().parse::()) + .collect::, _>>() + .map_err(anyhow::Error::from) + }) + .collect() +} + /// Parse `matrix` field from JSON params as semicolon-separated rows. fn parse_matrix_from_params(params: &serde_json::Value) -> anyhow::Result>> { let matrix_str = params @@ -1565,3 +1573,29 @@ fn solve_bundle_inner(bundle: ReductionBundle, solver_name: &str) -> anyhow::Res }); Ok(serde_json::to_string_pretty(&json)?) } + +#[cfg(test)] +mod tests { + use super::McpServer; + use crate::dispatch::ProblemJsonOutput; + use problemreductions::models::formula::NonTautology; + + #[test] + fn test_create_problem_inner_nontautology_uses_disjuncts() { + let server = McpServer::new(); + let output = server + .create_problem_inner( + "NonTautology", + &serde_json::json!({ + "num_vars": 3, + "disjuncts": "1,2,3;-1,-2,-3", + }), + ) + .unwrap(); + + let created: ProblemJsonOutput = serde_json::from_str(&output).unwrap(); + assert_eq!(created.problem_type, "NonTautology"); + let problem: NonTautology = serde_json::from_value(created.data).unwrap(); + assert_eq!(problem.disjuncts(), &[vec![1, 2, 3], vec![-1, -2, -3]]); + } +} diff --git a/problemreductions-cli/src/problem_name.rs b/problemreductions-cli/src/problem_name.rs index 835cc7a07..24a51eb73 100644 --- a/problemreductions-cli/src/problem_name.rs +++ b/problemreductions-cli/src/problem_name.rs @@ -35,6 +35,9 @@ pub fn resolve_alias(input: &str) -> String { if input.eq_ignore_ascii_case("ThreeMatroidIntersection") { return "ThreeMatroidIntersection".to_string(); } + if input.eq_ignore_ascii_case("GraphPartitioning") { + return "GraphPartitioning".to_string(); + } if let Some(pt) = problemreductions::registry::find_problem_type_by_alias(input) { return pt.canonical_name.to_string(); } diff --git a/src/lib.rs b/src/lib.rs index 3e4791a7b..2083070c1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -43,8 +43,9 @@ pub mod variant; pub mod prelude { // Problem types pub use crate::models::algebraic::{ - ConsecutiveOnesMatrixAugmentation, QuadraticAssignment, QuadraticCongruences, - SparseMatrixCompression, BMF, QUBO, + AlgebraicEquationsOverGF2, ConsecutiveOnesMatrixAugmentation, + MinimumWeightSolutionToLinearEquations, QuadraticAssignment, QuadraticCongruences, + SimultaneousIncongruences, SparseMatrixCompression, BMF, QUBO, }; pub use crate::models::formula::{ CNFClause, CircuitSAT, KSatisfiability, Maximum2Satisfiability, NAESatisfiability, @@ -54,12 +55,12 @@ pub mod prelude { pub use crate::models::graph::{ AcyclicPartition, BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation, BottleneckTravelingSalesman, BoundedComponentSpanningForest, - DirectedTwoCommodityIntegralFlow, DisjointConnectingPaths, GeneralizedHex, - HamiltonianCircuit, HamiltonianPath, HamiltonianPathBetweenTwoVertices, - IntegralFlowBundles, IntegralFlowHomologousArcs, IntegralFlowWithMultipliers, - IsomorphicSpanningTree, KClique, KthBestSpanningTree, LengthBoundedDisjointPaths, - LongestPath, MixedChinesePostman, SpinGlass, SteinerTree, StrongConnectivityAugmentation, - SubgraphIsomorphism, + DegreeConstrainedSpanningTree, DirectedTwoCommodityIntegralFlow, DisjointConnectingPaths, + GeneralizedHex, GraphPartitioning, HamiltonianCircuit, HamiltonianPath, + HamiltonianPathBetweenTwoVertices, IntegralFlowBundles, IntegralFlowHomologousArcs, + IntegralFlowWithMultipliers, IsomorphicSpanningTree, KClique, Kernel, KthBestSpanningTree, + LengthBoundedDisjointPaths, LongestPath, MixedChinesePostman, SpinGlass, SteinerTree, + StrongConnectivityAugmentation, SubgraphIsomorphism, }; pub use crate::models::graph::{ KColoring, LongestCircuit, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, @@ -68,8 +69,8 @@ pub mod prelude { MinimumFeedbackVertexSet, MinimumGeometricConnectedDominatingSet, MinimumGraphBandwidth, MinimumMultiwayCut, MinimumSumMulticenter, MinimumVertexCover, MonochromaticTriangle, MultipleChoiceBranching, MultipleCopyFileAllocation, OptimalLinearArrangement, - PartialFeedbackEdgeSet, PartitionIntoPathsOfLength2, PartitionIntoTriangles, - PathConstrainedNetworkFlow, RootedTreeArrangement, RuralPostman, + PartialFeedbackEdgeSet, PartitionIntoCliques, PartitionIntoPathsOfLength2, + PartitionIntoTriangles, PathConstrainedNetworkFlow, RootedTreeArrangement, RuralPostman, ShortestWeightConstrainedPath, SteinerTreeInGraphs, TravelingSalesman, UndirectedFlowLowerBounds, UndirectedTwoCommodityIntegralFlow, }; @@ -77,16 +78,16 @@ pub mod prelude { AdditionalKey, BinPacking, BoyceCoddNormalFormViolation, CapacityAssignment, CbqRelation, ConjunctiveBooleanQuery, ConjunctiveQueryFoldability, ConsistencyOfDatabaseFrequencyTables, CosineProductIntegration, EnsembleComputation, ExpectedRetrievalCost, Factoring, - FlowShopScheduling, GroupingBySwapping, JobShopScheduling, Knapsack, - LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, + FlowShopScheduling, GroupingBySwapping, IntegerExpressionMembership, JobShopScheduling, + Knapsack, LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, OpenShopScheduling, PaintShop, Partition, PreemptiveScheduling, ProductionPlanning, QueryArg, RectilinearPictureCompression, ResourceConstrainedScheduling, SchedulingWithIndividualDeadlines, SequencingToMinimizeMaximumCumulativeCost, - SequencingToMinimizeWeightedCompletionTime, SequencingToMinimizeWeightedTardiness, - SequencingWithDeadlinesAndSetUpTimes, SequencingWithReleaseTimesAndDeadlines, - SequencingWithinIntervals, ShortestCommonSupersequence, StackerCrane, StaffScheduling, - StringToStringCorrection, SubsetSum, SumOfSquaresPartition, Term, ThreePartition, - TimetableDesign, + SequencingToMinimizeTardyTaskWeight, SequencingToMinimizeWeightedCompletionTime, + SequencingToMinimizeWeightedTardiness, SequencingWithDeadlinesAndSetUpTimes, + SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, + ShortestCommonSupersequence, StackerCrane, StaffScheduling, StringToStringCorrection, + SubsetProduct, SubsetSum, SumOfSquaresPartition, Term, ThreePartition, TimetableDesign, }; pub use crate::models::set::{ ComparativeContainment, ConsecutiveSets, ExactCoverBy3Sets, IntegerKnapsack, diff --git a/src/models/algebraic/simultaneous_incongruences.rs b/src/models/algebraic/simultaneous_incongruences.rs index 5aee90f37..5dc6263d1 100644 --- a/src/models/algebraic/simultaneous_incongruences.rs +++ b/src/models/algebraic/simultaneous_incongruences.rs @@ -62,7 +62,7 @@ pub struct SimultaneousIncongruences { /// Maximum lcm value we will compute in full; if the lcm exceeds this cap we /// return this value to keep the brute-force search space manageable. -const MAX_LCM: u128 = 1_000_000; +pub(crate) const MAX_LCM: u128 = 1_000_000; fn lcm128(a: u128, b: u128) -> u128 { if a == 0 || b == 0 { diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs index 75aac7a59..9faae18d6 100644 --- a/src/models/formula/ksat.rs +++ b/src/models/formula/ksat.rs @@ -12,6 +12,42 @@ use serde::{Deserialize, Serialize}; use super::CNFClause; +pub(crate) fn first_n_odd_primes(count: usize) -> Vec { + let mut primes = Vec::with_capacity(count); + let mut candidate = 3u64; + + while primes.len() < count { + if is_prime(candidate) { + primes.push(candidate); + } + candidate += 2; + } + + primes +} + +fn is_prime(candidate: u64) -> bool { + if candidate < 2 { + return false; + } + if candidate == 2 { + return true; + } + if candidate.is_multiple_of(2) { + return false; + } + + let mut divisor = 3u64; + while divisor * divisor <= candidate { + if candidate.is_multiple_of(divisor) { + return false; + } + divisor += 2; + } + + true +} + inventory::submit! { ProblemSchemaEntry { name: "KSatisfiability", @@ -147,6 +183,23 @@ impl KSatisfiability { self.clauses().iter().map(|c| c.len()).sum() } + pub fn simultaneous_incongruences_num_incongruences(&self) -> usize { + first_n_odd_primes(self.num_vars) + .into_iter() + .map(|prime| usize::try_from(prime - 2).expect("prime fits in usize")) + .sum::() + + self.num_clauses() + } + + pub fn simultaneous_incongruences_bound(&self) -> usize { + first_n_odd_primes(self.num_vars) + .into_iter() + .try_fold(1usize, |product, prime| { + product.checked_mul(usize::try_from(prime).expect("prime fits in usize")) + }) + .expect("simultaneous incongruences bound must fit in usize") + } + /// Count satisfied clauses for an assignment. pub fn count_satisfied(&self, assignment: &[bool]) -> usize { self.clauses diff --git a/src/models/graph/graph_partitioning.rs b/src/models/graph/graph_partitioning.rs new file mode 100644 index 000000000..f69aadd2b --- /dev/null +++ b/src/models/graph/graph_partitioning.rs @@ -0,0 +1,164 @@ +//! GraphPartitioning problem implementation. +//! +//! The Graph Partitioning (Minimum Bisection) problem asks for a balanced partition +//! of vertices into two equal halves minimizing the number of crossing edges. + +use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension}; +use crate::topology::{Graph, SimpleGraph}; +use crate::traits::Problem; +use crate::types::Min; +use serde::{Deserialize, Serialize}; + +inventory::submit! { + ProblemSchemaEntry { + name: "GraphPartitioning", + display_name: "Graph Partitioning", + aliases: &[], + dimensions: &[ + VariantDimension::new("graph", "SimpleGraph", &["SimpleGraph"]), + ], + module_path: module_path!(), + description: "Find minimum cut balanced bisection of a graph", + fields: &[ + FieldInfo { name: "graph", type_name: "G", description: "The undirected graph G=(V,E)" }, + ], + } +} + +/// The Graph Partitioning (Minimum Bisection) problem. +/// +/// Given an undirected graph G = (V, E) with |V| = n (even), +/// partition V into two disjoint sets A and B with |A| = |B| = n/2, +/// minimizing the number of edges crossing the partition. +/// +/// # Type Parameters +/// +/// * `G` - The graph type (e.g., `SimpleGraph`) +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::graph::GraphPartitioning; +/// use problemreductions::topology::SimpleGraph; +/// use problemreductions::types::Min; +/// use problemreductions::{Problem, Solver, BruteForce}; +/// +/// // Square graph: 0-1, 1-2, 2-3, 3-0 +/// let graph = SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)]); +/// let problem = GraphPartitioning::new(graph); +/// +/// let solver = BruteForce::new(); +/// let solutions = solver.find_all_witnesses(&problem); +/// +/// // Minimum bisection of a 4-cycle: cut = 2 +/// for sol in solutions { +/// let size = problem.evaluate(&sol); +/// assert_eq!(size, Min(Some(2))); +/// } +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct GraphPartitioning { + /// The underlying graph structure. + graph: G, +} + +impl GraphPartitioning { + /// Create a GraphPartitioning problem from a graph. + /// + /// # Arguments + /// * `graph` - The undirected graph to partition + pub fn new(graph: G) -> Self { + Self { graph } + } + + /// Get a reference to the underlying graph. + pub fn graph(&self) -> &G { + &self.graph + } + + /// Get the number of vertices in the underlying graph. + pub fn num_vertices(&self) -> usize { + self.graph.num_vertices() + } + + /// Get the number of edges in the underlying graph. + pub fn num_edges(&self) -> usize { + self.graph.num_edges() + } +} + +impl Problem for GraphPartitioning +where + G: Graph + crate::variant::VariantParam, +{ + const NAME: &'static str = "GraphPartitioning"; + type Value = Min; + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![G] + } + + fn dims(&self) -> Vec { + vec![2; self.graph.num_vertices()] + } + + fn evaluate(&self, config: &[usize]) -> Min { + let n = self.graph.num_vertices(); + if config.len() != n { + return Min(None); + } + if config.iter().any(|&part| part >= 2) { + return Min(None); + } + // Balanced bisection requires even n + if !n.is_multiple_of(2) { + return Min(None); + } + // Check balanced: exactly n/2 vertices in partition 1 + let count_ones = config.iter().filter(|&&x| x == 1).count(); + if count_ones != n / 2 { + return Min(None); + } + // Count crossing edges + let mut cut = 0i32; + for (u, v) in self.graph.edges() { + if config[u] != config[v] { + cut += 1; + } + } + Min(Some(cut)) + } +} + +crate::declare_variants! { + default GraphPartitioning => "2^num_vertices", +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_model_example_specs() -> Vec { + use crate::topology::SimpleGraph; + // Two triangles connected by 3 edges; balanced cut = 3 + vec![crate::example_db::specs::ModelExampleSpec { + id: "graph_partitioning", + instance: Box::new(GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + ))), + optimal_config: vec![0, 0, 0, 1, 1, 1], + optimal_value: serde_json::json!(3), + }] +} + +#[cfg(test)] +#[path = "../../unit_tests/models/graph/graph_partitioning.rs"] +mod tests; diff --git a/src/models/graph/isomorphic_spanning_tree.rs b/src/models/graph/isomorphic_spanning_tree.rs index b340b6c59..ecf69e417 100644 --- a/src/models/graph/isomorphic_spanning_tree.rs +++ b/src/models/graph/isomorphic_spanning_tree.rs @@ -4,9 +4,10 @@ //! contains a spanning tree isomorphic to T. This is a classical NP-complete //! problem (Garey & Johnson, ND8) that generalizes Hamiltonian Path. -use crate::registry::{FieldInfo, ProblemSchemaEntry}; +use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension}; use crate::topology::{Graph, SimpleGraph}; use crate::traits::Problem; +use crate::variant::VariantParam; use serde::{Deserialize, Serialize}; inventory::submit! { @@ -14,11 +15,13 @@ inventory::submit! { name: "IsomorphicSpanningTree", display_name: "Isomorphic Spanning Tree", aliases: &[], - dimensions: &[], + dimensions: &[ + VariantDimension::new("graph", "SimpleGraph", &["SimpleGraph"]), + ], module_path: module_path!(), description: "Does graph G contain a spanning tree isomorphic to tree T?", fields: &[ - FieldInfo { name: "graph", type_name: "SimpleGraph", description: "The host graph G" }, + FieldInfo { name: "graph", type_name: "G", description: "The host graph G" }, FieldInfo { name: "tree", type_name: "SimpleGraph", description: "The target tree T (must be a tree with |V(T)| = |V(G)|)" }, ], } @@ -30,6 +33,9 @@ inventory::submit! { /// |V| = |V_T|, determine if there exists a bijection π: V_T → V such that /// for every edge {u, v} in E_T, {π(u), π(v)} is an edge in E. /// +/// The configuration encodes an isomorphism as a permutation of the vertices of +/// `graph`: `config[i]` is the graph vertex that tree vertex `i` maps to. +/// /// # Example /// /// ``` @@ -48,34 +54,37 @@ inventory::submit! { /// assert!(sol.is_some()); /// ``` #[derive(Debug, Clone, Serialize, Deserialize)] -pub struct IsomorphicSpanningTree { - graph: SimpleGraph, +#[serde(bound(deserialize = "G: serde::Deserialize<'de>"))] +pub struct IsomorphicSpanningTree { + graph: G, tree: SimpleGraph, } -impl IsomorphicSpanningTree { +impl IsomorphicSpanningTree { /// Create a new IsomorphicSpanningTree problem. /// /// # Panics /// /// Panics if |V(G)| != |V(T)| or if T is not a tree (not connected or /// wrong number of edges). - pub fn new(graph: SimpleGraph, tree: SimpleGraph) -> Self { + pub fn new(graph: G, tree: SimpleGraph) -> Self { let n = graph.num_vertices(); assert_eq!( n, tree.num_vertices(), "graph and tree must have the same number of vertices" ); - if n > 0 { - assert_eq!(tree.num_edges(), n - 1, "tree must have exactly n-1 edges"); - assert!(Self::is_connected(&tree), "tree must be connected"); - } + assert_eq!( + tree.num_edges(), + n.saturating_sub(1), + "tree must have exactly n-1 edges" + ); + assert!(is_connected(&tree), "tree must be connected"); Self { graph, tree } } /// Get a reference to the host graph. - pub fn graph(&self) -> &SimpleGraph { + pub fn graph(&self) -> &G { &self.graph } @@ -90,79 +99,86 @@ impl IsomorphicSpanningTree { } /// Get the number of edges in the host graph. - pub fn num_graph_edges(&self) -> usize { + pub fn num_edges(&self) -> usize { self.graph.num_edges() } - /// Get the number of edges in the target tree. - pub fn num_tree_edges(&self) -> usize { - self.tree.num_edges() - } - - /// Check if a graph is connected using BFS. - fn is_connected(graph: &SimpleGraph) -> bool { - let n = graph.num_vertices(); - if n == 0 { - return true; - } - let mut visited = vec![false; n]; - let mut queue = std::collections::VecDeque::new(); - visited[0] = true; - queue.push_back(0); - let mut count = 1; - while let Some(v) = queue.pop_front() { - for u in graph.neighbors(v) { - if !visited[u] { - visited[u] = true; - count += 1; - queue.push_back(u); - } - } - } - count == n + /// Get the edges of the target tree. + pub fn tree_edges(&self) -> Vec<(usize, usize)> { + self.tree.edges() } } -impl Problem for IsomorphicSpanningTree { +impl Problem for IsomorphicSpanningTree +where + G: Graph + VariantParam, +{ const NAME: &'static str = "IsomorphicSpanningTree"; type Value = crate::types::Or; + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![G] + } + fn dims(&self) -> Vec { - let n = self.graph.num_vertices(); - vec![n; n] + vec![self.graph.num_vertices(); self.graph.num_vertices()] } fn evaluate(&self, config: &[usize]) -> crate::types::Or { - crate::types::Or({ - let n = self.graph.num_vertices(); - if config.len() != n { - return crate::types::Or(false); - } + crate::types::Or(is_valid_isomorphic_spanning_tree( + &self.graph, + &self.tree, + config, + )) + } +} - // Check that config is a valid permutation: all values in 0..n, all distinct - let mut seen = vec![false; n]; - for &v in config { - if v >= n || seen[v] { - return crate::types::Or(false); - } - seen[v] = true; - } +fn is_valid_isomorphic_spanning_tree( + graph: &G, + tree: &SimpleGraph, + config: &[usize], +) -> bool { + let n = graph.num_vertices(); + if config.len() != n { + return false; + } - // Check that every tree edge maps to a graph edge under the permutation - // config[i] = π(i): tree vertex i maps to graph vertex config[i] - for (u, v) in self.tree.edges() { - if !self.graph.has_edge(config[u], config[v]) { - return crate::types::Or(false); - } - } + let mut seen = vec![false; n]; + for &v in config { + if v >= n || seen[v] { + return false; + } + seen[v] = true; + } + + tree.edges() + .into_iter() + .all(|(u, v)| graph.has_edge(config[u], config[v])) +} - true - }) +fn is_connected(graph: &SimpleGraph) -> bool { + let n = graph.num_vertices(); + if n == 0 { + return true; } - fn variant() -> Vec<(&'static str, &'static str)> { - crate::variant_params![] + let mut visited = vec![false; n]; + let mut queue = std::collections::VecDeque::new(); + visited[0] = true; + queue.push_back(0); + let mut count = 1; + + while let Some(v) = queue.pop_front() { + for u in graph.neighbors(v) { + if !visited[u] { + visited[u] = true; + count += 1; + queue.push_back(u); + } + } } + + count == n } #[cfg(feature = "example-db")] @@ -179,7 +195,7 @@ pub(crate) fn canonical_model_example_specs() -> Vec "factorial(num_vertices)", + default IsomorphicSpanningTree => "num_vertices^num_vertices", } #[cfg(test)] diff --git a/src/models/graph/mod.rs b/src/models/graph/mod.rs index 4bb2e365d..f5f395945 100644 --- a/src/models/graph/mod.rs +++ b/src/models/graph/mod.rs @@ -87,6 +87,7 @@ pub(crate) mod directed_hamiltonian_path; pub(crate) mod directed_two_commodity_integral_flow; pub(crate) mod disjoint_connecting_paths; pub(crate) mod generalized_hex; +pub(crate) mod graph_partitioning; pub(crate) mod hamiltonian_circuit; pub(crate) mod hamiltonian_path; pub(crate) mod hamiltonian_path_between_two_vertices; @@ -163,6 +164,7 @@ pub use directed_hamiltonian_path::DirectedHamiltonianPath; pub use directed_two_commodity_integral_flow::DirectedTwoCommodityIntegralFlow; pub use disjoint_connecting_paths::DisjointConnectingPaths; pub use generalized_hex::GeneralizedHex; +pub use graph_partitioning::GraphPartitioning; pub use hamiltonian_circuit::HamiltonianCircuit; pub use hamiltonian_path::HamiltonianPath; pub use hamiltonian_path_between_two_vertices::HamiltonianPathBetweenTwoVertices; @@ -305,5 +307,6 @@ pub(crate) fn canonical_model_example_specs() -> Vec usize { + self.num_subsets() + } + /// Get the subsets. pub fn subsets(&self) -> &[[usize; 3]] { &self.subsets } + /// Get the sets. + pub fn sets(&self) -> &[[usize; 3]] { + self.subsets() + } + /// Get a specific subset. pub fn get_subset(&self, index: usize) -> Option<&[usize; 3]> { self.subsets.get(index) diff --git a/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs b/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs new file mode 100644 index 000000000..c931682fc --- /dev/null +++ b/src/rules/exactcoverby3sets_algebraicequationsovergf2.rs @@ -0,0 +1,83 @@ +//! Reduction from ExactCoverBy3Sets to AlgebraicEquationsOverGF2. + +use crate::models::algebraic::AlgebraicEquationsOverGF2; +use crate::models::set::ExactCoverBy3Sets; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionX3CToAlgebraicEquationsOverGF2 { + target: AlgebraicEquationsOverGF2, +} + +impl ReductionResult for ReductionX3CToAlgebraicEquationsOverGF2 { + type Source = ExactCoverBy3Sets; + type Target = AlgebraicEquationsOverGF2; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + num_vars = "num_sets", +})] +impl ReduceTo for ExactCoverBy3Sets { + type Result = ReductionX3CToAlgebraicEquationsOverGF2; + + fn reduce_to(&self) -> Self::Result { + let mut sets_per_element = vec![Vec::new(); self.universe_size()]; + for (set_index, set) in self.sets().iter().enumerate() { + for &element in set { + sets_per_element[element].push(set_index); + } + } + + let mut equations = Vec::new(); + for containing_sets in sets_per_element { + let mut linear_equation = containing_sets + .iter() + .map(|&set_index| vec![set_index]) + .collect::>(); + linear_equation.push(vec![]); + equations.push(linear_equation); + + for left in 0..containing_sets.len() { + for right in (left + 1)..containing_sets.len() { + equations.push(vec![vec![containing_sets[left], containing_sets[right]]]); + } + } + } + + ReductionX3CToAlgebraicEquationsOverGF2 { + target: AlgebraicEquationsOverGF2::new(self.num_sets(), equations) + .expect("reduction produces valid equations"), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "exactcoverby3sets_to_algebraicequationsovergf2", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, AlgebraicEquationsOverGF2>( + ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]), + SolutionPair { + source_config: vec![1, 1, 0], + target_config: vec![1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/exactcoverby3sets_algebraicequationsovergf2.rs"] +mod tests; diff --git a/src/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs b/src/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs new file mode 100644 index 000000000..752c43d01 --- /dev/null +++ b/src/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs @@ -0,0 +1,78 @@ +//! Reduction from ExactCoverBy3Sets to MinimumWeightSolutionToLinearEquations. +//! +//! The incidence matrix has one row per universe element and one column per set. +//! Selecting a set corresponds to setting its variable to 1. The equation +//! system enforces that each universe element is covered exactly once, and the +//! sparsity bound enforces that at most `|U|/3` sets are selected. + +use crate::models::algebraic::MinimumWeightSolutionToLinearEquations; +use crate::models::set::ExactCoverBy3Sets; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionX3CToMinimumWeightSolutionToLinearEquations { + target: MinimumWeightSolutionToLinearEquations, +} + +impl ReductionResult for ReductionX3CToMinimumWeightSolutionToLinearEquations { + type Source = ExactCoverBy3Sets; + type Target = MinimumWeightSolutionToLinearEquations; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + num_variables = "num_sets", + num_equations = "universe_size", +})] +impl ReduceTo for ExactCoverBy3Sets { + type Result = ReductionX3CToMinimumWeightSolutionToLinearEquations; + + fn reduce_to(&self) -> Self::Result { + let mut coefficients = vec![vec![0i64; self.num_sets()]; self.universe_size()]; + for (set_index, set) in self.sets().iter().enumerate() { + for &element in set { + coefficients[element][set_index] = 1; + } + } + + ReductionX3CToMinimumWeightSolutionToLinearEquations { + target: MinimumWeightSolutionToLinearEquations::new( + coefficients, + vec![1; self.universe_size()], + ), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "exactcoverby3sets_to_minimumweightsolutiontolinearequations", + build: || { + crate::example_db::specs::rule_example_with_witness::< + _, + MinimumWeightSolutionToLinearEquations, + >( + ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]), + SolutionPair { + source_config: vec![1, 1, 0], + target_config: vec![1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs"] +mod tests; diff --git a/src/rules/exactcoverby3sets_subsetproduct.rs b/src/rules/exactcoverby3sets_subsetproduct.rs new file mode 100644 index 000000000..3b6aa896e --- /dev/null +++ b/src/rules/exactcoverby3sets_subsetproduct.rs @@ -0,0 +1,97 @@ +//! Reduction from ExactCoverBy3Sets to SubsetProduct. +//! +//! Assign a distinct prime to each universe element. Each triple becomes the +//! product of its three primes, and the target is the product of all universe +//! primes. Unique factorization then makes exact covers correspond exactly to +//! subsets whose product matches the target. + +use crate::models::formula::ksat::first_n_odd_primes; +use crate::models::misc::SubsetProduct; +use crate::models::set::ExactCoverBy3Sets; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use num_bigint::BigUint; +use num_traits::One; + +#[derive(Debug, Clone)] +pub struct ReductionX3CToSubsetProduct { + target: SubsetProduct, +} + +impl ReductionResult for ReductionX3CToSubsetProduct { + type Source = ExactCoverBy3Sets; + type Target = SubsetProduct; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +fn product_biguint(values: I) -> BigUint +where + I: IntoIterator, +{ + values.into_iter().fold(BigUint::one(), |product, value| { + product * BigUint::from(value) + }) +} + +fn assigned_primes(universe_size: usize) -> Vec { + match universe_size { + 0 => Vec::new(), + 1 => vec![2], + _ => { + let mut primes = Vec::with_capacity(universe_size); + primes.push(2); + primes.extend(first_n_odd_primes(universe_size - 1)); + primes + } + } +} + +#[reduction(overhead = { + num_elements = "num_sets", +})] +impl ReduceTo for ExactCoverBy3Sets { + type Result = ReductionX3CToSubsetProduct; + + fn reduce_to(&self) -> Self::Result { + let primes = assigned_primes(self.universe_size()); + let values = self + .sets() + .iter() + .map(|set| product_biguint(set.iter().map(|&element| primes[element]))) + .collect(); + let target = product_biguint(primes.iter().copied()); + + ReductionX3CToSubsetProduct { + target: SubsetProduct::new(values, target), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "exactcoverby3sets_to_subsetproduct", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, SubsetProduct>( + ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]), + SolutionPair { + source_config: vec![1, 1, 0], + target_config: vec![1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/exactcoverby3sets_subsetproduct.rs"] +mod tests; diff --git a/src/rules/graphpartitioning_ilp.rs b/src/rules/graphpartitioning_ilp.rs new file mode 100644 index 000000000..94b280286 --- /dev/null +++ b/src/rules/graphpartitioning_ilp.rs @@ -0,0 +1,114 @@ +//! Reduction from GraphPartitioning to ILP (Integer Linear Programming). +//! +//! Uses the standard balanced-cut ILP formulation: +//! - Variables: `x_v` for vertex-side assignment and `y_e` for edge-crossing indicators +//! - Constraints: one balance equality plus two linking inequalities per edge +//! - Objective: minimize the number of crossing edges + +use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; +use crate::models::graph::GraphPartitioning; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing GraphPartitioning to ILP. +/// +/// Variable layout (all binary): +/// - `x_v` for `v = 0..n-1`: vertex `v` belongs to side `B` +/// - `y_e` for `e = 0..m-1`: edge `e` crosses the partition +#[derive(Debug, Clone)] +pub struct ReductionGraphPartitioningToILP { + target: ILP, + num_vertices: usize, +} + +impl ReductionResult for ReductionGraphPartitioningToILP { + type Source = GraphPartitioning; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.num_vertices].to_vec() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices + num_edges", + num_constraints = "2 * num_edges + 1", + } +)] +impl ReduceTo> for GraphPartitioning { + type Result = ReductionGraphPartitioningToILP; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + let edges = self.graph().edges(); + let m = edges.len(); + let num_vars = n + m; + + let mut constraints = Vec::with_capacity(2 * m + 1); + + let balance_terms: Vec<(usize, f64)> = (0..n).map(|v| (v, 1.0)).collect(); + constraints.push(LinearConstraint::eq(balance_terms, n as f64 / 2.0)); + + for (edge_idx, (u, v)) in edges.iter().enumerate() { + let y_var = n + edge_idx; + constraints.push(LinearConstraint::ge( + vec![(y_var, 1.0), (*u, -1.0), (*v, 1.0)], + 0.0, + )); + constraints.push(LinearConstraint::ge( + vec![(y_var, 1.0), (*u, 1.0), (*v, -1.0)], + 0.0, + )); + } + + let objective: Vec<(usize, f64)> = (0..m).map(|edge_idx| (n + edge_idx, 1.0)).collect(); + let target = ILP::new(num_vars, constraints, objective, ObjectiveSense::Minimize); + + ReductionGraphPartitioningToILP { + target, + num_vertices: n, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "graphpartitioning_to_ilp", + build: || { + let source = GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + )); + crate::example_db::specs::rule_example_with_witness::<_, ILP>( + source, + SolutionPair { + source_config: vec![0, 0, 0, 1, 1, 1], + target_config: vec![0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/graphpartitioning_ilp.rs"] +mod tests; diff --git a/src/rules/graphpartitioning_maxcut.rs b/src/rules/graphpartitioning_maxcut.rs new file mode 100644 index 000000000..0bf31b369 --- /dev/null +++ b/src/rules/graphpartitioning_maxcut.rs @@ -0,0 +1,108 @@ +//! Reduction from GraphPartitioning to MaxCut on a weighted complete graph. + +use crate::models::graph::{GraphPartitioning, MaxCut}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing GraphPartitioning to MaxCut. +#[derive(Debug, Clone)] +pub struct ReductionGPToMaxCut { + target: MaxCut, +} + +#[cfg(any(test, feature = "example-db"))] +const ISSUE_EXAMPLE_WITNESS: [usize; 6] = [0, 0, 0, 1, 1, 1]; + +impl ReductionResult for ReductionGPToMaxCut { + type Source = GraphPartitioning; + type Target = MaxCut; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[cfg(any(test, feature = "example-db"))] +fn issue_example() -> GraphPartitioning { + GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + )) +} + +fn complete_graph_edges_and_weights(graph: &SimpleGraph) -> (Vec<(usize, usize)>, Vec) { + let num_vertices = graph.num_vertices(); + let p = penalty_weight(graph.num_edges()); + let mut edges = Vec::new(); + let mut weights = Vec::new(); + + for u in 0..num_vertices { + for v in (u + 1)..num_vertices { + edges.push((u, v)); + weights.push(if graph.has_edge(u, v) { p - 1 } else { p }); + } + } + + (edges, weights) +} + +fn penalty_weight(num_edges: usize) -> i32 { + i32::try_from(num_edges) + .ok() + .and_then(|num_edges| num_edges.checked_add(1)) + .expect("GraphPartitioning -> MaxCut penalty exceeds i32 range") +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_edges = "num_vertices * (num_vertices - 1) / 2", + } +)] +impl ReduceTo> for GraphPartitioning { + type Result = ReductionGPToMaxCut; + + fn reduce_to(&self) -> Self::Result { + let (edges, weights) = complete_graph_edges_and_weights(self.graph()); + let target = MaxCut::new(SimpleGraph::new(self.num_vertices(), edges), weights); + + ReductionGPToMaxCut { target } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "graphpartitioning_to_maxcut", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, MaxCut>( + issue_example(), + SolutionPair { + source_config: ISSUE_EXAMPLE_WITNESS.to_vec(), + target_config: ISSUE_EXAMPLE_WITNESS.to_vec(), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/graphpartitioning_maxcut.rs"] +mod tests; diff --git a/src/rules/graphpartitioning_qubo.rs b/src/rules/graphpartitioning_qubo.rs new file mode 100644 index 000000000..8e32846c9 --- /dev/null +++ b/src/rules/graphpartitioning_qubo.rs @@ -0,0 +1,99 @@ +//! Reduction from GraphPartitioning to QUBO. +//! +//! Uses the penalty-method QUBO +//! H = sum_(u,v in E) (x_u + x_v - 2 x_u x_v) + P (sum_i x_i - n/2)^2 +//! with P = |E| + 1 so any imbalanced partition is dominated by a balanced one. + +use crate::models::algebraic::QUBO; +use crate::models::graph::GraphPartitioning; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing GraphPartitioning to QUBO. +#[derive(Debug, Clone)] +pub struct ReductionGraphPartitioningToQUBO { + target: QUBO, +} + +impl ReductionResult for ReductionGraphPartitioningToQUBO { + type Source = GraphPartitioning; + type Target = QUBO; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { num_vars = "num_vertices" })] +impl ReduceTo> for GraphPartitioning { + type Result = ReductionGraphPartitioningToQUBO; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + let penalty = self.num_edges() as f64 + 1.0; + let mut matrix = vec![vec![0.0f64; n]; n]; + let mut degrees = vec![0usize; n]; + let edges = self.graph().edges(); + + for &(u, v) in &edges { + degrees[u] += 1; + degrees[v] += 1; + } + + for (i, row) in matrix.iter_mut().enumerate() { + row[i] = degrees[i] as f64 + penalty * (1.0 - n as f64); + for value in row.iter_mut().skip(i + 1) { + *value = 2.0 * penalty; + } + } + + for (u, v) in edges { + let (lo, hi) = if u < v { (u, v) } else { (v, u) }; + matrix[lo][hi] -= 2.0; + } + + ReductionGraphPartitioningToQUBO { + target: QUBO::from_matrix(matrix), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "graphpartitioning_to_qubo", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, QUBO>( + GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + )), + SolutionPair { + source_config: vec![0, 0, 0, 1, 1, 1], + target_config: vec![0, 0, 0, 1, 1, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/graphpartitioning_qubo.rs"] +mod tests; diff --git a/src/rules/hamiltonianpath_degreeconstrainedspanningtree.rs b/src/rules/hamiltonianpath_degreeconstrainedspanningtree.rs new file mode 100644 index 000000000..e6fc6c548 --- /dev/null +++ b/src/rules/hamiltonianpath_degreeconstrainedspanningtree.rs @@ -0,0 +1,174 @@ +//! Reduction from HamiltonianPath to DegreeConstrainedSpanningTree. +//! +//! A spanning tree with maximum degree 2 is exactly a Hamiltonian path. + +use crate::models::graph::{DegreeConstrainedSpanningTree, HamiltonianPath}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing HamiltonianPath to DegreeConstrainedSpanningTree. +#[derive(Debug, Clone)] +pub struct ReductionHamiltonianPathToDegreeConstrainedSpanningTree { + target: DegreeConstrainedSpanningTree, +} + +impl ReductionResult for ReductionHamiltonianPathToDegreeConstrainedSpanningTree { + type Source = HamiltonianPath; + type Target = DegreeConstrainedSpanningTree; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + extract_hamiltonian_order(self.target.graph(), target_solution) + } +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_edges = "num_edges", + } +)] +impl ReduceTo> for HamiltonianPath { + type Result = ReductionHamiltonianPathToDegreeConstrainedSpanningTree; + + fn reduce_to(&self) -> Self::Result { + let target = DegreeConstrainedSpanningTree::new( + SimpleGraph::new(self.graph().num_vertices(), self.graph().edges()), + 2, + ); + ReductionHamiltonianPathToDegreeConstrainedSpanningTree { target } + } +} + +fn extract_hamiltonian_order(graph: &SimpleGraph, target_solution: &[usize]) -> Vec { + let num_vertices = graph.num_vertices(); + if num_vertices == 0 { + return vec![]; + } + if num_vertices == 1 { + return vec![0]; + } + + let edges = graph.edges(); + if target_solution.len() != edges.len() { + return vec![]; + } + + let mut adjacency = vec![Vec::new(); num_vertices]; + for ((u, v), &selected) in edges.iter().copied().zip(target_solution.iter()) { + if selected != 1 { + continue; + } + adjacency[u].push(v); + adjacency[v].push(u); + } + + let mut endpoints: Vec = adjacency + .iter() + .enumerate() + .filter_map(|(vertex, neighbors)| (neighbors.len() == 1).then_some(vertex)) + .collect(); + endpoints.sort_unstable(); + if endpoints.len() != 2 { + return vec![]; + } + + let mut order = Vec::with_capacity(num_vertices); + let mut visited = vec![false; num_vertices]; + let mut previous = None; + let mut current = endpoints[0]; + + loop { + if visited[current] { + return vec![]; + } + visited[current] = true; + order.push(current); + + let next = adjacency[current] + .iter() + .copied() + .find(|&neighbor| Some(neighbor) != previous && !visited[neighbor]); + match next { + Some(next_vertex) => { + previous = Some(current); + current = next_vertex; + } + None => break, + } + } + + if order.len() == num_vertices { + order + } else { + vec![] + } +} + +#[cfg(feature = "example-db")] +fn edge_config_for_path(graph: &SimpleGraph, path: &[usize]) -> Vec { + let selected_edges: Vec<(usize, usize)> = path + .windows(2) + .map(|window| (window[0], window[1])) + .collect(); + graph + .edges() + .into_iter() + .map(|(u, v)| { + usize::from( + selected_edges + .iter() + .any(|&(a, b)| (a == u && b == v) || (a == v && b == u)), + ) + }) + .collect() +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + fn source_example() -> HamiltonianPath { + HamiltonianPath::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 3), + (2, 3), + (3, 4), + (3, 5), + (4, 2), + (5, 1), + ], + )) + } + + vec![crate::example_db::specs::RuleExampleSpec { + id: "hamiltonianpath_to_degreeconstrainedspanningtree", + build: || { + let source_config = vec![0, 2, 4, 3, 1, 5]; + let source = source_example(); + let reduction = + ReduceTo::>::reduce_to(&source); + let target_config = + edge_config_for_path(reduction.target_problem().graph(), &source_config); + crate::example_db::specs::rule_example_with_witness::< + _, + DegreeConstrainedSpanningTree, + >( + source, + crate::export::SolutionPair { + source_config, + target_config, + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltonianpath_degreeconstrainedspanningtree.rs"] +mod tests; diff --git a/src/rules/hamiltonianpath_isomorphicspanningtree.rs b/src/rules/hamiltonianpath_isomorphicspanningtree.rs index 481b24541..a5a96e829 100644 --- a/src/rules/hamiltonianpath_isomorphicspanningtree.rs +++ b/src/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -1,4 +1,4 @@ -//! Reduction from HamiltonianPath to IsomorphicSpanningTree. +//! Reduction from HamiltonianPath to IsomorphicSpanningTree. //! //! A Hamiltonian path in G exists iff G has a spanning tree isomorphic to the //! path graph P_n. The reduction keeps G unchanged as the host graph and @@ -9,15 +9,15 @@ use crate::reduction; use crate::rules::traits::{ReduceTo, ReductionResult}; use crate::topology::SimpleGraph; -/// Result of reducing HamiltonianPath to IsomorphicSpanningTree. +/// Result of reducing HamiltonianPath to IsomorphicSpanningTree. #[derive(Debug, Clone)] pub struct ReductionHPToIST { - target: IsomorphicSpanningTree, + target: IsomorphicSpanningTree, } impl ReductionResult for ReductionHPToIST { type Source = HamiltonianPath; - type Target = IsomorphicSpanningTree; + type Target = IsomorphicSpanningTree; fn target_problem(&self) -> &Self::Target { &self.target @@ -40,7 +40,7 @@ impl ReductionResult for ReductionHPToIST { num_tree_edges = "num_vertices - 1", } )] -impl ReduceTo for HamiltonianPath { +impl ReduceTo> for HamiltonianPath { type Result = ReductionHPToIST; fn reduce_to(&self) -> Self::Result { @@ -66,7 +66,10 @@ pub(crate) fn canonical_rule_example_specs() -> Vec( + crate::example_db::specs::rule_example_with_witness::< + _, + IsomorphicSpanningTree, + >( source, SolutionPair { source_config: vec![0, 1, 2, 3, 4], diff --git a/src/rules/hamiltonianpathbetweentwovertices_longestpath.rs b/src/rules/hamiltonianpathbetweentwovertices_longestpath.rs new file mode 100644 index 000000000..bc177227e --- /dev/null +++ b/src/rules/hamiltonianpathbetweentwovertices_longestpath.rs @@ -0,0 +1,129 @@ +//! Reduction from HamiltonianPathBetweenTwoVertices to LongestPath. +//! +//! A Hamiltonian s-t path in G has length n-1 edges (the maximum possible for +//! any simple path). Setting all edge lengths to unit weight and the same +//! source/target vertices, the longest path of length n-1 exactly corresponds +//! to a Hamiltonian s-t path. + +use crate::models::graph::{HamiltonianPathBetweenTwoVertices, LongestPath}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::types::One; + +/// Result of reducing HamiltonianPathBetweenTwoVertices to LongestPath. +#[derive(Debug, Clone)] +pub struct ReductionHPBTVToLP { + target: LongestPath, + /// Cached edge list from the graph, indexed by edge position. + edges: Vec<(usize, usize)>, + source_vertex: usize, + num_vertices: usize, +} + +impl ReductionResult for ReductionHPBTVToLP { + type Source = HamiltonianPathBetweenTwoVertices; + type Target = LongestPath; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + /// Extract a vertex-permutation solution from an edge-selection solution. + /// + /// The target solution is a binary vector over edges. We walk the selected + /// edges from the source vertex to reconstruct the vertex ordering. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let n = self.num_vertices; + + // Build adjacency from selected edges + let mut adj: Vec> = vec![Vec::new(); n]; + for (idx, &selected) in target_solution.iter().enumerate() { + if selected == 1 { + let (u, v) = self.edges[idx]; + adj[u].push(v); + adj[v].push(u); + } + } + + // Walk the path from source + let mut path = Vec::with_capacity(n); + let mut current = self.source_vertex; + let mut prev = usize::MAX; // sentinel for "no previous" + path.push(current); + + while path.len() < n { + let next = adj[current] + .iter() + .find(|&&neighbor| neighbor != prev) + .copied(); + match next { + Some(next_vertex) => { + prev = current; + current = next_vertex; + path.push(current); + } + None => break, + } + } + + path + } +} + +#[reduction(overhead = { + num_vertices = "num_vertices", + num_edges = "num_edges", +})] +impl ReduceTo> for HamiltonianPathBetweenTwoVertices { + type Result = ReductionHPBTVToLP; + + fn reduce_to(&self) -> Self::Result { + let graph = self.graph().clone(); + let num_edges = graph.num_edges(); + let edges = graph.edges(); + let edge_lengths = vec![One; num_edges]; + + let target = LongestPath::new( + graph, + edge_lengths, + self.source_vertex(), + self.target_vertex(), + ); + + ReductionHPBTVToLP { + target, + edges, + source_vertex: self.source_vertex(), + num_vertices: self.num_vertices(), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "hamiltonianpathbetweentwovertices_to_longestpath", + build: || { + // Path graph 0-1-2-3-4 with s=0, t=4 + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4)]), + 0, + 4, + ); + crate::example_db::specs::rule_example_with_witness::<_, LongestPath>( + source, + SolutionPair { + source_config: vec![0, 1, 2, 3, 4], + target_config: vec![1, 1, 1, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltonianpathbetweentwovertices_longestpath.rs"] +mod tests; diff --git a/src/rules/isomorphicspanningtree_ilp.rs b/src/rules/isomorphicspanningtree_ilp.rs index 9eefbe6a5..dad7a8126 100644 --- a/src/rules/isomorphicspanningtree_ilp.rs +++ b/src/rules/isomorphicspanningtree_ilp.rs @@ -7,7 +7,7 @@ use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; use crate::models::graph::IsomorphicSpanningTree; use crate::reduction; use crate::rules::traits::{ReduceTo, ReductionResult}; -use crate::topology::Graph; +use crate::topology::{Graph, SimpleGraph}; #[derive(Debug, Clone)] pub struct ReductionISTToILP { @@ -16,7 +16,7 @@ pub struct ReductionISTToILP { } impl ReductionResult for ReductionISTToILP { - type Source = IsomorphicSpanningTree; + type Source = IsomorphicSpanningTree; type Target = ILP; fn target_problem(&self) -> &ILP { @@ -39,10 +39,10 @@ impl ReductionResult for ReductionISTToILP { #[reduction( overhead = { num_vars = "num_vertices * num_vertices", - num_constraints = "2 * num_vertices + 2 * num_tree_edges * num_vertices * num_vertices", + num_constraints = "2 * num_vertices + 2 * (num_vertices - 1) * num_vertices * num_vertices", } )] -impl ReduceTo> for IsomorphicSpanningTree { +impl ReduceTo> for IsomorphicSpanningTree { type Result = ReductionISTToILP; fn reduce_to(&self) -> Self::Result { diff --git a/src/rules/kcoloring_partitionintocliques.rs b/src/rules/kcoloring_partitionintocliques.rs new file mode 100644 index 000000000..156f8c781 --- /dev/null +++ b/src/rules/kcoloring_partitionintocliques.rs @@ -0,0 +1,90 @@ +//! Reduction from KColoring to PartitionIntoCliques via complement graphs. +//! +//! A proper k-coloring of G is exactly a partition of V into k independent +//! sets, which become k cliques in the complement graph. + +use crate::models::graph::{KColoring, PartitionIntoCliques}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::variant::KN; + +/// Result of reducing KColoring to PartitionIntoCliques. +#[derive(Debug, Clone)] +pub struct ReductionKColoringToPartitionIntoCliques { + target: PartitionIntoCliques, +} + +impl ReductionResult for ReductionKColoringToPartitionIntoCliques { + type Source = KColoring; + type Target = PartitionIntoCliques; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + /// Solution extraction is the identity: color classes become clique classes. + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +fn complement_edges(graph: &SimpleGraph) -> Vec<(usize, usize)> { + let n = graph.num_vertices(); + let mut edges = Vec::new(); + for u in 0..n { + for v in (u + 1)..n { + if !graph.has_edge(u, v) { + edges.push((u, v)); + } + } + } + edges +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_edges = "num_vertices * (num_vertices - 1) / 2 - num_edges", + } +)] +impl ReduceTo> for KColoring { + type Result = ReductionKColoringToPartitionIntoCliques; + + fn reduce_to(&self) -> Self::Result { + let target = PartitionIntoCliques::new( + SimpleGraph::new(self.graph().num_vertices(), complement_edges(self.graph())), + self.num_colors(), + ); + ReductionKColoringToPartitionIntoCliques { target } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "kcoloring_to_partitionintocliques", + build: || { + let source = KColoring::::with_k( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 3), (2, 3), (2, 4), (3, 4)]), + 3, + ); + crate::example_db::specs::rule_example_with_witness::< + _, + PartitionIntoCliques, + >( + source, + SolutionPair { + source_config: vec![0, 1, 1, 0, 2], + target_config: vec![0, 1, 1, 0, 2], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/kcoloring_partitionintocliques.rs"] +mod tests; diff --git a/src/rules/ksatisfiability_kernel.rs b/src/rules/ksatisfiability_kernel.rs new file mode 100644 index 000000000..c09f9aca9 --- /dev/null +++ b/src/rules/ksatisfiability_kernel.rs @@ -0,0 +1,109 @@ +//! Reduction from 3-SAT to Kernel. +//! +//! This is Chvatal's 1973 construction using variable digons and clause +//! 3-cycles with arcs to literal vertices. + +use crate::models::formula::KSatisfiability; +use crate::models::graph::Kernel; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::DirectedGraph; +use crate::variant::K3; + +/// Result of reducing 3-SAT to Kernel. +#[derive(Debug, Clone)] +pub struct Reduction3SatToKernel { + target: Kernel, + source_num_vars: usize, +} + +impl ReductionResult for Reduction3SatToKernel { + type Source = KSatisfiability; + type Target = Kernel; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + (0..self.source_num_vars) + .map(|i| usize::from(target_solution.get(2 * i).copied().unwrap_or(0) == 1)) + .collect() + } +} + +fn literal_vertex(literal: i32) -> usize { + let variable = literal.unsigned_abs() as usize - 1; + if literal > 0 { + 2 * variable + } else { + 2 * variable + 1 + } +} + +#[reduction( + overhead = { + num_vertices = "2 * num_vars + 3 * num_clauses", + num_arcs = "2 * num_vars + 6 * num_clauses", + } +)] +impl ReduceTo for KSatisfiability { + type Result = Reduction3SatToKernel; + + fn reduce_to(&self) -> Self::Result { + let num_vars = self.num_vars(); + let num_clauses = self.num_clauses(); + let mut arcs = Vec::with_capacity(2 * num_vars + 6 * num_clauses); + + for variable in 0..num_vars { + let positive = 2 * variable; + let negative = positive + 1; + arcs.push((positive, negative)); + arcs.push((negative, positive)); + } + + for (clause_index, clause) in self.clauses().iter().enumerate() { + let clause_base = 2 * num_vars + 3 * clause_index; + arcs.push((clause_base, clause_base + 1)); + arcs.push((clause_base + 1, clause_base + 2)); + arcs.push((clause_base + 2, clause_base)); + + for (literal_index, &literal) in clause.literals.iter().enumerate() { + arcs.push((clause_base + literal_index, literal_vertex(literal))); + } + } + + Reduction3SatToKernel { + target: Kernel::new(DirectedGraph::new(2 * num_vars + 3 * num_clauses, arcs)), + source_num_vars: num_vars, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_kernel", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, Kernel>( + KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ), + SolutionPair { + source_config: vec![1, 1, 1], + target_config: vec![1, 0, 1, 0, 1, 0, 0, 0, 0, 0, 1, 0], + }, + ) + }, + }] +} +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_kernel.rs"] +mod tests; diff --git a/src/rules/ksatisfiability_simultaneousincongruences.rs b/src/rules/ksatisfiability_simultaneousincongruences.rs new file mode 100644 index 000000000..484d50585 --- /dev/null +++ b/src/rules/ksatisfiability_simultaneousincongruences.rs @@ -0,0 +1,219 @@ +//! Reduction from 3-SAT to Simultaneous Incongruences. +//! +//! Uses distinct odd primes to encode variable assignments via residues +//! 1 (true) and 2 (false), then forbids each clause's unique falsifying +//! residue class via the Chinese Remainder Theorem. + +use std::collections::BTreeMap; + +use crate::models::algebraic::simultaneous_incongruences::MAX_LCM; +use crate::models::algebraic::SimultaneousIncongruences; +use crate::models::formula::{ksat::first_n_odd_primes, CNFClause, KSatisfiability}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::variant::K3; + +#[derive(Debug, Clone)] +pub struct Reduction3SATToSimultaneousIncongruences { + target: SimultaneousIncongruences, + variable_primes: Vec, +} + +impl ReductionResult for Reduction3SATToSimultaneousIncongruences { + type Source = KSatisfiability; + type Target = SimultaneousIncongruences; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let x = target_solution.first().copied().unwrap_or(0) as u64; + self.variable_primes + .iter() + .map(|&prime| if x % prime == 1 { 1 } else { 0 }) + .collect() + } +} + +fn falsifying_residue(literal: i32) -> u64 { + if literal > 0 { + 2 + } else { + 1 + } +} + +fn modular_inverse(value: u64, modulus: u64) -> u64 { + let mut t = 0i128; + let mut new_t = 1i128; + let mut r = modulus as i128; + let mut new_r = value as i128; + + while new_r != 0 { + let quotient = r / new_r; + (t, new_t) = (new_t, t - quotient * new_t); + (r, new_r) = (new_r, r - quotient * new_r); + } + + assert_eq!(r, 1, "value and modulus must be coprime"); + if t < 0 { + t += modulus as i128; + } + t as u64 +} + +fn crt_residue(congruences: &[(u64, u64)]) -> (u64, u64) { + let modulus = congruences.iter().fold(1u64, |product, &(m, _)| { + product + .checked_mul(m) + .expect("CRT modulus product overflow") + }); + + let residue = congruences + .iter() + .fold(0u128, |acc, &(modulus_i, residue_i)| { + let partial = modulus / modulus_i; + let inverse = modular_inverse(partial % modulus_i, modulus_i); + acc + residue_i as u128 * partial as u128 * inverse as u128 + }) + % modulus as u128; + + (residue as u64, modulus) +} + +fn clause_bad_residue(clause: &CNFClause, variable_primes: &[u64]) -> (u64, u64) { + let mut residue_by_var = BTreeMap::new(); + let mut contradictory_var = None; + + for &literal in &clause.literals { + let var_index = literal.unsigned_abs() as usize - 1; + let residue = falsifying_residue(literal); + + match residue_by_var.insert(var_index, residue) { + Some(existing) if existing != residue => { + contradictory_var = Some(var_index); + residue_by_var.insert(var_index, 0); + break; + } + Some(existing) => { + residue_by_var.insert(var_index, existing); + } + None => {} + } + } + + if let Some(var_index) = contradictory_var { + for &literal in &clause.literals { + let candidate = literal.unsigned_abs() as usize - 1; + if candidate != var_index { + residue_by_var + .entry(candidate) + .or_insert_with(|| falsifying_residue(literal)); + } + } + } + + let congruences = residue_by_var + .into_iter() + .map(|(var_index, residue)| { + ( + *variable_primes + .get(var_index) + .expect("clause variable index must be within num_vars"), + residue, + ) + }) + .collect::>(); + + crt_residue(&congruences) +} + +fn ensure_prime_product_within_lcm_cap(variable_primes: &[u64]) { + let mut product = 1u128; + for &prime in variable_primes { + product = product.checked_mul(prime as u128).unwrap_or_else(|| { + panic!( + "3-SAT -> SimultaneousIncongruences requires the variable-prime product to fit within the target model's LCM cap ({MAX_LCM}); num_vars={} overflows while multiplying primes", + variable_primes.len() + ) + }); + if product > MAX_LCM { + panic!( + "3-SAT -> SimultaneousIncongruences requires the variable-prime product to fit within the target model's LCM cap ({MAX_LCM}); num_vars={} yields prime product {product}", + variable_primes.len() + ); + } + } +} + +#[reduction(overhead = { + num_pairs = "simultaneous_incongruences_num_incongruences", +})] +impl ReduceTo for KSatisfiability { + type Result = Reduction3SATToSimultaneousIncongruences; + + fn reduce_to(&self) -> Self::Result { + let variable_primes = first_n_odd_primes(self.num_vars()); + ensure_prime_product_within_lcm_cap(&variable_primes); + + let mut pairs = Vec::new(); + + for &prime in &variable_primes { + // Use (prime, prime) to forbid x ≡ 0 (mod prime), since the + // model requires a ≥ 1. Note: prime % prime = 0, so this is + // equivalent to forbidding residue 0. + pairs.push((prime, prime)); + for residue in 3..prime { + pairs.push((residue, prime)); + } + } + + for clause in self.clauses() { + let (bad_residue, clause_modulus) = clause_bad_residue(clause, &variable_primes); + // The model requires a >= 1. Use modulus instead of 0 since + // modulus % modulus = 0, achieving the same incongruence. + let a = if bad_residue == 0 { + clause_modulus + } else { + bad_residue + }; + pairs.push((a, clause_modulus)); + } + + Reduction3SATToSimultaneousIncongruences { + target: SimultaneousIncongruences::new(pairs) + .expect("reduction produces valid incongruences"), + variable_primes, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "ksatisfiability_to_simultaneous_incongruences", + build: || { + let source = KSatisfiability::::new( + 2, + vec![ + CNFClause::new(vec![1, 2, 2]), + CNFClause::new(vec![-1, 2, 2]), + ], + ); + crate::example_db::specs::rule_example_with_witness::<_, SimultaneousIncongruences>( + source, + SolutionPair { + source_config: vec![1, 1], + target_config: vec![1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_simultaneousincongruences.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 6789c92a8..5edde0754 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -11,11 +11,16 @@ pub use registry::{EdgeCapabilities, ReductionEntry, ReductionOverhead}; pub(crate) mod circuit_spinglass; mod closestvectorproblem_qubo; pub(crate) mod coloring_qubo; +pub(crate) mod exactcoverby3sets_algebraicequationsovergf2; pub(crate) mod exactcoverby3sets_maximumsetpacking; +pub(crate) mod exactcoverby3sets_minimumweightsolutiontolinearequations; pub(crate) mod exactcoverby3sets_staffscheduling; +pub(crate) mod exactcoverby3sets_subsetproduct; pub(crate) mod factoring_circuit; mod graph; pub(crate) mod graph_helpers; +pub(crate) mod graphpartitioning_maxcut; +pub(crate) mod graphpartitioning_qubo; pub(crate) mod hamiltoniancircuit_biconnectivityaugmentation; pub(crate) mod hamiltoniancircuit_bottlenecktravelingsalesman; pub(crate) mod hamiltoniancircuit_hamiltonianpath; @@ -26,18 +31,23 @@ pub(crate) mod hamiltoniancircuit_stackercrane; pub(crate) mod hamiltoniancircuit_strongconnectivityaugmentation; pub(crate) mod hamiltoniancircuit_travelingsalesman; pub(crate) mod hamiltonianpath_consecutiveonessubmatrix; +pub(crate) mod hamiltonianpath_degreeconstrainedspanningtree; pub(crate) mod hamiltonianpath_isomorphicspanningtree; +pub(crate) mod hamiltonianpathbetweentwovertices_longestpath; pub(crate) mod ilp_i32_ilp_bool; pub(crate) mod kclique_balancedcompletebipartitesubgraph; pub(crate) mod kclique_conjunctivebooleanquery; pub(crate) mod kclique_subgraphisomorphism; mod kcoloring_casts; +pub(crate) mod kcoloring_partitionintocliques; pub(crate) mod kcoloring_twodimensionalconsecutivesets; mod knapsack_qubo; mod ksatisfiability_casts; pub(crate) mod ksatisfiability_kclique; +pub(crate) mod ksatisfiability_kernel; pub(crate) mod ksatisfiability_minimumvertexcover; pub(crate) mod ksatisfiability_qubo; +pub(crate) mod ksatisfiability_simultaneousincongruences; pub(crate) mod ksatisfiability_subsetsum; pub(crate) mod longestcommonsubsequence_maximumindependentset; pub(crate) mod maxcut_minimumcutintoboundedsets; @@ -59,11 +69,15 @@ pub(crate) mod minimumvertexcover_minimumfeedbackvertexset; pub(crate) mod minimumvertexcover_minimumhittingset; pub(crate) mod minimumvertexcover_minimumsetcovering; pub(crate) mod naesatisfiability_maxcut; +pub(crate) mod naesatisfiability_setsplitting; pub(crate) mod paintshop_qubo; pub(crate) mod partition_binpacking; pub(crate) mod partition_cosineproductintegration; pub(crate) mod partition_knapsack; pub(crate) mod partition_multiprocessorscheduling; +pub(crate) mod partition_openshopscheduling; +pub(crate) mod partition_productionplanning; +pub(crate) mod partition_sequencingtominimizetardytaskweight; pub(crate) mod partition_sequencingwithinintervals; pub(crate) mod partition_shortestweightconstrainedpath; pub(crate) mod partition_subsetsum; @@ -75,11 +89,14 @@ pub(crate) mod sat_ksat; pub(crate) mod sat_maximumindependentset; pub(crate) mod sat_minimumdominatingset; pub(crate) mod satisfiability_naesatisfiability; +pub(crate) mod satisfiability_nontautology; mod spinglass_casts; pub(crate) mod spinglass_maxcut; pub(crate) mod spinglass_qubo; pub(crate) mod subsetsum_capacityassignment; pub(crate) mod subsetsum_closestvectorproblem; +pub(crate) mod subsetsum_integerexpressionmembership; +pub(crate) mod subsetsum_partition; #[cfg(test)] pub(crate) mod test_helpers; pub(crate) mod threepartition_flowshopscheduling; @@ -137,6 +154,8 @@ pub(crate) mod factoring_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod flowshopscheduling_ilp; #[cfg(feature = "ilp-solver")] +pub(crate) mod graphpartitioning_ilp; +#[cfg(feature = "ilp-solver")] pub(crate) mod hamiltonianpath_ilp; #[cfg(feature = "ilp-solver")] mod ilp_bool_ilp_i32; @@ -324,6 +343,11 @@ pub(crate) fn canonical_rule_example_specs() -> Vec Vec Vec Vec Vec &SetSplitting { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + assert!( + target_solution.len() >= self.num_source_variables, + "SetSplitting solution has {} variables but source requires {}", + target_solution.len(), + self.num_source_variables, + ); + target_solution[..self.num_source_variables].to_vec() + } +} + +fn literal_element_index(lit: i32, num_vars: usize) -> usize { + let var_index = lit.unsigned_abs() as usize - 1; + if lit > 0 { + var_index + } else { + num_vars + var_index + } +} + +#[reduction( + overhead = { + universe_size = "2 * num_vars", + num_subsets = "num_vars + num_clauses", + } +)] +impl ReduceTo for NAESatisfiability { + type Result = ReductionNAESATToSetSplitting; + + fn reduce_to(&self) -> Self::Result { + let num_vars = self.num_vars(); + let mut subsets = Vec::with_capacity(num_vars + self.num_clauses()); + + for var_index in 0..num_vars { + subsets.push(vec![var_index, num_vars + var_index]); + } + + for clause in self.clauses() { + subsets.push( + clause + .literals + .iter() + .map(|&lit| literal_element_index(lit, num_vars)) + .collect(), + ); + } + + ReductionNAESATToSetSplitting { + target: SetSplitting::new(2 * num_vars, subsets), + num_source_variables: num_vars, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "naesatisfiability_to_setsplitting", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, SetSplitting>( + NAESatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ), + SolutionPair { + source_config: vec![1, 1, 1], + target_config: vec![1, 1, 1, 0, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/naesatisfiability_setsplitting.rs"] +mod tests; diff --git a/src/rules/partition_openshopscheduling.rs b/src/rules/partition_openshopscheduling.rs new file mode 100644 index 000000000..309bd441d --- /dev/null +++ b/src/rules/partition_openshopscheduling.rs @@ -0,0 +1,129 @@ +//! Reduction from Partition to Open Shop Scheduling. + +use crate::models::misc::{OpenShopScheduling, Partition}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionPartitionToOpenShopScheduling { + target: OpenShopScheduling, +} + +impl ReductionResult for ReductionPartitionToOpenShopScheduling { + type Source = Partition; + type Target = OpenShopScheduling; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let num_elements = self.target.num_jobs().saturating_sub(1); + let mut source_config = vec![0; num_elements]; + let Some(orders) = self.target.decode_orders(target_solution) else { + return source_config; + }; + if num_elements == 0 { + return source_config; + } + + let special_job = num_elements; + let half_sum = self.target.processing_times()[special_job][0]; + + // Find the middle machine and compute start times + let makespan_orders = &orders; + let n = self.target.num_jobs(); + let m = self.target.num_machines(); + + // Simulate to get start times + let mut machine_avail = vec![0usize; m]; + let mut job_avail = vec![0usize; n]; + let mut start_times = vec![vec![0usize; m]; n]; + + // Schedule by processing the orders + let mut cursor = vec![0usize; m]; + let total_ops = n * m; + for _ in 0..total_ops { + let mut best: Option<(usize, usize, usize)> = None; // (start, machine, job) + for (mi, order) in makespan_orders.iter().enumerate() { + if cursor[mi] < order.len() { + let job = order[cursor[mi]]; + let start = machine_avail[mi].max(job_avail[job]); + if best.is_none_or(|(bs, _, _)| start < bs) { + best = Some((start, mi, job)); + } + } + } + let (start, mi, job) = best.expect("schedule incomplete"); + start_times[job][mi] = start; + let end = start + self.target.processing_times()[job][mi]; + machine_avail[mi] = end; + job_avail[job] = end; + cursor[mi] += 1; + } + + // Find the middle machine where the special job starts at half_sum + let middle_machine = (0..m) + .find(|&machine| start_times[special_job][machine] == half_sum) + .unwrap_or_else(|| { + let mut machines: Vec = (0..m).collect(); + machines.sort_by_key(|&machine| (start_times[special_job][machine], machine)); + machines[m / 2] + }); + let pivot = start_times[special_job][middle_machine]; + + for (job, slot) in source_config.iter_mut().enumerate() { + let completion = start_times[job][middle_machine] + + self.target.processing_times()[job][middle_machine]; + if completion <= pivot { + *slot = 1; + } + } + + source_config + } +} + +#[reduction(overhead = { + num_jobs = "num_elements + 1", + num_machines = "3", +})] +impl ReduceTo for Partition { + type Result = ReductionPartitionToOpenShopScheduling; + + fn reduce_to(&self) -> Self::Result { + let half_sum = self.total_sum() as usize / 2; + let mut processing_times: Vec> = self + .sizes() + .iter() + .map(|&size| vec![size as usize; 3]) + .collect(); + processing_times.push(vec![half_sum; 3]); + + ReductionPartitionToOpenShopScheduling { + target: OpenShopScheduling::new(3, processing_times), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "partition_to_open_shop_scheduling", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, OpenShopScheduling>( + Partition::new(vec![1, 2, 3]), + SolutionPair { + source_config: vec![0, 0, 1], + target_config: vec![0, 1, 2, 3, 0, 1, 2, 3, 2, 3, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/partition_openshopscheduling.rs"] +mod tests; diff --git a/src/rules/partition_productionplanning.rs b/src/rules/partition_productionplanning.rs new file mode 100644 index 000000000..c4ddcd3d3 --- /dev/null +++ b/src/rules/partition_productionplanning.rs @@ -0,0 +1,85 @@ +//! Reduction from Partition to Production Planning. + +use crate::models::misc::{Partition, ProductionPlanning}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +#[derive(Debug, Clone)] +pub struct ReductionPartitionToProductionPlanning { + target: ProductionPlanning, +} + +impl ReductionResult for ReductionPartitionToProductionPlanning { + type Source = Partition; + type Target = ProductionPlanning; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution + .iter() + .take(self.target.num_periods().saturating_sub(1)) + .map(|&production| usize::from(production > 0)) + .collect() + } +} + +#[reduction(overhead = { + num_periods = "num_elements + 1", +})] +impl ReduceTo for Partition { + type Result = ReductionPartitionToProductionPlanning; + + fn reduce_to(&self) -> Self::Result { + let half_floor = self.total_sum() / 2; + let half_ceil = half_floor + (self.total_sum() % 2); + let mut demands = vec![0; self.num_elements()]; + demands.push(half_ceil); + + let mut capacities = self.sizes().to_vec(); + capacities.push(0); + + let mut setup_costs = self.sizes().to_vec(); + setup_costs.push(0); + + let production_costs = vec![0; self.num_elements() + 1]; + let inventory_costs = vec![0; self.num_elements() + 1]; + + let num_periods = self.num_elements() + 1; + ReductionPartitionToProductionPlanning { + target: ProductionPlanning::new( + num_periods, + demands, + capacities, + setup_costs, + production_costs, + inventory_costs, + half_floor, + ), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "partition_to_production_planning", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, ProductionPlanning>( + Partition::new(vec![3, 5, 2, 4, 6]), + SolutionPair { + source_config: vec![0, 0, 0, 1, 1], + target_config: vec![0, 0, 0, 4, 6, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/partition_productionplanning.rs"] +mod tests; diff --git a/src/rules/partition_sequencingtominimizetardytaskweight.rs b/src/rules/partition_sequencingtominimizetardytaskweight.rs new file mode 100644 index 000000000..f47be5bc8 --- /dev/null +++ b/src/rules/partition_sequencingtominimizetardytaskweight.rs @@ -0,0 +1,95 @@ +//! Reduction from Partition to Sequencing to Minimize Tardy Task Weight. + +use crate::models::misc::{Partition, SequencingToMinimizeTardyTaskWeight}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +/// Result of reducing Partition to SequencingToMinimizeTardyTaskWeight. +#[derive(Debug, Clone)] +pub struct ReductionPartitionToSequencingToMinimizeTardyTaskWeight { + target: SequencingToMinimizeTardyTaskWeight, +} + +impl ReductionPartitionToSequencingToMinimizeTardyTaskWeight { + fn decode_schedule(&self, target_solution: &[usize]) -> Vec { + let n = self.target.num_tasks(); + assert_eq!( + target_solution.len(), + n, + "target solution length must equal target num_tasks" + ); + + // The target model uses direct permutation encoding (dims = [n; n]). + // Each position is a task index; the solver returns a valid permutation. + target_solution.to_vec() + } +} + +impl ReductionResult for ReductionPartitionToSequencingToMinimizeTardyTaskWeight { + type Source = Partition; + type Target = SequencingToMinimizeTardyTaskWeight; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let schedule = self.decode_schedule(target_solution); + let mut source_config = vec![1; self.target.num_tasks()]; + let mut completion_time = 0u64; + + for task in schedule { + completion_time = completion_time + .checked_add(self.target.lengths()[task]) + .expect("completion time overflowed u64"); + if completion_time <= self.target.deadlines()[task] { + source_config[task] = 0; + } + } + + source_config + } +} + +#[reduction(overhead = { + num_tasks = "num_elements", +})] +impl ReduceTo for Partition { + type Result = ReductionPartitionToSequencingToMinimizeTardyTaskWeight; + + fn reduce_to(&self) -> Self::Result { + let common_deadline = self.total_sum() / 2; + let lengths = self.sizes().to_vec(); + let weights = self.sizes().to_vec(); + let deadlines = vec![common_deadline; self.num_elements()]; + + ReductionPartitionToSequencingToMinimizeTardyTaskWeight { + target: SequencingToMinimizeTardyTaskWeight::new(lengths, weights, deadlines), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "partition_to_sequencing_to_minimize_tardy_task_weight", + build: || { + crate::example_db::specs::rule_example_with_witness::< + _, + SequencingToMinimizeTardyTaskWeight, + >( + Partition::new(vec![3, 1, 1, 2, 2, 1]), + SolutionPair { + source_config: vec![1, 0, 0, 1, 0, 0], + target_config: vec![1, 2, 4, 5, 0, 3], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/partition_sequencingtominimizetardytaskweight.rs"] +mod tests; diff --git a/src/rules/satisfiability_nontautology.rs b/src/rules/satisfiability_nontautology.rs new file mode 100644 index 000000000..be900a4a0 --- /dev/null +++ b/src/rules/satisfiability_nontautology.rs @@ -0,0 +1,77 @@ +//! Reduction from Satisfiability to NonTautology via negation. +//! +//! Negating a CNF formula with De Morgan's law turns each clause into a DNF +//! disjunct whose literals all have their signs flipped. + +use crate::models::formula::{NonTautology, Satisfiability}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; + +/// Result of reducing SAT to NonTautology. +#[derive(Debug, Clone)] +pub struct ReductionSATToNonTautology { + target: NonTautology, +} + +impl ReductionResult for ReductionSATToNonTautology { + type Source = Satisfiability; + type Target = NonTautology; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + num_vars = "num_vars", + num_disjuncts = "num_clauses", +})] +impl ReduceTo for Satisfiability { + type Result = ReductionSATToNonTautology; + + fn reduce_to(&self) -> Self::Result { + let disjuncts = self + .clauses() + .iter() + .map(|clause| clause.literals.iter().map(|&lit| -lit).collect()) + .collect(); + + ReductionSATToNonTautology { + target: NonTautology::new(self.num_vars(), disjuncts), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "satisfiability_to_nontautology", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, NonTautology>( + Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![-2, -3]), + ], + ), + SolutionPair { + source_config: vec![1, 0, 1], + target_config: vec![1, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/satisfiability_nontautology.rs"] +mod tests; diff --git a/src/rules/subsetsum_integerexpressionmembership.rs b/src/rules/subsetsum_integerexpressionmembership.rs new file mode 100644 index 000000000..dd3bef7d3 --- /dev/null +++ b/src/rules/subsetsum_integerexpressionmembership.rs @@ -0,0 +1,99 @@ +use crate::models::misc::SubsetSum; +use crate::models::misc::{IntExpr, IntegerExpressionMembership}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use num_traits::ToPrimitive; + +#[derive(Debug, Clone)] +pub struct ReductionSubsetSumToIntegerExpressionMembership { + target: IntegerExpressionMembership, +} + +impl ReductionResult for ReductionSubsetSumToIntegerExpressionMembership { + type Source = SubsetSum; + type Target = IntegerExpressionMembership; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + // Union choice 0 = left = Atom(1) = exclude, choice 1 = right = Atom(s_i+1) = include. + // This maps directly to SubsetSum's 0/1 include/exclude encoding. + target_solution.to_vec() + } +} + +/// Build a left-associative chain of `Sum` nodes over the given union nodes. +/// +/// For n items with sizes s_0, ..., s_{n-1}, each item becomes +/// `Union(Atom(1), Atom(s_i + 1))`. The chain is built as: +/// `Sum(Sum(...Sum(Union_0, Union_1), Union_2), ..., Union_{n-1})`. +/// +/// DFS order visits Union_0 first, then Union_1, etc., so config[i] +/// corresponds to item i. +fn build_expression(sizes: &[u64]) -> IntExpr { + assert!( + !sizes.is_empty(), + "SubsetSum must have at least one element" + ); + + let make_union = |s: u64| -> IntExpr { + IntExpr::Union(Box::new(IntExpr::Atom(1)), Box::new(IntExpr::Atom(s + 1))) + }; + + let mut expr = make_union(sizes[0]); + for &s in &sizes[1..] { + expr = IntExpr::Sum(Box::new(expr), Box::new(make_union(s))); + } + expr +} + +#[reduction(overhead = { + num_union_nodes = "num_elements", +})] +impl ReduceTo for SubsetSum { + type Result = ReductionSubsetSumToIntegerExpressionMembership; + + fn reduce_to(&self) -> Self::Result { + let sizes: Vec = self + .sizes() + .iter() + .map(|size| size.to_u64().unwrap()) + .collect(); + + let shift = u64::try_from(self.num_elements()) + .expect("SubsetSum -> IntegerExpressionMembership requires num_elements to fit in u64"); + let target = self.target().to_u64().unwrap().checked_add(shift).expect( + "SubsetSum -> IntegerExpressionMembership requires shifted target to fit in u64", + ); + + let expr = build_expression(&sizes); + + ReductionSubsetSumToIntegerExpressionMembership { + target: IntegerExpressionMembership::new(expr, target), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "subsetsum_to_integerexpressionmembership", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, IntegerExpressionMembership>( + SubsetSum::new(vec![1u32, 5, 6, 8], 11u32), + SolutionPair { + source_config: vec![0, 1, 1, 0], + target_config: vec![0, 1, 1, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/subsetsum_integerexpressionmembership.rs"] +mod tests; diff --git a/src/rules/subsetsum_partition.rs b/src/rules/subsetsum_partition.rs new file mode 100644 index 000000000..4bb333f87 --- /dev/null +++ b/src/rules/subsetsum_partition.rs @@ -0,0 +1,113 @@ +//! Reduction from Subset Sum to Partition. + +use crate::models::misc::{Partition, SubsetSum}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use num_bigint::BigUint; +use num_traits::ToPrimitive; +use std::cmp::Ordering; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum PaddingRelation { + None, + SameSide, + OppositeSide, +} + +/// Result of reducing SubsetSum to Partition. +#[derive(Debug, Clone)] +pub struct ReductionSubsetSumToPartition { + target: Partition, + source_len: usize, + padding_relation: PaddingRelation, +} + +impl ReductionResult for ReductionSubsetSumToPartition { + type Source = SubsetSum; + type Target = Partition; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let source_bits = &target_solution[..self.source_len]; + + match self.padding_relation { + PaddingRelation::None => source_bits.to_vec(), + PaddingRelation::SameSide => { + let padding_is_selected = target_solution[self.source_len] == 1; + source_bits + .iter() + .map(|&bit| if padding_is_selected { bit } else { 1 - bit }) + .collect() + } + PaddingRelation::OppositeSide => { + let padding_is_selected = target_solution[self.source_len] == 1; + source_bits + .iter() + .map(|&bit| if padding_is_selected { 1 - bit } else { bit }) + .collect() + } + } + } +} + +fn biguint_to_u64(value: &BigUint) -> u64 { + value + .to_u64() + .expect("SubsetSum -> Partition requires all sizes and padding to fit in u64") +} + +#[reduction(overhead = { + num_elements = "num_elements + 1", +})] +impl ReduceTo for SubsetSum { + type Result = ReductionSubsetSumToPartition; + + fn reduce_to(&self) -> Self::Result { + let total: BigUint = self.sizes().iter().cloned().sum(); + let double_target = self.target() * 2u32; + let relation = total.cmp(&double_target); + let padding_relation = match relation { + Ordering::Equal => PaddingRelation::None, + Ordering::Greater => PaddingRelation::SameSide, + Ordering::Less => PaddingRelation::OppositeSide, + }; + + let mut sizes: Vec = self.sizes().iter().map(biguint_to_u64).collect(); + match relation { + Ordering::Equal => {} + Ordering::Greater => sizes.push(biguint_to_u64(&(total - double_target))), + Ordering::Less => sizes.push(biguint_to_u64(&(double_target - total))), + } + + ReductionSubsetSumToPartition { + target: Partition::new(sizes), + source_len: self.num_elements(), + padding_relation, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "subsetsum_to_partition", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, Partition>( + SubsetSum::new(vec![1u32, 5, 6, 8], 11u32), + SolutionPair { + source_config: vec![0, 1, 1, 0], + target_config: vec![0, 1, 1, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/subsetsum_partition.rs"] +mod tests; diff --git a/src/unit_tests/models/graph/graph_partitioning.rs b/src/unit_tests/models/graph/graph_partitioning.rs new file mode 100644 index 000000000..2791d563b --- /dev/null +++ b/src/unit_tests/models/graph/graph_partitioning.rs @@ -0,0 +1,169 @@ +use super::*; +use crate::solvers::BruteForce; +use crate::topology::SimpleGraph; +use crate::traits::Problem; + +/// Issue example: 6 vertices, edges forming two triangles connected by 3 edges. +/// Optimal partition A={0,1,2}, B={3,4,5}, cut=3. +fn issue_example() -> GraphPartitioning { + let graph = SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + ); + GraphPartitioning::new(graph) +} + +#[test] +fn test_graphpartitioning_basic() { + let problem = issue_example(); + + // Check dims: 6 binary variables + assert_eq!(problem.dims(), vec![2, 2, 2, 2, 2, 2]); + + // Evaluate a valid balanced partition: A={0,1,2}, B={3,4,5} + // config: [0, 0, 0, 1, 1, 1] + // Crossing edges: (1,3), (2,3), (2,4) => cut = 3 + let config = vec![0, 0, 0, 1, 1, 1]; + let result = problem.evaluate(&config); + assert_eq!(result, Min(Some(3))); +} + +#[test] +fn test_graphpartitioning_serialization() { + let problem = issue_example(); + let json = serde_json::to_string(&problem).unwrap(); + let deserialized: GraphPartitioning = serde_json::from_str(&json).unwrap(); + assert_eq!(deserialized.graph().num_vertices(), 6); + assert_eq!(deserialized.graph().num_edges(), 9); + + // Verify evaluation is consistent after round-trip + let config = vec![0, 0, 0, 1, 1, 1]; + assert_eq!(problem.evaluate(&config), deserialized.evaluate(&config)); +} + +#[test] +fn test_graphpartitioning_solver() { + let problem = issue_example(); + let solver = BruteForce::new(); + let best = solver.find_witness(&problem).unwrap(); + let size = problem.evaluate(&best); + assert_eq!(size, Min(Some(3))); + + // All optimal solutions should have cut = 3 + let all_best = solver.find_all_witnesses(&problem); + assert!(!all_best.is_empty()); + for sol in &all_best { + assert_eq!(problem.evaluate(sol), Min(Some(3))); + } +} + +#[test] +fn test_graphpartitioning_odd_vertices() { + // 3 vertices: all configs must be Invalid since n is odd + let graph = SimpleGraph::new(3, vec![(0, 1), (1, 2)]); + let problem = GraphPartitioning::new(graph); + + // Every possible config should be Invalid + for a in 0..2 { + for b in 0..2 { + for c in 0..2 { + assert_eq!( + problem.evaluate(&[a, b, c]), + Min(None), + "Expected Invalid for odd n, config [{}, {}, {}]", + a, + b, + c + ); + } + } + } +} + +#[test] +fn test_graphpartitioning_unbalanced_invalid() { + // 4 vertices: only configs with exactly 2 ones are valid + let graph = SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (0, 3)]); + let problem = GraphPartitioning::new(graph); + + // All zeros: 0 ones, not balanced + assert_eq!(problem.evaluate(&[0, 0, 0, 0]), Min(None)); + + // All ones: 4 ones, not balanced + assert_eq!(problem.evaluate(&[1, 1, 1, 1]), Min(None)); + + // One vertex in partition 1: not balanced + assert_eq!(problem.evaluate(&[1, 0, 0, 0]), Min(None)); + + // Three vertices in partition 1: not balanced + assert_eq!(problem.evaluate(&[1, 1, 1, 0]), Min(None)); + + // Two vertices in partition 1: balanced, should be Valid + // 4-cycle edges: (0,1),(1,2),(2,3),(0,3). Config [1,1,0,0] cuts (1,2) and (0,3) => cut=2 + assert_eq!(problem.evaluate(&[1, 1, 0, 0]), Min(Some(2))); +} + +#[test] +fn test_graphpartitioning_rejects_non_binary_configs() { + let problem = issue_example(); + + assert_eq!(problem.evaluate(&[0, 0, 1, 1, 1, 2]), Min(None)); +} + +#[test] +fn test_graphpartitioning_size_getters() { + let problem = issue_example(); + assert_eq!(problem.num_vertices(), 6); + assert_eq!(problem.num_edges(), 9); +} + +#[test] +fn test_graphpartitioning_square_graph() { + // Square graph: 0-1, 1-2, 2-3, 3-0 (the doctest example) + let graph = SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)]); + let problem = GraphPartitioning::new(graph); + + let solver = BruteForce::new(); + let all_best = solver.find_all_witnesses(&problem); + + // Minimum bisection of a 4-cycle: cut = 2 + for sol in &all_best { + assert_eq!(problem.evaluate(sol), Min(Some(2))); + } +} + +#[test] +fn test_graphpartitioning_problem_name() { + assert_eq!( + as Problem>::NAME, + "GraphPartitioning" + ); +} + +#[test] +fn test_graphpartitioning_graph_accessor() { + let problem = issue_example(); + let graph = problem.graph(); + assert_eq!(graph.num_vertices(), 6); + assert_eq!(graph.num_edges(), 9); +} + +#[test] +fn test_graphpartitioning_empty_graph() { + // 4 vertices, no edges: any balanced partition has cut = 0 + let graph = SimpleGraph::new(4, vec![]); + let problem = GraphPartitioning::new(graph); + + let config = vec![0, 0, 1, 1]; + assert_eq!(problem.evaluate(&config), Min(Some(0))); +} diff --git a/src/unit_tests/models/graph/isomorphic_spanning_tree.rs b/src/unit_tests/models/graph/isomorphic_spanning_tree.rs index b16d36f62..51e89cc66 100644 --- a/src/unit_tests/models/graph/isomorphic_spanning_tree.rs +++ b/src/unit_tests/models/graph/isomorphic_spanning_tree.rs @@ -1,6 +1,6 @@ use super::*; use crate::solvers::BruteForce; -use crate::topology::SimpleGraph; +use crate::topology::{Graph, SimpleGraph}; use crate::traits::Problem; #[test] @@ -8,13 +8,19 @@ fn test_isomorphicspanningtree_basic() { // Triangle graph, path tree let graph = SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]); let tree = SimpleGraph::new(3, vec![(0, 1), (1, 2)]); - let problem = IsomorphicSpanningTree::new(graph, tree); + let problem: IsomorphicSpanningTree = + IsomorphicSpanningTree::new(graph.clone(), tree.clone()); assert_eq!(problem.dims(), vec![3, 3, 3]); + assert_eq!(problem.graph(), &graph); + assert_eq!(problem.tree(), &tree); assert_eq!(problem.num_vertices(), 3); - assert_eq!(problem.num_graph_edges(), 3); - assert_eq!(problem.num_tree_edges(), 2); - assert_eq!(IsomorphicSpanningTree::NAME, "IsomorphicSpanningTree"); + assert_eq!(problem.num_edges(), 3); + assert_eq!(problem.tree_edges(), tree.edges()); + assert_eq!( + as Problem>::NAME, + "IsomorphicSpanningTree" + ); } #[test] @@ -111,11 +117,11 @@ fn test_isomorphicspanningtree_serialization() { let problem = IsomorphicSpanningTree::new(graph, tree); let json = serde_json::to_string(&problem).unwrap(); - let deserialized: IsomorphicSpanningTree = serde_json::from_str(&json).unwrap(); + let deserialized: IsomorphicSpanningTree = serde_json::from_str(&json).unwrap(); assert_eq!(deserialized.num_vertices(), 3); - assert_eq!(deserialized.num_graph_edges(), 3); - assert_eq!(deserialized.num_tree_edges(), 2); + assert_eq!(deserialized.num_edges(), 3); + assert_eq!(deserialized.tree_edges(), vec![(0, 1), (1, 2)]); // Verify same evaluation assert!(deserialized.evaluate(&[0, 1, 2])); } @@ -170,7 +176,10 @@ fn test_isomorphicspanningtree_paper_example() { #[test] fn test_isomorphicspanningtree_variant() { - assert!(IsomorphicSpanningTree::variant().is_empty()); + assert_eq!( + as Problem>::variant(), + vec![("graph", "SimpleGraph")] + ); } #[test] @@ -189,3 +198,11 @@ fn test_isomorphicspanningtree_not_a_tree() { let tree = SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]); IsomorphicSpanningTree::new(graph, tree); } + +#[test] +#[should_panic(expected = "tree must be connected")] +fn test_isomorphicspanningtree_disconnected_tree() { + let graph = SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (0, 3)]); + let tree = SimpleGraph::new(4, vec![(0, 1), (1, 2), (0, 2)]); + IsomorphicSpanningTree::new(graph, tree); +} diff --git a/src/unit_tests/models/set/exact_cover_by_3_sets.rs b/src/unit_tests/models/set/exact_cover_by_3_sets.rs index f5406303b..fef828bfb 100644 --- a/src/unit_tests/models/set/exact_cover_by_3_sets.rs +++ b/src/unit_tests/models/set/exact_cover_by_3_sets.rs @@ -7,6 +7,7 @@ fn test_exact_cover_by_3_sets_creation() { let problem = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); assert_eq!(problem.universe_size(), 6); assert_eq!(problem.num_subsets(), 3); + assert_eq!(problem.num_sets(), 3); assert_eq!(problem.num_variables(), 3); assert_eq!(problem.dims(), vec![2, 2, 2]); } @@ -94,6 +95,8 @@ fn test_exact_cover_by_3_sets_serialization() { let deserialized: ExactCoverBy3Sets = serde_json::from_str(&json).unwrap(); assert_eq!(deserialized.universe_size(), problem.universe_size()); assert_eq!(deserialized.num_subsets(), problem.num_subsets()); + assert_eq!(deserialized.num_sets(), problem.num_sets()); + assert_eq!(deserialized.sets(), problem.sets()); assert_eq!(deserialized.subsets(), problem.subsets()); } diff --git a/src/unit_tests/prelude.rs b/src/unit_tests/prelude.rs index da240315d..6e7295b53 100644 --- a/src/unit_tests/prelude.rs +++ b/src/unit_tests/prelude.rs @@ -1,7 +1,20 @@ use crate::prelude::*; +use crate::topology::SimpleGraph; #[test] fn test_prelude_exports_rectilinear_picture_compression() { let problem = RectilinearPictureCompression::new(vec![vec![true]], 1); assert_eq!(problem.bound(), 1); } + +#[test] +fn test_prelude_exports_partition_into_cliques() { + let problem = PartitionIntoCliques::new(SimpleGraph::new(2, vec![(0, 1)]), 1); + assert_eq!(problem.num_cliques(), 1); +} + +#[test] +fn test_prelude_exports_degree_constrained_spanning_tree() { + let problem = DegreeConstrainedSpanningTree::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), 2); + assert_eq!(problem.max_degree(), 2); +} diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index ff9a14967..105344d5f 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -5,7 +5,7 @@ use crate::prelude::*; use crate::rules::{MinimizeSteps, ReductionGraph, ReductionMode, TraversalFlow}; use crate::topology::{KingsSubgraph, SimpleGraph, TriangularSubgraph, UnitDiskGraph}; use crate::types::ProblemSize; -use crate::variant::K3; +use crate::variant::{K3, KN}; use std::collections::BTreeMap; // ---- Discovery and registration ---- @@ -208,6 +208,13 @@ fn test_direct_reduction_exists() { assert!(graph.has_direct_reduction::, MaxCut>()); } +#[test] +fn test_kcoloring_to_partitionintocliques_smoke() { + let source = KColoring::::with_k(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), 2); + let reduction = ReduceTo::>::reduce_to(&source); + assert_eq!(reduction.target_problem().num_cliques(), 2); +} + #[test] fn test_find_direct_path() { let graph = ReductionGraph::new(); diff --git a/src/unit_tests/rules/analysis.rs b/src/unit_tests/rules/analysis.rs index a12dd4a2b..6f81d5c6f 100644 --- a/src/unit_tests/rules/analysis.rs +++ b/src/unit_tests/rules/analysis.rs @@ -261,6 +261,11 @@ fn test_find_dominated_rules_returns_known_set() { ), // ExactCoverBy3Sets → MaxSetPacking → ILP is better than direct ExactCoverBy3Sets → ILP ("ExactCoverBy3Sets", "ILP {variable: \"bool\"}"), + // GraphPartitioning → MaxCut → SpinGlass → QUBO is better than direct GraphPartitioning → QUBO + ( + "GraphPartitioning {graph: \"SimpleGraph\"}", + "QUBO {weight: \"f64\"}", + ), ] .into_iter() .collect(); diff --git a/src/unit_tests/rules/exactcoverby3sets_algebraicequationsovergf2.rs b/src/unit_tests/rules/exactcoverby3sets_algebraicequationsovergf2.rs new file mode 100644 index 000000000..8c0d53d7c --- /dev/null +++ b/src/unit_tests/rules/exactcoverby3sets_algebraicequationsovergf2.rs @@ -0,0 +1,48 @@ +use crate::models::algebraic::AlgebraicEquationsOverGF2; +use crate::models::set::ExactCoverBy3Sets; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; + +#[test] +fn test_exactcoverby3sets_to_algebraicequationsovergf2_closed_loop() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "ExactCoverBy3Sets -> AlgebraicEquationsOverGF2 closed loop", + ); +} + +#[test] +fn test_exactcoverby3sets_to_algebraicequationsovergf2_structure() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_variables(), 3); + assert_eq!(target.num_equations(), 9); + assert_eq!( + target.equations(), + &[ + vec![vec![0], vec![2], vec![]], + vec![vec![0, 2]], + vec![vec![0], vec![]], + vec![vec![0], vec![]], + vec![vec![1], vec![2], vec![]], + vec![vec![1, 2]], + vec![vec![1], vec![2], vec![]], + vec![vec![1, 2]], + vec![vec![1], vec![]], + ] + ); +} + +#[test] +fn test_exactcoverby3sets_to_algebraicequationsovergf2_extract_solution_is_identity() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.extract_solution(&[1, 0, 1]), vec![1, 0, 1]); +} diff --git a/src/unit_tests/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs b/src/unit_tests/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs new file mode 100644 index 000000000..b6e98c9f8 --- /dev/null +++ b/src/unit_tests/rules/exactcoverby3sets_minimumweightsolutiontolinearequations.rs @@ -0,0 +1,46 @@ +use crate::models::algebraic::MinimumWeightSolutionToLinearEquations; +use crate::models::set::ExactCoverBy3Sets; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; + +#[test] +fn test_exactcoverby3sets_to_minimumweightsolutiontolinearequations_closed_loop() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "ExactCoverBy3Sets -> MinimumWeightSolutionToLinearEquations closed loop", + ); +} + +#[test] +fn test_exactcoverby3sets_to_minimumweightsolutiontolinearequations_structure() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!( + target.matrix(), + &[ + vec![1, 0, 1], + vec![1, 0, 0], + vec![1, 0, 0], + vec![0, 1, 1], + vec![0, 1, 1], + vec![0, 1, 0], + ] + ); + assert_eq!(target.rhs(), &[1, 1, 1, 1, 1, 1]); + assert_eq!(target.num_variables(), 3); + assert_eq!(target.num_equations(), 6); +} + +#[test] +fn test_exactcoverby3sets_to_minimumweightsolutiontolinearequations_extract_solution_is_identity() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.extract_solution(&[1, 0, 1]), vec![1, 0, 1]); +} diff --git a/src/unit_tests/rules/exactcoverby3sets_subsetproduct.rs b/src/unit_tests/rules/exactcoverby3sets_subsetproduct.rs new file mode 100644 index 000000000..6433f7dcd --- /dev/null +++ b/src/unit_tests/rules/exactcoverby3sets_subsetproduct.rs @@ -0,0 +1,54 @@ +use crate::models::misc::SubsetProduct; +use crate::models::set::ExactCoverBy3Sets; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use num_bigint::BigUint; + +#[test] +fn test_exactcoverby3sets_to_subsetproduct_closed_loop() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "ExactCoverBy3Sets -> SubsetProduct closed loop", + ); +} + +#[test] +fn test_exactcoverby3sets_to_subsetproduct_structure() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + let expected_sizes: Vec = vec![30u64, 1001, 154] + .into_iter() + .map(BigUint::from) + .collect(); + assert_eq!(target.sizes(), &expected_sizes[..]); + assert_eq!(target.target(), &BigUint::from(30030u64)); + assert_eq!(target.num_elements(), 3); +} + +#[test] +fn test_exactcoverby3sets_to_subsetproduct_extract_solution_is_identity() { + let source = ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.extract_solution(&[1, 0, 1]), vec![1, 0, 1]); +} + +#[test] +fn test_exactcoverby3sets_to_subsetproduct_supports_large_universe() { + let source = ExactCoverBy3Sets::new(18, vec![[0, 1, 2], [15, 16, 17]]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + let expected_sizes: Vec = vec![30u64, 190_747u64] + .into_iter() + .map(BigUint::from) + .collect(); + assert_eq!(target.sizes(), &expected_sizes[..]); + assert!(target.target() > &BigUint::from(u64::MAX)); +} diff --git a/src/unit_tests/rules/graph.rs b/src/unit_tests/rules/graph.rs index a011c1a6b..54e1213f2 100644 --- a/src/unit_tests/rules/graph.rs +++ b/src/unit_tests/rules/graph.rs @@ -1,5 +1,7 @@ use super::*; use crate::models::algebraic::{ILP, QUBO}; +use crate::models::formula::NAESatisfiability; +use crate::models::graph::MaxCut; use crate::models::graph::{MaximumIndependentSet, MinimumVertexCover}; use crate::models::misc::Knapsack; use crate::models::set::MaximumSetPacking; @@ -873,6 +875,13 @@ fn test_ksat_reductions() { assert!(graph.has_direct_reduction::, Satisfiability>()); } +#[test] +fn test_nae_sat_to_maxcut_reduction_registered() { + let graph = ReductionGraph::new(); + + assert!(graph.has_direct_reduction::>()); +} + #[test] fn test_all_categories_present() { let graph = ReductionGraph::new(); diff --git a/src/unit_tests/rules/graphpartitioning_ilp.rs b/src/unit_tests/rules/graphpartitioning_ilp.rs new file mode 100644 index 000000000..bb0ec4e4e --- /dev/null +++ b/src/unit_tests/rules/graphpartitioning_ilp.rs @@ -0,0 +1,132 @@ +use super::*; +use crate::models::algebraic::{Comparison, ObjectiveSense}; +use crate::models::graph::GraphPartitioning; +use crate::solvers::{BruteForce, ILPSolver}; +use crate::topology::SimpleGraph; +use crate::traits::Problem; +use crate::types::Min; + +fn canonical_instance() -> GraphPartitioning { + let graph = SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + ); + GraphPartitioning::new(graph) +} + +#[test] +fn test_reduction_creates_valid_ilp() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 15); + assert_eq!(ilp.constraints.len(), 19); + assert_eq!(ilp.sense, ObjectiveSense::Minimize); + assert_eq!( + ilp.objective, + vec![ + (6, 1.0), + (7, 1.0), + (8, 1.0), + (9, 1.0), + (10, 1.0), + (11, 1.0), + (12, 1.0), + (13, 1.0), + (14, 1.0), + ] + ); +} + +#[test] +fn test_reduction_constraint_shape() { + let problem = GraphPartitioning::new(SimpleGraph::new(2, vec![(0, 1)])); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 3); + assert_eq!(ilp.constraints.len(), 3); + + let balance = &ilp.constraints[0]; + assert_eq!(balance.cmp, Comparison::Eq); + assert_eq!(balance.terms, vec![(0, 1.0), (1, 1.0)]); + assert_eq!(balance.rhs, 1.0); + + let first_link = &ilp.constraints[1]; + assert_eq!(first_link.cmp, Comparison::Ge); + assert_eq!(first_link.terms, vec![(2, 1.0), (0, -1.0), (1, 1.0)]); + assert_eq!(first_link.rhs, 0.0); + + let second_link = &ilp.constraints[2]; + assert_eq!(second_link.cmp, Comparison::Ge); + assert_eq!(second_link.terms, vec![(2, 1.0), (0, 1.0), (1, -1.0)]); + assert_eq!(second_link.rhs, 0.0); +} + +#[test] +fn test_graphpartitioning_to_ilp_closed_loop() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + let bf = BruteForce::new(); + let ilp_solver = ILPSolver::new(); + + let bf_solutions = bf.find_all_witnesses(&problem); + let bf_obj = problem.evaluate(&bf_solutions[0]); + + let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + let ilp_obj = problem.evaluate(&extracted); + + assert_eq!(bf_obj, Min(Some(3))); + assert_eq!(ilp_obj, Min(Some(3))); +} + +#[test] +fn test_odd_vertices_reduce_to_infeasible_ilp() { + let problem = GraphPartitioning::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)])); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.constraints[0].cmp, Comparison::Eq); + assert_eq!(ilp.constraints[0].rhs, 1.5); + + let solver = ILPSolver::new(); + assert_eq!(solver.solve(ilp), None); +} + +#[test] +fn test_solution_extraction() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + + let ilp_solution = vec![0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0]; + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(extracted, vec![0, 0, 0, 1, 1, 1]); + assert_eq!(problem.evaluate(&extracted), Min(Some(3))); +} + +#[test] +fn test_solve_reduced() { + let problem = canonical_instance(); + + let ilp_solver = ILPSolver::new(); + let solution = ilp_solver + .solve_reduced(&problem) + .expect("solve_reduced should work"); + + assert_eq!(problem.evaluate(&solution), Min(Some(3))); +} diff --git a/src/unit_tests/rules/graphpartitioning_maxcut.rs b/src/unit_tests/rules/graphpartitioning_maxcut.rs new file mode 100644 index 000000000..ca9acf458 --- /dev/null +++ b/src/unit_tests/rules/graphpartitioning_maxcut.rs @@ -0,0 +1,65 @@ +use crate::models::graph::{GraphPartitioning, MaxCut}; +use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +fn issue_example() -> GraphPartitioning { + super::issue_example() +} + +#[test] +fn test_graphpartitioning_to_maxcut_closed_loop() { + let source = issue_example(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "GraphPartitioning->MaxCut closed loop", + ); +} + +#[test] +fn test_graphpartitioning_to_maxcut_target_structure() { + let source = issue_example(); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + let num_vertices = source.num_vertices(); + let penalty = i32::try_from(source.num_edges()).unwrap() + 1; + + assert_eq!(target.num_vertices(), num_vertices); + assert_eq!(target.num_edges(), num_vertices * (num_vertices - 1) / 2); + + for u in 0..num_vertices { + for v in (u + 1)..num_vertices { + let expected_weight = if source.graph().has_edge(u, v) { + penalty - 1 + } else { + penalty + }; + assert_eq!( + target.edge_weight(u, v), + Some(&expected_weight), + "unexpected weight on edge ({u}, {v})" + ); + } + } +} + +#[test] +fn test_graphpartitioning_to_maxcut_extract_solution_identity() { + let source = issue_example(); + let reduction = ReduceTo::>::reduce_to(&source); + let target_solution = super::ISSUE_EXAMPLE_WITNESS.to_vec(); + + assert_eq!( + reduction.extract_solution(&target_solution), + target_solution + ); +} + +#[test] +fn test_graphpartitioning_to_maxcut_penalty_overflow_panics() { + let result = std::panic::catch_unwind(|| super::penalty_weight(i32::MAX as usize)); + assert!(result.is_err()); +} diff --git a/src/unit_tests/rules/graphpartitioning_qubo.rs b/src/unit_tests/rules/graphpartitioning_qubo.rs new file mode 100644 index 000000000..779eea84f --- /dev/null +++ b/src/unit_tests/rules/graphpartitioning_qubo.rs @@ -0,0 +1,82 @@ +use super::*; +use crate::models::algebraic::QUBO; +use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target; +use crate::topology::SimpleGraph; + +fn example_problem() -> GraphPartitioning { + GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + )) +} + +#[test] +fn test_graphpartitioning_to_qubo_closed_loop() { + let source = example_problem(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "GraphPartitioning->QUBO closed loop", + ); +} + +#[test] +fn test_graphpartitioning_to_qubo_matrix_matches_issue_example() { + let source = example_problem(); + let reduction = ReduceTo::>::reduce_to(&source); + let qubo = reduction.target_problem(); + + assert_eq!(qubo.num_vars(), 6); + + let expected_diagonal = [-48.0, -47.0, -46.0, -46.0, -47.0, -48.0]; + for (index, expected) in expected_diagonal.into_iter().enumerate() { + assert_eq!(qubo.get(index, index), Some(&expected)); + } + + let edge_pairs = [ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ]; + for &(u, v) in &edge_pairs { + assert_eq!(qubo.get(u, v), Some(&18.0), "edge ({u}, {v})"); + } + + let non_edge_pairs = [(0, 3), (0, 4), (0, 5), (1, 4), (1, 5), (2, 5)]; + for &(u, v) in &non_edge_pairs { + assert_eq!(qubo.get(u, v), Some(&20.0), "non-edge ({u}, {v})"); + } +} + +#[cfg(feature = "example-db")] +#[test] +fn test_graphpartitioning_to_qubo_canonical_example_spec() { + let spec = canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "graphpartitioning_to_qubo") + .expect("missing canonical GraphPartitioning -> QUBO example spec"); + let example = (spec.build)(); + + assert_eq!(example.source.problem, "GraphPartitioning"); + assert_eq!(example.target.problem, "QUBO"); + assert_eq!(example.target.instance["num_vars"], 6); + assert!(!example.solutions.is_empty()); +} diff --git a/src/unit_tests/rules/hamiltonianpath_degreeconstrainedspanningtree.rs b/src/unit_tests/rules/hamiltonianpath_degreeconstrainedspanningtree.rs new file mode 100644 index 000000000..610a9b1d8 --- /dev/null +++ b/src/unit_tests/rules/hamiltonianpath_degreeconstrainedspanningtree.rs @@ -0,0 +1,58 @@ +use crate::models::graph::{DegreeConstrainedSpanningTree, HamiltonianPath}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::traits::Problem; + +fn edge_config(graph: &SimpleGraph, selected_edges: &[(usize, usize)]) -> Vec { + graph + .edges() + .into_iter() + .map(|(u, v)| { + usize::from( + selected_edges + .iter() + .any(|&(a, b)| (a == u && b == v) || (a == v && b == u)), + ) + }) + .collect() +} + +#[test] +fn test_hamiltonianpath_to_degreeconstrainedspanningtree_structure() { + let source = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (0, 2)])); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.graph(), source.graph()); + assert_eq!(target.num_vertices(), source.num_vertices()); + assert_eq!(target.num_edges(), source.num_edges()); + assert_eq!(target.max_degree(), 2); +} + +#[test] +fn test_hamiltonianpath_to_degreeconstrainedspanningtree_closed_loop() { + let source = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (0, 2)])); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "HamiltonianPath->DegreeConstrainedSpanningTree closed loop", + ); +} + +#[test] +fn test_hamiltonianpath_to_degreeconstrainedspanningtree_extract_solution_reconstructs_order() { + let source = HamiltonianPath::new(SimpleGraph::path(4)); + let reduction = ReduceTo::>::reduce_to(&source); + let target_solution = edge_config( + reduction.target_problem().graph(), + &[(0, 1), (1, 2), (2, 3)], + ); + + let extracted = reduction.extract_solution(&target_solution); + + assert_eq!(extracted, vec![0, 1, 2, 3]); + assert!(source.evaluate(&extracted)); +} diff --git a/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs b/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs index 65483d472..77ec0ab99 100644 --- a/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs +++ b/src/unit_tests/rules/hamiltonianpath_isomorphicspanningtree.rs @@ -15,14 +15,14 @@ fn test_hamiltonianpath_to_isomorphicspanningtree_closed_loop() { 5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 3), (1, 4)], )); - let result = ReduceTo::::reduce_to(&source); + let result = ReduceTo::>::reduce_to(&source); let target = result.target_problem(); // Target should have same number of vertices and edges as source graph assert_eq!(target.num_vertices(), 5); - assert_eq!(target.num_graph_edges(), 6); + assert_eq!(target.num_edges(), 6); // Tree is P_5: 4 edges - assert_eq!(target.num_tree_edges(), 4); + assert_eq!(target.tree_edges().len(), 4); assert_satisfaction_round_trip_from_satisfaction_target( &source, @@ -35,7 +35,7 @@ fn test_hamiltonianpath_to_isomorphicspanningtree_closed_loop() { fn test_hamiltonianpath_to_isomorphicspanningtree_path_graph() { // Simple path graph: 0-1-2-3 (trivially has a Hamiltonian path) let source = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)])); - let result = ReduceTo::::reduce_to(&source); + let result = ReduceTo::>::reduce_to(&source); assert_satisfaction_round_trip_from_satisfaction_target( &source, @@ -56,7 +56,7 @@ fn test_hamiltonianpath_to_isomorphicspanningtree_no_hamiltonian_path() { // go to unvisited leaves, and from a leaf we can only go back to 0 (already visited). // Path: leaf-0-leaf is length 2, can't extend. No HP exists. let source = HamiltonianPath::new(SimpleGraph::new(5, vec![(0, 1), (0, 2), (0, 3), (0, 4)])); - let result = ReduceTo::::reduce_to(&source); + let result = ReduceTo::>::reduce_to(&source); let solver = BruteForce::new(); let target_solutions = solver.find_all_witnesses(result.target_problem()); assert!( @@ -79,7 +79,7 @@ fn test_hamiltonianpath_to_isomorphicspanningtree_complete_graph() { 4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)], )); - let result = ReduceTo::::reduce_to(&source); + let result = ReduceTo::>::reduce_to(&source); let target_solution = solve_satisfaction_problem(result.target_problem()) .expect("K4 should have an IST solution"); @@ -95,12 +95,12 @@ fn test_hamiltonianpath_to_isomorphicspanningtree_complete_graph() { fn test_hamiltonianpath_to_isomorphicspanningtree_small_triangle() { // Triangle: 0-1-2-0 (has Hamiltonian path, e.g. 0-1-2) let source = HamiltonianPath::new(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)])); - let result = ReduceTo::::reduce_to(&source); + let result = ReduceTo::>::reduce_to(&source); let target = result.target_problem(); assert_eq!(target.num_vertices(), 3); - assert_eq!(target.num_graph_edges(), 3); - assert_eq!(target.num_tree_edges(), 2); + assert_eq!(target.num_edges(), 3); + assert_eq!(target.tree_edges().len(), 2); assert_satisfaction_round_trip_from_satisfaction_target( &source, diff --git a/src/unit_tests/rules/hamiltonianpathbetweentwovertices_longestpath.rs b/src/unit_tests/rules/hamiltonianpathbetweentwovertices_longestpath.rs new file mode 100644 index 000000000..f112ca82f --- /dev/null +++ b/src/unit_tests/rules/hamiltonianpathbetweentwovertices_longestpath.rs @@ -0,0 +1,109 @@ +use super::*; +use crate::models::graph::{HamiltonianPathBetweenTwoVertices, LongestPath}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +use crate::topology::SimpleGraph; +use crate::types::One; + +#[test] +fn test_hamiltonianpathbetweentwovertices_to_longestpath_closed_loop() { + // Graph with a known Hamiltonian 0-4 path: 0-1-2-3-4 plus extra edges + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 3), (1, 4)]), + 0, + 4, + ); + let result = ReduceTo::>::reduce_to(&source); + let target = result.target_problem(); + + assert_eq!(target.num_vertices(), 5); + assert_eq!(target.num_edges(), 6); + assert_eq!(target.source_vertex(), 0); + assert_eq!(target.target_vertex(), 4); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &result, + "HamiltonianPathBetweenTwoVertices->LongestPath closed loop", + ); +} + +#[test] +fn test_hamiltonianpathbetweentwovertices_to_longestpath_path_graph() { + // Simple path graph: 0-1-2-3 with s=0, t=3 (trivially has a Hamiltonian path) + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), + 0, + 3, + ); + let result = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &result, + "HamiltonianPathBetweenTwoVertices->LongestPath path graph", + ); +} + +#[test] +fn test_hamiltonianpathbetweentwovertices_to_longestpath_no_hamiltonian_path() { + // Star graph K_{1,4}: vertex 0 connected to 1,2,3,4. + // No Hamiltonian path from 1 to 2 exists (vertices 3,4 are leaves + // connected only to 0, so no path can visit all without revisiting 0). + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (0, 3), (0, 4)]), + 1, + 2, + ); + let result = ReduceTo::>::reduce_to(&source); + let solver = BruteForce::new(); + let target_best = solver + .find_witness(result.target_problem()) + .expect("LongestPath should have some valid path"); + + // The best path has fewer than n-1 = 4 edges (it's not Hamiltonian) + let selected_edges: usize = target_best.iter().sum(); + assert!( + selected_edges < 4, + "Best path should have fewer than n-1 edges since no Hamiltonian s-t path exists" + ); +} + +#[test] +fn test_hamiltonianpathbetweentwovertices_to_longestpath_complete_graph() { + // Complete graph K4 with s=0, t=3: many Hamiltonian 0-3 paths exist + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]), + 0, + 3, + ); + let result = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &result, + "HamiltonianPathBetweenTwoVertices->LongestPath complete K4", + ); +} + +#[test] +fn test_hamiltonianpathbetweentwovertices_to_longestpath_triangle() { + // Triangle: 0-1-2-0, with s=0, t=2 + let source = HamiltonianPathBetweenTwoVertices::new( + SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]), + 0, + 2, + ); + let result = ReduceTo::>::reduce_to(&source); + let target = result.target_problem(); + + assert_eq!(target.num_vertices(), 3); + assert_eq!(target.num_edges(), 3); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &result, + "HamiltonianPathBetweenTwoVertices->LongestPath triangle", + ); +} diff --git a/src/unit_tests/rules/kcoloring_partitionintocliques.rs b/src/unit_tests/rules/kcoloring_partitionintocliques.rs new file mode 100644 index 000000000..c64337df2 --- /dev/null +++ b/src/unit_tests/rules/kcoloring_partitionintocliques.rs @@ -0,0 +1,53 @@ +use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::topology::Graph; +use crate::variant::KN; + +#[test] +fn test_kcoloring_to_partitionintocliques_closed_loop() { + let source = KColoring::::with_k( + SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 3), (2, 3), (2, 4), (3, 4)]), + 3, + ); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "KColoring->PartitionIntoCliques closed loop", + ); +} + +#[test] +fn test_kcoloring_to_partitionintocliques_complement_structure() { + let source = KColoring::::with_k(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), 2); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.graph().num_vertices(), 4); + assert_eq!(target.graph().num_edges(), 3); + assert_eq!(target.num_cliques(), 2); + assert!(target.graph().has_edge(0, 2)); + assert!(target.graph().has_edge(0, 3)); + assert!(target.graph().has_edge(1, 3)); +} + +#[test] +fn test_kcoloring_to_partitionintocliques_extract_solution_identity() { + let source = KColoring::::with_k(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), 2); + let reduction = ReduceTo::>::reduce_to(&source); + let config = vec![0, 1, 0]; + + assert_eq!(reduction.extract_solution(&config), config); +} + +#[test] +fn test_kcoloring_to_partitionintocliques_unsat_preserved() { + let source = KColoring::::with_k(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]), 2); + let reduction = ReduceTo::>::reduce_to(&source); + let solver = BruteForce::new(); + + assert!(solver.find_witness(&source).is_none()); + assert!(solver.find_witness(reduction.target_problem()).is_none()); +} diff --git a/src/unit_tests/rules/ksatisfiability_kernel.rs b/src/unit_tests/rules/ksatisfiability_kernel.rs new file mode 100644 index 000000000..38776937e --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_kernel.rs @@ -0,0 +1,76 @@ +use crate::models::formula::{CNFClause, KSatisfiability}; +use crate::models::graph::Kernel; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; +use crate::variant::K3; + +#[test] +fn test_ksatisfiability_to_kernel_structure() { + let source = KSatisfiability::::new(2, vec![CNFClause::new(vec![1, -2, 1])]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vertices(), 7); + assert_eq!(target.num_arcs(), 10); + + for arc in [ + (0, 1), + (1, 0), + (2, 3), + (3, 2), + (4, 5), + (5, 6), + (6, 4), + (4, 0), + (5, 3), + (6, 0), + ] { + assert!(target.graph().has_arc(arc.0, arc.1)); + } +} + +#[test] +fn test_ksatisfiability_to_kernel_closed_loop() { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "3SAT -> Kernel closed loop", + ); +} + +#[test] +fn test_ksatisfiability_to_kernel_unsatisfiable_instance_has_no_kernel() { + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_ksatisfiability_to_kernel_extract_solution_reads_variable_gadgets() { + let source = KSatisfiability::::new(2, vec![CNFClause::new(vec![1, -2, 1])]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.extract_solution(&[1, 0, 0, 1, 0, 0, 0]), + vec![1, 0] + ); +} diff --git a/src/unit_tests/rules/ksatisfiability_simultaneousincongruences.rs b/src/unit_tests/rules/ksatisfiability_simultaneousincongruences.rs new file mode 100644 index 000000000..c2613cdc6 --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_simultaneousincongruences.rs @@ -0,0 +1,90 @@ +use super::*; +use crate::models::formula::CNFClause; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use crate::variant::K3; + +#[test] +fn test_ksatisfiability_to_simultaneous_incongruences_closed_loop() { + let source = KSatisfiability::::new( + 2, + vec![ + CNFClause::new(vec![1, 2, 2]), + CNFClause::new(vec![-1, 2, 2]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.lcm_moduli(), 15); + assert_eq!(target.num_pairs(), 6); + + let solver = BruteForce::new(); + let target_solution = solver + .find_witness(target) + .expect("target should be satisfiable"); + let extracted = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&extracted)); +} + +#[test] +fn test_ksatisfiability_to_simultaneous_incongruences_structure() { + let source = KSatisfiability::::new( + 2, + vec![ + CNFClause::new(vec![1, 2, 2]), + CNFClause::new(vec![-1, 2, 2]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + let pairs: Vec<(u64, u64)> = target.pairs().to_vec(); + assert_eq!( + pairs, + vec![(3, 3), (5, 5), (3, 5), (4, 5), (2, 15), (7, 15)] + ); +} + +#[test] +fn test_ksatisfiability_to_simultaneous_incongruences_unsatisfiable() { + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + + assert_eq!(solver.find_witness(reduction.target_problem()), None); +} + +#[test] +fn test_ksatisfiability_to_simultaneous_incongruences_tautological_clause_is_redundant() { + let source = KSatisfiability::::new( + 2, + vec![ + CNFClause::new(vec![1, -1, 2]), + CNFClause::new(vec![2, 2, 2]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + let target_solution = solver + .find_witness(reduction.target_problem()) + .expect("target should remain satisfiable"); + let extracted = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&extracted)); +} + +#[test] +#[should_panic(expected = "3-SAT -> SimultaneousIncongruences requires the variable-prime product")] +fn test_ksatisfiability_to_simultaneous_incongruences_rejects_large_instances() { + let source = KSatisfiability::::new(7, vec![CNFClause::new(vec![1, 2, 3])]); + + let _ = ReduceTo::::reduce_to(&source); +} diff --git a/src/unit_tests/rules/naesatisfiability_setsplitting.rs b/src/unit_tests/rules/naesatisfiability_setsplitting.rs new file mode 100644 index 000000000..a52ea2206 --- /dev/null +++ b/src/unit_tests/rules/naesatisfiability_setsplitting.rs @@ -0,0 +1,87 @@ +use crate::models::formula::{CNFClause, NAESatisfiability}; +use crate::models::set::SetSplitting; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +fn rule_example_problem() -> NAESatisfiability { + NAESatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, -2, 3]), + CNFClause::new(vec![-1, 2, -3]), + ], + ) +} + +#[test] +fn test_naesatisfiability_to_setsplitting_closed_loop() { + let source = rule_example_problem(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "NAE-SAT -> SetSplitting", + ); +} + +#[test] +fn test_naesatisfiability_to_setsplitting_structure() { + let source = rule_example_problem(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.universe_size(), 6); + assert_eq!(target.num_subsets(), 5); + assert_eq!( + target.subsets(), + &[ + vec![0, 3], + vec![1, 4], + vec![2, 5], + vec![0, 4, 2], + vec![3, 1, 5], + ], + ); +} + +#[test] +fn test_naesatisfiability_to_setsplitting_extract_solution_uses_positive_literals() { + let source = rule_example_problem(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.extract_solution(&[1, 0, 1, 0, 1, 0]), + vec![1, 0, 1] + ); +} + +#[test] +fn test_naesatisfiability_to_setsplitting_target_witness_extracts_to_satisfying_assignment() { + let source = rule_example_problem(); + let reduction = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + + let target_solution = solver.find_witness(reduction.target_problem()).unwrap(); + let source_solution = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&source_solution)); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_naesatisfiability_to_setsplitting_canonical_example_spec() { + let specs = crate::rules::naesatisfiability_setsplitting::canonical_rule_example_specs(); + assert_eq!(specs.len(), 1); + + let example = (specs[0].build)(); + assert_eq!(example.source.problem, "NAESatisfiability"); + assert_eq!(example.target.problem, "SetSplitting"); + assert_eq!(example.solutions.len(), 1); + + let pair = &example.solutions[0]; + assert_eq!(pair.source_config, vec![1, 1, 1]); + assert_eq!(pair.target_config, vec![1, 1, 1, 0, 0, 0]); +} diff --git a/src/unit_tests/rules/partition_openshopscheduling.rs b/src/unit_tests/rules/partition_openshopscheduling.rs new file mode 100644 index 000000000..ff3b42f81 --- /dev/null +++ b/src/unit_tests/rules/partition_openshopscheduling.rs @@ -0,0 +1,64 @@ +use super::*; +use crate::models::misc::{OpenShopScheduling, Partition}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use crate::types::Min; + +#[test] +fn test_partition_to_open_shop_scheduling_closed_loop() { + let source = Partition::new(vec![1, 2, 3]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "Partition -> OpenShopScheduling closed loop", + ); +} + +#[test] +fn test_partition_to_open_shop_scheduling_structure() { + let source = Partition::new(vec![1, 2, 3]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_jobs(), 4); + assert_eq!(target.num_machines(), 3); + assert_eq!( + target.processing_times(), + &[vec![1, 1, 1], vec![2, 2, 2], vec![3, 3, 3], vec![3, 3, 3]] + ); +} + +#[test] +fn test_partition_to_open_shop_scheduling_extract_solution() { + let source = Partition::new(vec![1, 2, 3]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // Use the solver to get a valid optimal target config + let target_solution = BruteForce::new() + .find_witness(target) + .expect("target should have an optimal solution"); + let extracted = reduction.extract_solution(&target_solution); + + // The extracted solution should be a valid partition decision + assert_eq!(extracted.len(), 3); + assert!(extracted.iter().all(|&v| v <= 1)); + // Since total=6 is even, a satisfying partition exists + assert!(source.evaluate(&extracted)); +} + +#[test] +fn test_partition_to_open_shop_scheduling_odd_total_is_not_satisfying() { + let source = Partition::new(vec![2, 4, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + let best = BruteForce::new() + .find_witness(target) + .expect("open-shop target should always have an optimal solution"); + + assert_eq!(target.evaluate(&best), Min(Some(16))); + assert!(!source.evaluate(&reduction.extract_solution(&best))); +} diff --git a/src/unit_tests/rules/partition_productionplanning.rs b/src/unit_tests/rules/partition_productionplanning.rs new file mode 100644 index 000000000..ceca9105c --- /dev/null +++ b/src/unit_tests/rules/partition_productionplanning.rs @@ -0,0 +1,54 @@ +use super::*; +use crate::models::misc::{Partition, ProductionPlanning}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; + +#[test] +fn test_partition_to_productionplanning_closed_loop() { + let source = Partition::new(vec![3, 5, 2, 4, 6]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "Partition -> ProductionPlanning closed loop", + ); +} + +#[test] +fn test_partition_to_productionplanning_structure_even_total() { + let source = Partition::new(vec![3, 5, 2, 4, 6]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.demands(), &[0, 0, 0, 0, 0, 10]); + assert_eq!(target.capacities(), &[3, 5, 2, 4, 6, 0]); + assert_eq!(target.setup_costs(), &[3, 5, 2, 4, 6, 0]); + assert_eq!(target.production_costs(), &[0, 0, 0, 0, 0, 0]); + assert_eq!(target.inventory_costs(), &[0, 0, 0, 0, 0, 0]); + assert_eq!(target.cost_bound(), 10); +} + +#[test] +fn test_partition_to_productionplanning_odd_total_is_infeasible() { + let source = Partition::new(vec![2, 4, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.demands(), &[0, 0, 0, 6]); + assert_eq!(target.capacities(), &[2, 4, 5, 0]); + assert_eq!(target.setup_costs(), &[2, 4, 5, 0]); + assert_eq!(target.cost_bound(), 5); + assert!(BruteForce::new().find_witness(target).is_none()); +} + +#[test] +fn test_partition_to_productionplanning_extract_solution() { + let source = Partition::new(vec![3, 5, 2, 4, 6]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.extract_solution(&[0, 0, 0, 4, 6, 0]), + vec![0, 0, 0, 1, 1] + ); +} diff --git a/src/unit_tests/rules/partition_sequencingtominimizetardytaskweight.rs b/src/unit_tests/rules/partition_sequencingtominimizetardytaskweight.rs new file mode 100644 index 000000000..75749bc3b --- /dev/null +++ b/src/unit_tests/rules/partition_sequencingtominimizetardytaskweight.rs @@ -0,0 +1,101 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use crate::models::misc::{Partition, SequencingToMinimizeTardyTaskWeight}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target; +use crate::rules::traits::ReductionResult; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use crate::types::Min; + +#[test] +fn test_partition_to_sequencing_to_minimize_tardy_task_weight_closed_loop() { + let source = Partition::new(vec![3, 1, 1, 2, 2, 1]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "Partition -> SequencingToMinimizeTardyTaskWeight closed loop", + ); +} + +#[test] +fn test_partition_to_sequencing_to_minimize_tardy_task_weight_structure() { + let source = Partition::new(vec![3, 1, 1, 2, 2, 1]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.lengths(), &[3, 1, 1, 2, 2, 1]); + assert_eq!(target.weights(), &[3, 1, 1, 2, 2, 1]); + assert_eq!(target.deadlines(), &[5, 5, 5, 5, 5, 5]); + assert_eq!(target.num_tasks(), source.num_elements()); +} + +#[test] +fn test_partition_to_sequencing_to_minimize_tardy_task_weight_extract_solution() { + let source = Partition::new(vec![3, 1, 1, 2, 2, 1]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.extract_solution(&[1, 2, 4, 5, 0, 3]), + vec![1, 0, 0, 1, 0, 0] + ); +} + +#[test] +fn test_partition_to_sequencing_to_minimize_tardy_task_weight_odd_total_is_unsatisfying() { + let source = Partition::new(vec![2, 4, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + let best = BruteForce::new() + .find_witness(target) + .expect("target should always have an optimal schedule"); + + assert_eq!(target.evaluate(&best), Min(Some(6))); + assert!(!source.evaluate(&reduction.extract_solution(&best))); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_partition_to_sequencing_to_minimize_tardy_task_weight_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "partition_to_sequencing_to_minimize_tardy_task_weight") + .expect("missing canonical Partition -> SequencingToMinimizeTardyTaskWeight example spec") + .build)(); + + assert_eq!(example.source.problem, "Partition"); + assert_eq!( + example.target.problem, + "SequencingToMinimizeTardyTaskWeight" + ); + assert_eq!( + example.target.instance["lengths"], + serde_json::json!([3, 1, 1, 2, 2, 1]) + ); + assert_eq!( + example.target.instance["weights"], + serde_json::json!([3, 1, 1, 2, 2, 1]) + ); + assert_eq!( + example.target.instance["deadlines"], + serde_json::json!([5, 5, 5, 5, 5, 5]) + ); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![1, 0, 0, 1, 0, 0]); + assert_eq!(example.solutions[0].target_config, vec![1, 2, 4, 5, 0, 3]); + + let source: Partition = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: SequencingToMinimizeTardyTaskWeight = + serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + + assert!(source + .evaluate(&example.solutions[0].source_config) + .is_valid()); + assert!(target + .evaluate(&example.solutions[0].target_config) + .is_valid()); +} diff --git a/src/unit_tests/rules/satisfiability_nontautology.rs b/src/unit_tests/rules/satisfiability_nontautology.rs new file mode 100644 index 000000000..e7a2101e1 --- /dev/null +++ b/src/unit_tests/rules/satisfiability_nontautology.rs @@ -0,0 +1,69 @@ +use crate::models::formula::{CNFClause, NonTautology, Satisfiability}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionGraph, ReductionResult}; +use crate::solvers::BruteForce; + +#[test] +fn test_satisfiability_to_non_tautology_structure() { + let source = Satisfiability::new( + 3, + vec![CNFClause::new(vec![1, -2]), CNFClause::new(vec![-1, 3])], + ); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 3); + assert_eq!(target.num_disjuncts(), 2); + assert_eq!(target.disjuncts(), &[vec![-1, 2], vec![1, -3]]); +} + +#[test] +fn test_satisfiability_to_non_tautology_closed_loop() { + let source = Satisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2]), + CNFClause::new(vec![-1, 3]), + CNFClause::new(vec![-2, -3]), + ], + ); + + let reduction = ReduceTo::::reduce_to(&source); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "SAT->NonTautology closed loop", + ); +} + +#[test] +fn test_satisfiability_to_non_tautology_unsatisfiable_source_has_no_target_witness() { + let source = Satisfiability::new(1, vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])]); + + let reduction = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + + assert_eq!(solver.find_witness(reduction.target_problem()), None); +} + +#[test] +fn test_satisfiability_to_non_tautology_extract_solution_is_identity() { + let source = Satisfiability::new(2, vec![CNFClause::new(vec![1]), CNFClause::new(vec![2])]); + + let reduction = ReduceTo::::reduce_to(&source); + let target_solution = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("target should have a witness"); + + assert_eq!( + reduction.extract_solution(&target_solution), + target_solution + ); +} + +#[test] +fn test_reduction_graph_registers_satisfiability_to_non_tautology() { + let graph = ReductionGraph::new(); + assert!(graph.has_direct_reduction_by_name("Satisfiability", "NonTautology")); +} diff --git a/src/unit_tests/rules/subsetsum_capacityassignment.rs b/src/unit_tests/rules/subsetsum_capacityassignment.rs index ddd1078ca..fa23929b3 100644 --- a/src/unit_tests/rules/subsetsum_capacityassignment.rs +++ b/src/unit_tests/rules/subsetsum_capacityassignment.rs @@ -100,12 +100,14 @@ fn test_subsetsum_to_capacityassignment_monotonicity() { let target = reduction.target_problem(); for (link, cost_row) in target.cost().iter().enumerate() { + let cost_row: &[u64] = cost_row; assert!( cost_row.windows(2).all(|w| w[0] <= w[1]), "cost row {link} must be non-decreasing" ); } for (link, delay_row) in target.delay().iter().enumerate() { + let delay_row: &[u64] = delay_row; assert!( delay_row.windows(2).all(|w| w[0] >= w[1]), "delay row {link} must be non-increasing" diff --git a/src/unit_tests/rules/subsetsum_integerexpressionmembership.rs b/src/unit_tests/rules/subsetsum_integerexpressionmembership.rs new file mode 100644 index 000000000..87b3fe6a3 --- /dev/null +++ b/src/unit_tests/rules/subsetsum_integerexpressionmembership.rs @@ -0,0 +1,99 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use crate::models::misc::IntegerExpressionMembership; +use crate::models::misc::SubsetSum; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::traits::ReductionResult; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +#[cfg(feature = "example-db")] +use crate::traits::Problem; + +fn issue_example_source() -> SubsetSum { + SubsetSum::new(vec![1u32, 5, 6, 8], 11u32) +} + +fn issue_example_source_config() -> Vec { + vec![0, 1, 1, 0] +} + +fn issue_example_target_config() -> Vec { + vec![0, 1, 1, 0] +} + +#[test] +fn test_subsetsum_to_integerexpressionmembership_closed_loop() { + let source = issue_example_source(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + // 4 items -> 4 union nodes + assert_eq!(target.num_union_nodes(), 4); + // Shifted target: 11 + 4 = 15 + assert_eq!(target.target(), 15); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "SubsetSum -> IntegerExpressionMembership closed loop", + ); +} + +#[test] +fn test_subsetsum_to_integerexpressionmembership_extract_solution_matches_choice_bits() { + let source = issue_example_source(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.extract_solution(&issue_example_target_config()), + issue_example_source_config() + ); + assert_eq!(reduction.extract_solution(&[1, 0, 0, 1]), vec![1, 0, 0, 1]); +} + +#[test] +fn test_subsetsum_to_integerexpressionmembership_unsatisfiable_instance_stays_unsatisfiable() { + let source = SubsetSum::new(vec![2u32, 4, 6], 5u32); + let reduction = ReduceTo::::reduce_to(&source); + + assert!(BruteForce::new().find_witness(&source).is_none()); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_subsetsum_to_integerexpressionmembership_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "subsetsum_to_integerexpressionmembership") + .expect("missing canonical SubsetSum -> IntegerExpressionMembership example spec") + .build)(); + + assert_eq!(example.source.problem, "SubsetSum"); + assert_eq!(example.target.problem, "IntegerExpressionMembership"); + assert_eq!(example.target.instance["target"], serde_json::json!(15)); + assert!(!example.solutions.is_empty()); + assert_eq!( + example.solutions[0].source_config, + issue_example_source_config() + ); + assert_eq!( + example.solutions[0].target_config, + issue_example_target_config() + ); + + let source: SubsetSum = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: IntegerExpressionMembership = + serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + + assert!(source + .evaluate(&example.solutions[0].source_config) + .is_valid()); + assert!(target + .evaluate(&example.solutions[0].target_config) + .is_valid()); +} diff --git a/src/unit_tests/rules/subsetsum_partition.rs b/src/unit_tests/rules/subsetsum_partition.rs new file mode 100644 index 000000000..cda81b51d --- /dev/null +++ b/src/unit_tests/rules/subsetsum_partition.rs @@ -0,0 +1,87 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use crate::models::misc::{Partition, SubsetSum}; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::traits::ReductionResult; +use crate::rules::ReduceTo; +use crate::solvers::BruteForce; +#[cfg(feature = "example-db")] +use crate::traits::Problem; + +#[test] +fn test_subsetsum_to_partition_closed_loop() { + let source = SubsetSum::new(vec![1u32, 5, 6, 8], 11u32); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.sizes(), &[1, 5, 6, 8, 2]); + assert_eq!(target.num_elements(), source.num_elements() + 1); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "SubsetSum -> Partition closed loop", + ); +} + +#[test] +fn test_subsetsum_to_partition_sigma_greater_than_two_t_extraction() { + let source = SubsetSum::new(vec![10u32, 20, 30], 10u32); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.target_problem().sizes(), &[10, 20, 30, 40]); + assert_eq!(reduction.extract_solution(&[1, 0, 0, 1]), vec![1, 0, 0]); + assert_eq!(reduction.extract_solution(&[0, 1, 1, 0]), vec![1, 0, 0]); +} + +#[test] +fn test_subsetsum_to_partition_sigma_equals_two_t_extraction() { + let source = SubsetSum::new(vec![3u32, 5, 2, 6], 8u32); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.target_problem().sizes(), &[3, 5, 2, 6]); + assert_eq!(reduction.extract_solution(&[1, 1, 0, 0]), vec![1, 1, 0, 0]); +} + +#[test] +fn test_subsetsum_to_partition_unsatisfiable_instance_stays_unsatisfiable() { + let source = SubsetSum::new(vec![3u32, 7, 11], 5u32); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.sizes(), &[3, 7, 11, 11]); + assert!(BruteForce::new().find_witness(&source).is_none()); + assert!(BruteForce::new().find_witness(target).is_none()); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_subsetsum_to_partition_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "subsetsum_to_partition") + .expect("missing canonical SubsetSum -> Partition example spec") + .build)(); + + assert_eq!(example.source.problem, "SubsetSum"); + assert_eq!(example.target.problem, "Partition"); + assert_eq!( + example.target.instance["sizes"], + serde_json::json!([1, 5, 6, 8, 2]) + ); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![0, 1, 1, 0]); + assert_eq!(example.solutions[0].target_config, vec![0, 1, 1, 0, 0]); + + let source: SubsetSum = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: Partition = serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + + assert!(source + .evaluate(&example.solutions[0].source_config) + .is_valid()); + assert!(target + .evaluate(&example.solutions[0].target_config) + .is_valid()); +} diff --git a/src/unit_tests/trait_consistency.rs b/src/unit_tests/trait_consistency.rs index d1be4fde7..a8e62e9bd 100644 --- a/src/unit_tests/trait_consistency.rs +++ b/src/unit_tests/trait_consistency.rs @@ -136,6 +136,10 @@ fn test_all_problems_implement_trait_correctly() { &HamiltonianPath::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)])), "HamiltonianPath", ); + check_problem_trait( + &DegreeConstrainedSpanningTree::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), 2), + "DegreeConstrainedSpanningTree", + ); check_problem_trait( &ShortestWeightConstrainedPath::new( SimpleGraph::new(3, vec![(0, 1), (1, 2)]), diff --git a/tests/main.rs b/tests/main.rs index 6a7cc0c00..777283aef 100644 --- a/tests/main.rs +++ b/tests/main.rs @@ -6,5 +6,9 @@ mod examples; mod integration; #[path = "suites/jl_parity.rs"] mod jl_parity; +#[path = "suites/ksatisfiability_simultaneous_incongruences.rs"] +mod ksatisfiability_simultaneous_incongruences; #[path = "suites/reductions.rs"] mod reductions; +#[path = "suites/simultaneous_incongruences.rs"] +mod simultaneous_incongruences; diff --git a/tests/suites/ksatisfiability_simultaneous_incongruences.rs b/tests/suites/ksatisfiability_simultaneous_incongruences.rs new file mode 100644 index 000000000..73791447a --- /dev/null +++ b/tests/suites/ksatisfiability_simultaneous_incongruences.rs @@ -0,0 +1,31 @@ +use problemreductions::models::algebraic::SimultaneousIncongruences; +use problemreductions::models::formula::{CNFClause, KSatisfiability}; +use problemreductions::rules::{ReduceTo, ReductionResult}; +use problemreductions::solvers::BruteForce; +use problemreductions::variant::K3; +use problemreductions::Problem; + +#[test] +fn test_ksatisfiability_to_simultaneous_incongruences_closed_loop() { + let source = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, 2, 3]), + ], + ); + + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.lcm_moduli(), 105); + assert_eq!(target.num_pairs(), 11); + + let solver = BruteForce::new(); + let target_solution = solver + .find_witness(target) + .expect("target should be satisfiable"); + let extracted = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&extracted)); +} diff --git a/tests/suites/simultaneous_incongruences.rs b/tests/suites/simultaneous_incongruences.rs new file mode 100644 index 000000000..5d1aca63e --- /dev/null +++ b/tests/suites/simultaneous_incongruences.rs @@ -0,0 +1,31 @@ +use problemreductions::models::algebraic::SimultaneousIncongruences; +use problemreductions::solvers::BruteForce; +use problemreductions::traits::Problem; + +#[test] +fn test_simultaneous_incongruences_issue_example() { + // pairs: (a_i, b_i) meaning x != a_i (mod b_i) + let problem = SimultaneousIncongruences::new(vec![(2, 2), (1, 3), (2, 5), (3, 7)]).unwrap(); + + assert_eq!(problem.num_pairs(), 4); + assert_eq!(problem.pairs(), &[(2, 2), (1, 3), (2, 5), (3, 7)]); + assert_eq!(problem.lcm_moduli(), 210); + assert_eq!(problem.dims(), vec![210]); + // x=5: 5%2=1!=0(=2%2), 5%3=2!=1, 5%5=0!=2, 5%7=5!=3 => valid + assert!(problem.evaluate(&[5])); + // x=2: 2%2=0=2%2 => invalid (first incongruence violated) + assert!(!problem.evaluate(&[2])); +} + +#[test] +fn test_simultaneous_incongruences_solver_finds_witness() { + let problem = SimultaneousIncongruences::new(vec![(2, 2), (1, 3), (2, 5), (3, 7)]).unwrap(); + let solver = BruteForce::new(); + + let witness = solver.find_witness(&problem); + // x=1: 1%2=1!=0, 1%3=1!=1? No, 1%3=1=1 so invalid! + // x=3: 3%2=1!=0, 3%3=0!=1, 3%5=3!=2, 3%7=3!=3 => valid. First valid. + assert!(witness.is_some()); + let w = witness.unwrap(); + assert!(problem.evaluate(&w)); +}