diff --git a/.claude/skills/review-paper/SKILL.md b/.claude/skills/review-paper/SKILL.md new file mode 100644 index 00000000..d1c98cdf --- /dev/null +++ b/.claude/skills/review-paper/SKILL.md @@ -0,0 +1,142 @@ +--- +name: review-paper +description: Review the Typst paper (docs/paper/reductions.typ) for quality issues — evaluates 10 entries per session, reports mechanical and critical issues without fixing +--- + +# Review Paper + +Evaluate the quality of problem definitions and reduction rules in `docs/paper/reductions.typ`. Each session reviews **10 entries** (problems or rules), producing a structured report. **Read-only — do not modify any files.** + +## Usage + +``` +/review-paper # review next 10 unreviewed problem-defs +/review-paper rules # review next 10 unreviewed reduction-rules +/review-paper ProblemName # review a specific problem-def +/review-paper Source Target # review a specific reduction-rule +``` + +## Step 0: Determine Scope + +Parse the argument: +- No argument or `problems` → review problem-defs +- `rules` → review reduction-rules +- A specific name → review that single entry + +To pick which 10 to review, scan `docs/paper/reductions.typ` for all `problem-def(...)` or `reduction-rule(...)` entries. Start from the beginning of the file, skipping any that have been reviewed in a previous session (check memory for `paper-review-progress`). If all have been reviewed, report completion. + +## Step 1: Load Gold Standard + +Read the reference examples before reviewing: +- **Problem gold standard:** search for `problem-def("MaximumIndependentSet")` in `reductions.typ` — note its structure, depth, and components +- **Rule gold standard:** search for `reduction-rule("MaximumIndependentSet", "MinimumVertexCover"` — note its proof depth and example + +## Step 2: Review Each Entry + +For each of the 10 entries, read the full entry text and evaluate against the checklists below. + +### Problem-Def Checklist + +**Mechanical checks** (objective, can be verified by reading): + +| Check | Criterion | +|-------|-----------| +| M1. Display name | Entry exists in `display-name` dictionary | +| M2. Formal definition | `def` parameter is present and non-empty | +| M3. Self-contained notation | Every symbol in `def` is defined before first use | +| M4. Background text | Body contains at least 2 sentences of background/motivation | +| M5. Example present | Body contains `*Example.*` or `Example.` | +| M6. Example from fixture | Example data matches `src/example_db/fixtures/examples.json` (not invented) — check by loading the JSON and comparing | +| M7. Figure present | Body contains `#figure(` | +| M8. Pred commands | Body contains `pred-commands(` or `pred create` | +| M9. Algorithm citation | Complexity claims have `@citation` or a footnote explaining absence | +| M10. Evaluation shown | Example shows how the objective/verifier computes the value | + +**Critical checks** (require judgment): + +| Check | Criterion | +|-------|-----------| +| C1. Definition correctness | Does the formal definition accurately describe the problem? Compare with the Rust implementation (`src/models/`) and literature | +| C2. Background quality | Is the background informative? Does it mention applications, history, special cases, or algorithmic context? | +| C3. Example pedagogy | Is the example small enough to verify by hand? Does it illustrate the key aspects of the problem? | +| C4. Completeness | Are there important aspects of the problem that are missing (e.g., well-known special cases, relationship to other problems)? | + +### Reduction-Rule Checklist + +**Mechanical checks:** + +| Check | Criterion | +|-------|-----------| +| M1. Theorem statement | Rule body describes the construction | +| M2. Proof present | Proof body is non-empty | +| M3. Proof length | Proof is at least 3 sentences (not just "trivial" or a one-liner) | +| M4. Overhead documented | Overhead is auto-generated from JSON (verify edge exists in `reduction_graph.json`) | +| M5. Example present | `example: true` and example renders correctly | +| M6. Example from fixture | Example data matches `src/example_db/fixtures/examples.json` | +| M7. Pred commands | Example section contains `pred-commands(` with create/reduce/evaluate pipeline | +| M8. Both directions | If the reverse rule also exists in the graph, check it has its own entry | + +**Critical checks:** + +| Check | Criterion | +|-------|-----------| +| C1. Construction correctness | Does the theorem statement accurately describe what `reduce_to()` does? Read `src/rules/_.rs` to verify | +| C2. Proof correctness | Does the proof correctly argue that the reduction preserves solutions? | +| C3. Example clarity | Does the example clearly show source → target → solution extraction? | +| C4. Proof-only flag | If this is a proof-only reduction (not solver-executable), is that stated? | + +## Step 3: Generate Report + +Present results **one entry at a time** in this format: + +``` +### [N/10] ProblemName (or Source → Target) + +**Mechanical Issues:** +- [PASS] M1. Display name +- [FAIL] M5. Example present — no worked example in body +- [WARN] M9. Algorithm citation — complexity claim "O*(2^n)" has no @citation + +**Critical Issues:** +- [FAIL] C2. Background quality — body is only one sentence ("This is NP-hard.") + with no applications, history, or algorithmic context +- [OK] C1. Definition correctness — matches Rust implementation + +**Verdict:** 2 mechanical fails, 1 critical fail — needs improvement +``` + +After each entry, pause and ask: **"Continue to next entry, or discuss this one?"** + +Use these severity levels: +- **PASS** — meets criterion +- **WARN** — minor issue, could be improved but acceptable +- **FAIL** — does not meet criterion, should be fixed + +## Step 4: Session Summary + +After all 10 entries, print a summary table: + +``` +## Session Summary + +| Entry | Mechanical | Critical | Verdict | +|-------|-----------|----------|---------| +| ProblemA | 9/10 pass | 4/4 pass | Good | +| ProblemB | 7/10 pass | 3/4 pass | Needs work | +| ... | ... | ... | ... | + +Overall: X/10 entries pass all checks. +Top priorities for improvement: [list the 3 worst entries] +``` + +## Step 5: Save Progress + +Save progress to memory so the next session can continue where this one left off. Record which entries have been reviewed and their verdicts. + +## Important Rules + +1. **Do not modify any files.** This skill is read-only. +2. **Do not invent issues.** Only report problems you can verify by reading the source. +3. **Check the Rust source** for critical checks — don't guess whether the math is right. +4. **Be specific.** "Background is thin" is not useful. "Background is one sentence with no applications or algorithmic context" is useful. +5. **Compare to gold standard.** The MIS entry is the reference — entries don't need to be as long, but they should cover the same structural elements. diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index e64bb909..6b4cd724 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -838,6 +838,14 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| "pred solve vc.json", "pred evaluate vc.json --config " + sol.map(str).join(","), ) + + #figure({ + let edges = inner.graph.edges.map(e => (e.at(0), e.at(1))) + let verts = ((0, 0), (1, 0), (0.5, 1), (1.5, 1)) + draw-node-highlight(verts, edges, cover) + }, + caption: [A graph on #nv vertices with vertex cover $S = {#cover.map(i => $v_#i$).join(", ")}$ (blue). Total weight $|S| = #{cover.len()} <= k = #k$, certifying a yes-instance.], + ) ] ] } @@ -1020,7 +1028,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("BiconnectivityAugmentation")[ Given an undirected graph $G = (V, E)$, a set $F$ of candidate edges on $V$ with $F inter E = emptyset$, weights $w: F -> RR$, and a budget $B in RR$, find $F' subset.eq F$ such that $sum_(e in F') w(e) <= B$ and the augmented graph $G' = (V, E union F')$ is biconnected, meaning $G'$ is connected and deleting any single vertex leaves it connected. ][ - Biconnectivity augmentation is a classical network-design problem: add backup links so the graph survives any single vertex failure. The weighted candidate-edge formulation modeled here captures communication, transportation, and infrastructure planning settings where only a prescribed set of new links is feasible and each carries a cost. In this library, the exact baseline is brute-force enumeration over the $m = |F|$ candidate edges, yielding $O^*(2^m)$ time and matching the exported complexity metadata for the model. + Biconnectivity augmentation is a classical network-design problem: add backup links so the graph survives any single vertex failure. Eswaran and Tarjan @eswarantarjan1976 showed that the unweighted version (finding the minimum number of edges to add) is solvable in linear time. Frederickson and Ja'Ja' @fredericksonjaja1981 proved that the weighted version is NP-complete, even when the input graph is a tree and edge weights are restricted to ${1, 2}$. The weighted candidate-edge formulation modeled here captures communication, transportation, and infrastructure planning settings where only a prescribed set of new links is feasible and each carries a cost. In this library, the exact baseline is brute-force enumeration over the $m = |F|$ candidate edges, yielding $O^*(2^m)$ time and matching the exported complexity metadata for the model. *Example.* Consider the path graph #range(nv).map(i => $v_#i$).join($-$) with candidate edges #candidates.map(c => $(v_#(c.u), v_#(c.v))$).join(", ") carrying weights $(#candidates.map(c => str(c.w)).join(", "))$ and budget $B = #budget$. Selecting $F' = {#sel-idx.map(i => $(v_#(candidates.at(i).u), v_#(candidates.at(i).v))$).join(", ")}$ uses total weight $#sel-idx.map(i => str(candidates.at(i).w)).join(" + ") = #sel-weight$ and eliminates every articulation point: after deleting any single vertex, the remaining graph is still connected. @@ -1352,7 +1360,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| ][ Disjoint Connecting Paths is the classical routing form of the vertex-disjoint paths problem, catalogued as ND40 in Garey & Johnson @garey1979. When the number of terminal pairs $k$ is part of the input, the problem is NP-complete @karp1972. In contrast, for every fixed $k$, Robertson and Seymour give an $O(n^3)$ algorithm @robertsonSeymour1995, and Kawarabayashi, Kobayashi, and Reed later improve the dependence on $n$ to $O(n^2)$ @kawarabayashiKobayashiReed2012. The implementation in this crate uses one binary variable per undirected edge, so brute-force search explores an $O^*(2^|E|)$ configuration space.#footnote[This is the exact-search bound induced by the edge-subset encoding implemented in the codebase; no sharper general exact worst-case bound is claimed here.] - *Example.* Consider the repaired YES instance with $n = #nv$ vertices, $|E| = #ne$ edges, and terminal pairs $(v_0, v_3)$ and $(v_2, v_5)$. Selecting the edges $v_0v_1$, $v_1v_3$, $v_2v_4$, and $v_4v_5$ yields the two vertex-disjoint paths $v_0 arrow v_1 arrow v_3$ and $v_2 arrow v_4 arrow v_5$, so the instance is satisfying. + *Example.* Consider the canonical YES instance with $n = #nv$ vertices, $|E| = #ne$ edges, and terminal pairs $(v_0, v_3)$ and $(v_2, v_5)$. Selecting the edges $v_0v_1$, $v_1v_3$, $v_2v_4$, and $v_4v_5$ yields the two vertex-disjoint paths $v_0 arrow v_1 arrow v_3$ and $v_2 arrow v_4 arrow v_5$, so the instance is satisfying. #pred-commands( "pred create --example DisjointConnectingPaths -o disjoint-connecting-paths.json", @@ -1592,9 +1600,9 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("DirectedHamiltonianPath")[ Given a directed graph $G = (V, A)$, determine whether $G$ contains a _directed Hamiltonian path_, i.e., a simple directed path that visits every vertex exactly once following arc directions. ][ - A classical NP-complete decision problem from Garey & Johnson (A2.1 GT39). The directed version is NP-complete even for tournaments and remains hard for most restricted digraph classes. + A classical NP-complete decision problem from Garey & Johnson (A2.1 GT39) @garey1979. The directed version is NP-complete even for tournaments and remains hard for most restricted digraph classes. Directed Hamiltonian paths arise naturally in genome assembly (finding Eulerian or Hamiltonian traversals of de Bruijn graphs), job sequencing with precedence constraints, and one-way street routing. - The best known exact algorithm runs in $O(n^2 dot 2^n)$ time using Held--Karp style dynamic programming with bitmask DP. + Björklund's randomized $O^*(1.657^n)$ algebraic method applies to directed graphs as well as undirected ones @bjorklund2014. The classical Held--Karp dynamic programming algorithm @heldkarp1962 gives a deterministic $O(n^2 dot 2^n)$ bound by tracking visited vertex subsets with bitmask DP. *Example.* Consider the directed graph $G$ on #nv vertices with arcs ${#arcs.map(((u, v)) => $(#u arrow.r #v)$).join(", ")}$. The directed Hamiltonian path $#path-order.map(v => $v_#v$).join($arrow.r$)$ visits every vertex exactly once with all consecutive pairs being arcs. @@ -1654,7 +1662,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("Kernel")[ Given a directed graph $G = (V, A)$, find a _kernel_ $V' subset.eq V$ such that (1) $V'$ is _independent_ — no arc joins any two vertices in $V'$ — and (2) $V'$ is _absorbing_ — every vertex $u in.not V'$ has an arc $(u, v) in A$ for some $v in V'$. ][ - A classical graph-theoretic concept introduced by von Neumann and Morgenstern (1944) in the context of game theory. Deciding whether a directed graph has a kernel is NP-complete in general, though every DAG has a unique kernel. Kernels appear in combinatorial game theory, graph coloring (Galvin's theorem), and stable set problems on digraphs. + A classical graph-theoretic concept introduced by von Neumann and Morgenstern @vonNeumannMorgenstern1944 in the context of game theory. Chvátal showed that deciding whether a directed graph has a kernel is NP-complete in general @chvatal1973, though Richardson proved that every DAG has a unique kernel @richardson1953. Kernels appear in combinatorial game theory, graph coloring (Galvin's theorem on list-chromatic index @galvin1995), and stable set problems on digraphs. Variables: A binary vector of length $|V|$, where $x_v = 1$ iff vertex $v$ is in the kernel. @@ -2202,7 +2210,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| let color-groups = range(k).map(c => coloring.enumerate().filter(((i, v)) => v == c).map(((i, _)) => i)) [ #problem-def("KColoring")[ - Given $G = (V, E)$ and $k$ colors, find $c: V -> {1, ..., k}$ minimizing $|{(u, v) in E : c(u) = c(v)}|$. + Given $G = (V, E)$ and a positive integer $k$, determine whether there exists a proper $k$-coloring $c: V -> {1, ..., k}$ such that $c(u) eq.not c(v)$ for every $(u, v) in E$. ][ Graph coloring arises in register allocation, frequency assignment, and scheduling @garey1979. Deciding $k$-colorability is NP-complete for $k >= 3$ but solvable in $O(n+m)$ for $k=2$ via bipartiteness testing. For $k = 3$, the best known algorithm runs in $O^*(1.3289^n)$ @beigel2005; for $k = 4$ in $O^*(1.7159^n)$ @wu2024; for $k = 5$ in $O^*((2-epsilon)^n)$ @zamir2021. In general, inclusion-exclusion achieves $O^*(2^n)$ @bjorklund2009. @@ -2236,7 +2244,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("MaximumAchromaticNumber")[ Given an undirected graph $G = (V, E)$, find a proper vertex coloring $c: V -> {1, dots, k}$ that is _complete_ --- for every pair of distinct colors $i, j$ there exists an edge $(u, v) in E$ with $c(u) = i$ and $c(v) = j$ --- maximizing the number of colors $k$. ][ - The achromatic number $psi(G)$ is the largest $k$ such that $G$ admits a complete proper $k$-coloring. It was introduced by Harary and Hedetniemi (1970) and shown NP-hard @garey1979[GT5]. Applications include network partition and information dissemination. Brute-force enumeration runs in $O^*(n^n)$ time. + The achromatic number $psi(G)$ is the largest $k$ such that $G$ admits a complete proper $k$-coloring. It was introduced by Harary and Hedetniemi (1970) and shown NP-complete by Yannakakis and Gavril @yannakakis1980 (as a corollary of edge dominating set hardness). Garey and Johnson list it as GT5 @garey1979. Applications include network partition and information dissemination. Brute-force enumeration runs in $O^*(n^n)$ time. *Example.* Consider the 6-cycle $C_6$ with $n = #nv$ vertices and $|E| = #ne$ edges: #edges.map(((u, v)) => [${#u, #v}$]).join(", "). The coloring #range(nv).map(i => $c(v_#i) = #(coloring.at(i) + 1)$).join(", ") uses $#num-colors$ colors. It is proper (no adjacent pair shares a color) and complete: every pair of color classes is connected by at least one edge. Thus $psi(C_6) >= #num-colors$. @@ -2245,6 +2253,17 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| "pred solve achromatic.json", "pred evaluate achromatic.json --config " + x.optimal_config.map(str).join(","), ) + + #figure({ + let r = 1.1 + let hex-verts = range(nv).map(i => { + let angle = calc.pi / 2 + 2 * calc.pi * i / nv + (r * calc.cos(angle), r * calc.sin(angle)) + }) + draw-node-colors(hex-verts, edges, coloring) + }, + caption: [A complete proper coloring of $C_6$ with $psi(C_6) = #num-colors$ colors. Every pair of distinct colors is connected by at least one edge, so the coloring is complete.], + ) ] ] } @@ -2299,7 +2318,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("MinimumGeometricConnectedDominatingSet")[ Given points $P = {p_1, dots, p_n}$ in $RR^2$ and distance threshold $B > 0$, find $P' subset.eq P$ minimizing $|P'|$ s.t. (1) $forall p in P backslash P': exists q in P'$ with $d(p,q) <= B$ (domination), and (2) the unit-disk graph on $P'$ with radius $B$ is connected. ][ - Geometric Connected Dominating Set arises in wireless ad-hoc networks: selected nodes form a connected backbone that covers all other nodes within communication range. The problem is NP-hard and generalizes both dominating set (dropping connectivity) and connected subgraph (dropping domination). + Geometric Connected Dominating Set arises in wireless ad-hoc networks: selected nodes form a connected backbone that covers all other nodes within communication range. Clark, Colbourn, and Johnson showed that domination and connected domination on unit disk graphs are NP-complete @clark1990; the geometric variant inherits this hardness. The problem generalizes both dominating set (dropping connectivity) and connected subgraph (dropping domination). Brute-force enumeration runs in $O^*(2^n)$ time. *Example.* Consider $n = #n$ points arranged in a $4 times 2$ ladder with spacing $3$ and threshold $B = #B$. The bottom row $P' = {#S.map(i => $p_#i$).join(", ")}$ forms a minimum connected dominating set of size $#wS$: each bottom-row point dominates the top-row point directly above it (vertical distance $3 <= #B$), and consecutive bottom-row points are within distance $3 <= #B$ of each other, so $P'$ induces a connected path. @@ -2308,6 +2327,43 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| "pred solve mgcds.json", "pred evaluate mgcds.json --config " + x.optimal_config.map(str).join(","), ) + + #figure({ + let blue = graph-colors.at(0) + let gray = luma(200) + // Manual layout: 4×2 grid, bottom row y=0, top row y=1.4, columns spaced 1.5 + let disp = ( + (0, 0), (1.5, 0), (3.0, 0), (4.5, 0), // bottom: p0–p3 + (0, 1.4), (1.5, 1.4), (3.0, 1.4), (4.5, 1.4), // top: p4–p7 + ) + // In the original coordinate system, spacing=3 and B=3.5. + // Display scale factor = 1.5/3 = 0.5, so disk radius = 3.5*0.5 = 1.75. + // That still overwhelms. Instead, draw a dashed "coverage arc" from each + // selected point to its dominated neighbor — clearer than huge overlapping disks. + canvas(length: 1cm, { + import draw: * + // Draw edges between points within distance B (vertical=3 ≤ 3.5, horizontal=3 ≤ 3.5, diagonal=√18 > 3.5) + let adj = ((0,1),(1,2),(2,3),(0,4),(1,5),(2,6),(3,7),(4,5),(5,6),(6,7)) + for (i, j) in adj { + let on-backbone = S.contains(i) and S.contains(j) + g-edge(disp.at(i), disp.at(j), stroke: if on-backbone { 2pt + blue } else { 0.8pt + gray }) + } + // Domination arcs: dashed blue from selected to dominated neighbor + let dom-edges = ((0,4),(1,5),(2,6),(3,7)) + for (i, j) in dom-edges { + g-edge(disp.at(i), disp.at(j), stroke: (paint: blue, thickness: 1.2pt, dash: "dashed")) + } + // Draw points + for (k, pos) in disp.enumerate() { + let selected = S.contains(k) + g-node(pos, name: "p" + str(k), + fill: if selected { blue } else { white }, + label: if selected { text(fill: white)[$p_#k$] } else { [$p_#k$] }) + } + }) + }, + caption: [Geometric Connected Dominating Set on a $4 times 2$ ladder ($B = #B$). Blue points $P' = {#S.map(i => $p_#i$).join(", ")}$ form the connected backbone (solid blue edges). Dashed blue edges show domination: each top-row point is within distance $3 <= #B$ of the bottom-row point below it.], + ) ] ] } @@ -2318,20 +2374,51 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| let edges = x.instance.graph.edges let sol = (config: x.optimal_config, metric: x.optimal_value) let num-cliques = metric-value(sol.metric) - let groups = range(num-cliques).map(c => sol.config.enumerate().filter(((i, v)) => v == c).map(((i, _)) => i)) + let edge-groups = range(num-cliques).map(c => sol.config.enumerate().filter(((i, v)) => v == c).map(((i, _)) => i)) + // Convert edge-index groups to vertex sets (cliques) + let clique-verts = edge-groups.map(eg => { + let verts = () + for idx in eg { + let (u, v) = edges.at(idx) + if u not in verts { verts.push(u) } + if v not in verts { verts.push(v) } + } + verts.sorted() + }) [ #problem-def("MinimumCoveringByCliques")[ Given an undirected graph $G = (V, E)$, find a collection of cliques $C_1, dots, C_k$ in $G$ such that every edge $e in E$ is contained in at least one $C_i$, and the number of cliques $k$ is minimized. ][ - Minimum Covering by Cliques (also called _edge clique cover_) is NP-hard @garey1979[GT59]. Applications include intersection graph recognition and computational biology. The minimum edge clique cover number equals the minimum dimension of a dot-product representation of the graph. Brute-force enumeration runs in $O^*(2^(|E|))$ time. + Minimum Covering by Cliques (also called _edge clique cover_) is NP-hard @garey1979[GT59]. Applications include intersection graph recognition and computational biology. The minimum edge clique cover number equals the minimum dimension of a dot-product representation of the graph @erdosgoodmanposa1966. Gramm et al. give an exact branch-and-reduce algorithm with a kernel of at most $2^k$ vertices @gramm2009. - *Example.* Consider $G$ with $n = #nv$ vertices and $|E| = #ne$ edges: #edges.map(((u, v)) => [${#u, #v}$]).join(", "). An optimal cover uses $#num-cliques$ cliques: #groups.enumerate().filter(((_, g)) => g.len() > 0).map(((i, g)) => [$C_#(i + 1)$: edges #g.map(j => str(j)).join(", ")]).join("; "). + *Example.* Consider $G$ with $n = #nv$ vertices and $|E| = #ne$ edges: #edges.map(((u, v)) => [${#u, #v}$]).join(", "). An optimal cover uses $#num-cliques$ cliques: #clique-verts.enumerate().filter(((_, vs)) => vs.len() > 0).map(((i, vs)) => [$C_#(i + 1) = {#vs.map(v => $v_#v$).join(", ")}$]).join(", "). Each $C_i$ is a triangle in $G$, and every edge belongs to at least one of these triangles. #pred-commands( "pred create --example MinimumCoveringByCliques -o covering-by-cliques.json", "pred solve covering-by-cliques.json", "pred evaluate covering-by-cliques.json --config " + x.optimal_config.map(str).join(","), ) + + #figure({ + let blue = graph-colors.at(0) + let gray = luma(200) + // Layout: 4 inner vertices (0-3) as a square, 2 outer (4,5) + let verts = ((0, 0), (1.5, 0), (1.5, 1.5), (0, 1.5), (-0.8, -0.6), (2.3, 2.1)) + let clique-colors = (graph-colors.at(0), graph-colors.at(1), graph-colors.at(2), rgb("#f28e2b")) + canvas(length: 1cm, { + import draw: * + // Draw edges colored by their clique assignment + for (idx, (u, v)) in edges.enumerate() { + let c = sol.config.at(idx) + g-edge(verts.at(u), verts.at(v), stroke: 1.5pt + clique-colors.at(c)) + } + for (k, pos) in verts.enumerate() { + g-node(pos, name: "v" + str(k), label: [$v_#k$]) + } + }) + }, + caption: [Edge clique cover of $G$ with #num-cliques cliques. Each color represents one clique: #clique-verts.enumerate().filter(((_, vs)) => vs.len() > 0).map(((i, vs)) => [$C_#(i + 1) = {#vs.map(v => $v_#v$).join(", ")}$]).join(", ").], + ) ] ] } @@ -2346,15 +2433,40 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("MinimumIntersectionGraphBasis")[ Given an undirected graph $G = (V, E)$, find a universe $U$ of minimum cardinality and an assignment of subsets $S_v subset.eq U$ for each vertex $v in V$ such that two vertices $u, v$ are adjacent if and only if $S_u inter S_v eq.not emptyset$. The minimum $|U|$ is the _intersection number_ of $G$. ][ - Minimum Intersection Graph Basis is NP-hard @garey1979[GT60]. Every graph is an intersection graph; the intersection number measures how compactly such a representation can be chosen. The intersection number is at most $|E|$. Brute-force enumeration runs in $O^*(|E|^(|E|))$ time. + Minimum Intersection Graph Basis is NP-hard @garey1979[GT60]. Erdős, Goodman, and Pósa showed that the intersection number equals the minimum edge clique cover number and is at most $floor(n^2 slash 4)$ @erdosgoodmanposa1966. Applications include bandwidth allocation in fiber-optic networks, scheduling shared resources, and formulating compact integer-programming relaxations for independent-set problems. Brute-force enumeration runs in $O^*(|E|^(|E|))$ time. - *Example.* Consider the path $P_3$ with $n = #nv$ vertices and $|E| = #ne$ edges: #edges.map(((u, v)) => [${#u, #v}$]).join(", "). An optimal representation uses $#universe-size$ elements: $S_0 = {0}$, $S_1 = {0, 1}$, $S_2 = {1}$. + *Example.* Consider the path $P_3$ with $n = #nv$ vertices and $|E| = #ne$ edges: #edges.map(((u, v)) => [${#u, #v}$]).join(", "). An optimal representation uses $#universe-size$ elements: $S_0 = {0}$, $S_1 = {0, 1}$, $S_2 = {1}$. Edges are witnessed by shared elements ($S_0 inter S_1 = {0}$, $S_1 inter S_2 = {1}$), and the non-edge $(0, 2)$ is confirmed by $S_0 inter S_2 = emptyset$. #pred-commands( "pred create --example MinimumIntersectionGraphBasis -o intersection-basis.json", "pred solve intersection-basis.json", "pred evaluate intersection-basis.json --config " + x.optimal_config.map(str).join(","), ) + + #figure({ + let blue = graph-colors.at(0) + let orange = graph-colors.at(1) + let gray = luma(200) + canvas(length: 1cm, { + import draw: * + // P3: v0 — v1 — v2 + let verts = ((0, 0), (1.8, 0), (3.6, 0)) + g-edge(verts.at(0), verts.at(1), stroke: 1.5pt + blue) + g-edge(verts.at(1), verts.at(2), stroke: 1.5pt + orange) + for (k, pos) in verts.enumerate() { + g-node(pos, name: "v" + str(k), label: [$v_#k$]) + } + // Subset labels below each vertex + draw.content((0, -0.6), text(8pt)[$S_0 = {0}$]) + draw.content((1.8, -0.6), text(8pt)[$S_1 = {0, 1}$]) + draw.content((3.6, -0.6), text(8pt)[$S_2 = {1}$]) + // Element labels on edges + draw.content((0.9, 0.35), text(7pt, fill: blue)[$inter = {0}$]) + draw.content((2.7, 0.35), text(7pt, fill: orange)[$inter = {1}$]) + }) + }, + caption: [Intersection graph representation of $P_3$ with intersection number $#universe-size$. Each vertex $v_i$ is assigned a subset $S_i subset.eq {0, 1}$; adjacent vertices share an element, non-adjacent vertices have disjoint subsets.], + ) ] ] } @@ -2782,6 +2894,47 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| "pred solve optimal-linear-arrangement.json", "pred evaluate optimal-linear-arrangement.json --config " + x.optimal_config.map(str).join(","), ) + + // Build inverse mapping: pos[p] = vertex placed at position p + #let inv = range(nv).map(p => config.position(c => c == p)) + #figure({ + let spacing = 1.2 + canvas(length: 1cm, { + // Number-line tick marks + for p in range(nv) { + draw.line((p * spacing, -0.12), (p * spacing, 0.12), stroke: 0.5pt + luma(160)) + draw.content((p * spacing, -0.35), text(7pt, fill: luma(100))[#p]) + } + // Vertices at their assigned positions + for v in range(nv) { + let p = config.at(v) + g-node((p * spacing, 0), name: "v" + str(v), + fill: graph-colors.at(0), + label: text(fill: white)[$v_#v$]) + } + // Edges as arcs above the line + for (u, v) in edges { + let pu = config.at(u) + let pv = config.at(v) + let span = calc.abs(pu - pv) + let rise = 0.35 + 0.25 * span + let mid-x = (pu + pv) / 2 * spacing + let left-x = calc.min(pu, pv) * spacing + let right-x = calc.max(pu, pv) * spacing + // Shorten endpoints to avoid overlap with vertex circles + let r = 0.24 + let p0 = (left-x + r, r * rise / (spacing * span / 2)) + let p1 = (right-x - r, r * rise / (spacing * span / 2)) + let ctrl = (mid-x, rise) + draw.bezier(p0, p1, ctrl, + stroke: if span > 1 { 1.4pt + graph-colors.at(0) } else { 1pt + luma(160) }) + draw.content((mid-x, rise + 0.2), + text(7pt, fill: if span > 1 { graph-colors.at(0) } else { luma(100) })[#span]) + } + }) + }, + caption: [Optimal linear arrangement of #nv vertices. Each vertex $v_i$ is placed at position $f(v_i)$ on a number line. Arcs show edges; labels give stretch $|f(u) - f(v)|$. Cross-edges $(v_0, v_3)$ and $(v_2, v_5)$ (blue arcs, stretch 3) dominate the total cost #total-cost.], + ) ] ] } @@ -2806,6 +2959,48 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| "pred solve rooted-tree-arrangement.json --solver brute-force", "pred evaluate rooted-tree-arrangement.json --config " + x.optimal_config.map(str).join(","), ) + + #figure({ + // Left: source graph G. Right: chain tree T with identity mapping. + let blue = graph-colors.at(0) + canvas(length: 1cm, { + // --- Source graph G (left) --- + let gv = ((0, 1.5), (1.5, 1.5), (1.5, 0), (3.0, 0)) + for (idx, (u, v)) in edges.enumerate() { + g-edge(gv.at(u), gv.at(v), stroke: 1pt + luma(160)) + } + for (k, pos) in gv.enumerate() { + g-node(pos, name: "g" + str(k), + fill: blue, + label: text(fill: white)[$v_#k$]) + } + draw.content((1.5, -0.7), text(9pt)[$G$]) + + // Arrow between the two diagrams + draw.content((4.2, 0.75), text(10pt)[$arrow.r.double$]) + + // --- Chain tree T (right) --- + let tv = ((5.4, 2.4), (5.4, 1.6), (5.4, 0.8), (5.4, 0)) + for i in range(3) { + draw.line(tv.at(i), tv.at(i + 1), stroke: 1.4pt + blue) + } + for (k, pos) in tv.enumerate() { + g-node(pos, name: "t" + str(k), + fill: if k == 0 { blue } else { white }, + stroke: if k == 0 { none } else { 1pt + blue }, + label: if k == 0 { text(fill: white)[$u_#k$] } else { [$u_#k$] }) + } + draw.content((5.4, -0.7), text(9pt)[$T$ (chain)]) + + // Stretch labels on the right side of the chain + for i in range(3) { + let my = (tv.at(i).at(1) + tv.at(i + 1).at(1)) / 2 + draw.content((6.1, my), text(7pt, fill: luma(100))[1]) + } + }) + }, + caption: [Source graph $G$ (left) mapped to a chain tree $T$ (right) via $f = "id"$. The root $u_0$ (filled) heads the chain $u_0 dash u_1 dash u_2 dash u_3$. Each graph edge maps to a pair on the root-to-leaf path with total stretch $d_T(v_0, v_1) + d_T(v_0, v_2) + d_T(v_1, v_2) + d_T(v_2, v_3) = 1 + 2 + 1 + 1 = 5 <= K$.], + ) ] ] } @@ -2891,7 +3086,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("MaximalIS")[ Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that $S$ is independent ($forall u, v in S: (u, v) in.not E$) and maximal (no vertex $u in V backslash S$ can be added to $S$ while maintaining independence). ][ - The maximality constraint (no vertex can be added) distinguishes this from MIS, which only requires maximum weight. Every maximum independent set is maximal, but not vice versa. The enumeration bound of $O^*(3^(n slash 3))$ for listing all maximal independent sets @tomita2006 is tight: Moon and Moser @moonmoser1965 showed every $n$-vertex graph has at most $3^(n slash 3)$ maximal independent sets, achieved by disjoint triangles. + The maximality constraint (no vertex can be added without violating independence) distinguishes this from Maximum Independent Set (MIS). In MIS, the feasible set is _all_ independent sets and the objective is to maximize weight; here, the feasible set is restricted to _maximal_ independent sets only. Every maximum independent set is maximal, but the converse fails: a maximal IS can be arbitrarily smaller than the maximum. For unit weights the two optima coincide in value, but the search spaces differ — MaximalIS must certify that every non-selected vertex has a neighbor in $S$, a domination-like constraint absent from MIS. Indeed, a maximal independent set is equivalently an independent dominating set, linking MaximalIS to Minimum Dominating Set. The enumeration bound of $O^*(3^(n slash 3))$ for listing all maximal independent sets @tomita2006 is tight: Moon and Moser @moonmoser1965 showed every $n$-vertex graph has at most $3^(n slash 3)$ maximal independent sets, achieved by disjoint triangles. *Example.* Consider the path graph $P_#nv$ with $n = #nv$ vertices, edges $(v_i, v_(i+1))$ for $i = 0, ..., #(ne - 1)$, and unit weights $w(v) = 1$. The set $S = {#S-sub.map(i => $v_#i$).join(", ")}$ is a maximal independent set: no two vertices in $S$ are adjacent, and neither $v_0$ (adjacent to $v_1$), $v_2$ (adjacent to both), nor $v_4$ (adjacent to $v_3$) can be added. However, $S' = {#S-opt.map(i => $v_#i$).join(", ")}$ with $w(S') = #w-opt$ is a strictly larger maximal IS, illustrating that maximality does not imply maximum weight. @@ -2922,9 +3117,9 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| #problem-def("MinimumMaximalMatching")[ Given $G = (V, E)$, find $M subset.eq E$ of minimum cardinality such that $M$ is a matching and $M$ is maximal: every $e in E backslash M$ shares an endpoint with some $e' in M$. ][ - A maximal matching cannot be extended by any edge, so every non-selected edge must be "blocked" by a selected one. Among all such matchings, the problem seeks one of minimum size. Unlike Maximum Matching (solvable in $O(n^3)$ by Edmonds' algorithm @edmonds1965), Minimum Maximal Matching is NP-hard @yannakakis1980; it can also be viewed as a Minimum Dominating Set in the line graph. + A maximal matching cannot be extended by any edge, so every non-selected edge must be "blocked" by a selected one. Among all such matchings, the problem seeks one of minimum size. Unlike Maximum Matching (solvable in $O(n^3)$ by Edmonds' algorithm @edmonds1965), Minimum Maximal Matching is NP-hard @yannakakis1980; it can also be viewed as a Minimum Dominating Set in the line graph. The problem is equivalent to Minimum Edge Dominating Set, and the best known exact algorithm runs in $O^*(1.3160^n)$ via branch-and-reduce with measure-and-conquer analysis @xiao2014. - *Example.* Consider the path graph $P_#nv$ with $n = #nv$ vertices and $#ne$ edges. A minimum maximal matching is $M = {#matched-edges.map(((u, v)) => $(v_#u, v_#v)$).join(", ")}$ with $|M| = #sz$. Every unselected edge shares an endpoint with a selected one, so $M$ is maximal. + *Example.* Consider the path graph $P_#nv$ with $n = #nv$ vertices and $#ne$ edges. A minimum maximal matching is $M = {#matched-edges.map(((u, v)) => $(v_#u, v_#v)$).join(", ")}$ with $|M| = #sz$. Every unselected edge shares an endpoint with a selected one, so $M$ is maximal and no matching of size less than $#sz$ is maximal on this graph. #pred-commands( "pred create --example MinimumMaximalMatching -o mmm.json", @@ -3049,13 +3244,44 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| ] } -#problem-def("PartitionIntoPathsOfLength2")[ - Given $G = (V, E)$ with $|V| = 3q$, determine if $V$ can be partitioned into $q$ disjoint sets $V_1, ..., V_q$ of three vertices each, such that each $V_t$ induces at least two edges in $G$. -][ -A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], proved hard by reduction from 3-Dimensional Matching. Each triple in the partition must form a path of length 2 (exactly two edges, i.e., a $P_3$ subgraph) or a triangle (all three edges). The problem models constrained grouping scenarios where cluster connectivity is required. The best known exact approach uses subset DP in $O^*(3^n)$ time. +#{ + let x = load-model-example("PartitionIntoPathsOfLength2") + let nv = graph-num-vertices(x.instance) + let edges = x.instance.graph.edges + let ne = edges.len() + let q = calc.div-euclid(nv, 3) + let config = x.optimal_config + // Group vertices by partition assignment + let groups = range(q).map(g => config.enumerate().filter(((i, c)) => c == g).map(((i, _)) => i)) + // Count induced edges per group + let group-edges(g) = edges.filter(((u, v)) => config.at(u) == g and config.at(v) == g) + [ + #problem-def("PartitionIntoPathsOfLength2")[ + Given $G = (V, E)$ with $|V| = 3q$, determine if $V$ can be partitioned into $q$ disjoint sets $V_1, ..., V_q$ of three vertices each, such that each $V_t$ induces at least two edges in $G$. + ][ + A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], proved hard by reduction from 3-Dimensional Matching. Each triple in the partition must form a path of length 2 (exactly two edges, i.e., a $P_3$ subgraph) or a triangle (all three edges). The problem models constrained grouping scenarios where cluster connectivity is required. The best known exact approach uses subset DP in $O^*(3^n)$ time. -*Example.* Consider the graph $G$ with $n = 9$ vertices and edges ${0,1}, {1,2}, {3,4}, {4,5}, {6,7}, {7,8}$ (plus cross-edges ${0,3}, {2,5}, {3,6}, {5,8}$). Setting $q = 3$, the partition $V_1 = {0,1,2}$, $V_2 = {3,4,5}$, $V_3 = {6,7,8}$ is valid: $V_1$ contains edges ${0,1}, {1,2}$ (path $0 dash.em 1 dash.em 2$), $V_2$ contains ${3,4}, {4,5}$, and $V_3$ contains ${6,7}, {7,8}$. -] + *Example.* Consider the $3 times 3$ grid-like graph $G$ with $n = #nv$ vertices and $|E| = #ne$ edges (three row-paths plus six cross-edges), and $q = #q$. The row partition #range(q).map(g => $V_#(g + 1) = {#groups.at(g).map(i => $v_#i$).join(", ")}$).join(", ") is valid: #range(q).map(g => { + let ge = group-edges(g) + [$V_#(g + 1)$ induces edges #ge.map(((u, v)) => $\{v_#u, v_#v\}$).join(", ") (path $#groups.at(g).map(i => $v_#i$).join($dash.em$)$)] + }).join("; "). The cross-edges also admit a column partition ${v_0, v_3, v_6}, {v_1, v_4, v_7}, {v_2, v_5, v_8}$ and several mixed groupings — the combinatorial competition among overlapping triples is what makes the problem NP-hard in general. + + #pred-commands( + "pred create --example PartitionIntoPathsOfLength2 -o partition-paths2.json", + "pred solve partition-paths2.json", + "pred evaluate partition-paths2.json --config " + x.optimal_config.map(str).join(","), + ) + + #figure({ + // 3x3 grid layout: row r, column c -> vertex 3r+c + let verts = range(nv).map(i => (calc.rem(i, 3) * 1.8, -calc.div-euclid(i, 3) * 1.5)) + draw-node-colors(verts, edges, config) + }, + caption: [Partition into Paths of Length 2 on a $3 times 3$ grid-like graph ($q = #q$). The row partition #range(q).map(g => $V_#(g + 1) = {#groups.at(g).map(i => $v_#i$).join(", ")}$).join(", ") is shown; cross-edges also admit a column partition and mixed groupings.], + ) + ] + ] +} #{ let x = load-model-example("SteinerTreeInGraphs") @@ -3139,9 +3365,9 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], #problem-def("MinimumSumMulticenter")[ Given a graph $G = (V, E)$ with vertex weights $w: V -> ZZ_(>= 0)$, edge lengths $l: E -> ZZ_(>= 0)$, and a positive integer $K <= |V|$, find a set $P subset.eq V$ of $K$ vertices (centers) that minimizes the total weighted distance $sum_(v in V) w(v) dot d(v, P)$, where $d(v, P) = min_(p in P) d(v, p)$ is the shortest-path distance from $v$ to the nearest center in $P$. ][ - Also known as the _p-median problem_. This is a classical NP-complete facility location problem from Garey & Johnson (A2 ND51). The goal is to optimally place $K$ service centers (e.g., warehouses, hospitals) to minimize total service cost. NP-completeness was established by Kariv and Hakimi (1979) via transformation from Dominating Set. The problem remains NP-complete even with unit weights and unit edge lengths, but is solvable in polynomial time for fixed $K$ or when $G$ is a tree. + Also known as the _p-median problem_. This is a classical NP-complete facility location problem from Garey & Johnson (A2 ND51). The goal is to optimally place $K$ service centers (e.g., warehouses, hospitals) to minimize total service cost. NP-completeness was established by Kariv and Hakimi @karivhakimi1979 via transformation from Dominating Set. The problem remains NP-complete even with unit weights and unit edge lengths, but is solvable in polynomial time for fixed $K$ or when $G$ is a tree. - The best known exact algorithm runs in $O^*(2^n)$ time by brute-force enumeration of all $binom(n, K)$ vertex subsets. Constant-factor approximation algorithms exist: Charikar et al. (1999) gave the first constant-factor result, and the best known ratio is $(2 + epsilon)$ by Cohen-Addad et al. (STOC 2022). + The best known exact algorithm runs in $O^*(2^n)$ time by brute-force enumeration of all $binom(n, K)$ vertex subsets. Constant-factor approximation algorithms exist, and the best known ratio is $(2 + epsilon)$ by Cohen-Addad et al. @cohenaddad2022. *Example.* Consider the graph $G$ on #nv vertices with unit weights $w(v) = 1$ and unit edge lengths, edges ${#edges.map(((u, v)) => $(#u, #v)$).join(", ")}$, and $K = #K$. Placing centers at $P = {#centers.map(i => $v_#i$).join(", ")}$ gives distances $d(v_0) = 2$, $d(v_1) = 1$, $d(v_2) = 0$, $d(v_3) = 1$, $d(v_4) = 1$, $d(v_5) = 0$, $d(v_6) = 1$, for a total cost of $2 + 1 + 0 + 1 + 1 + 0 + 1 = #opt-cost$. This is optimal. @@ -3186,11 +3412,11 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], #problem-def("MinMaxMulticenter")[ Given a graph $G = (V, E)$ with vertex weights $w: V -> ZZ_(>= 0)$, edge lengths $l: E -> ZZ_(>= 0)$, and a positive integer $K <= |V|$, find $S subset.eq V$ with $|S| = K$ that minimizes $max_(v in V) w(v) dot d(v, S)$, where $d(v, S) = min_(s in S) d(v, s)$ is the shortest weighted-path distance from $v$ to the nearest vertex in $S$. ][ - Also known as the _vertex p-center problem_ (Garey & Johnson A2 ND50). The goal is to place $K$ facilities so that the worst-case weighted distance from any demand point to its nearest facility is minimized. NP-hard even with unit weights and unit edge lengths (Kariv and Hakimi, 1979). + Also known as the _vertex p-center problem_ (Garey & Johnson A2 ND50). The goal is to place $K$ facilities so that the worst-case weighted distance from any demand point to its nearest facility is minimized. NP-hard even with unit weights and unit edge lengths @karivhakimi1979. - Closely related to Dominating Set: on unweighted unit-length graphs, a $K$-center with optimal radius 1 corresponds to a dominating set of size $K$. The best known exact algorithm runs in $O^*(1.4969^n)$ via binary search over distance thresholds combined with dominating set computation @vanrooij2011. An optimal 2-approximation exists (Hochbaum and Shmoys, 1985); no $(2 - epsilon)$-approximation is possible unless $P = "NP"$ (Hsu and Nemhauser, 1979). + Closely related to Dominating Set: on unweighted unit-length graphs, a $K$-center with optimal radius 1 corresponds to a dominating set of size $K$. The best known exact algorithm runs in $O^*(1.4969^n)$ via binary search over distance thresholds combined with dominating set computation @vanrooij2011. An optimal 2-approximation exists @hochbaumshmoys1985; no $(2 - epsilon)$-approximation is possible unless $P = "NP"$ @hsunemhauser1979. - *Example.* Consider the graph $G$ on #nv vertices with unit weights $w(v) = 1$, unit edge lengths, edges ${#edges.map(((u, v)) => $(#u, #v)$).join(", ")}$, and $K = #K$. Placing centers at $S = {#centers.map(i => $v_#i$).join(", ")}$ gives maximum distance $max_v d(v, S) = #opt$, which is optimal. + *Example.* Consider the graph $G$ on #nv vertices with unit weights $w(v) = 1$, unit edge lengths, edges ${#edges.map(((u, v)) => $(#u, #v)$).join(", ")}$, and $K = #K$. Placing centers at $S = {#centers.map(i => $v_#i$).join(", ")}$ gives distances $d(v_0) = 1$, $d(v_1) = 0$, $d(v_2) = 1$, $d(v_3) = 1$, $d(v_4) = 0$, $d(v_5) = 1$, so $max_v d(v, S) = #opt$. The diagonal edge $(1, 4)$ lets centers #centers.map(i => $v_#i$).join(" and ") cover every vertex within distance 1. #pred-commands( "pred create --example MinMaxMulticenter -o min-max-multicenter.json", @@ -3223,18 +3449,24 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], #{ let x = load-model-example("MultipleCopyFileAllocation") + let nv = graph-num-vertices(x.instance) let edges = x.instance.graph.edges.map(e => (e.at(0), e.at(1))) + let usage = x.instance.usage + let storage = x.instance.storage let sol = (config: x.optimal_config, metric: x.optimal_value) let copies = sol.config.enumerate().filter(((i, v)) => v == 1).map(((i, _)) => i) + let opt = metric-value(sol.metric) + let s-cost = copies.map(i => storage.at(i)).sum() + let a-cost = opt - s-cost [ #problem-def("MultipleCopyFileAllocation")[ Given a graph $G = (V, E)$, usage values $u: V -> ZZ_(> 0)$, and storage costs $s: V -> ZZ_(> 0)$, find a subset $V' subset.eq V$ that minimizes $sum_(v in V') s(v) + sum_(v in V) u(v) dot d(v, V'),$ where $d(v, V') = min_(w in V') d_G(v, w)$ is the shortest-path distance from $v$ to the nearest copy vertex. ][ - Multiple Copy File Allocation appears in the storage-and-retrieval section of Garey and Johnson (SR6) @garey1979. The model combines two competing costs: each chosen copy vertex incurs a storage charge, while every vertex pays an access cost weighted by its demand and graph distance to the nearest copy. Garey and Johnson record the problem as NP-hard in the strong sense, even when usage and storage costs are uniform @garey1979. + Multiple Copy File Allocation appears in the storage-and-retrieval section of Garey and Johnson (SR6) @garey1979. The model combines two competing costs: each chosen copy vertex incurs a storage charge, while every vertex pays an access cost weighted by its demand and graph distance to the nearest copy. Applications include content distribution networks (placing cache servers), database replication across data centers, and distributed file systems. Garey and Johnson record the problem as NP-hard in the strong sense, even when usage and storage costs are uniform @garey1979. It generalizes Uncapacitated Facility Location when the network topology is arbitrary. - *Example.* Consider the 6-cycle $C_6$ with uniform usage $u(v) = 10$ and uniform storage $s(v) = 1$. Placing copies at every vertex $V' = {#copies.map(i => $v_#i$).join(", ")}$ gives storage cost $6 dot 1 = 6$ and access cost $0$ (each vertex is distance $0$ from its own copy), for a total cost of $#sol.metric$. This is optimal: removing any copy saves $1$ in storage but adds at least $10$ in access cost for each neighbor that must now reach a more distant copy. + *Example.* Consider the path $P_#nv$ with usage $u = (#usage.map(str).join(", "))$ and storage costs $s = (#storage.map(str).join(", "))$. The endpoints $v_0, v_5$ have high demand ($u = 5$) but expensive storage ($s = 6$), while $v_1, v_4$ are cheap server locations ($s = 2$). Placing copies at $V' = {#copies.map(i => $v_#i$).join(", ")}$ gives storage cost $#copies.map(i => str(storage.at(i))).join(" + ") = #s-cost$ and access cost $5 dot 1 + 1 dot 0 + 1 dot 1 + 1 dot 1 + 1 dot 0 + 5 dot 1 = #a-cost$, for a total of $#opt$. Adding a copy at $v_0$ would save $5 dot 1 = 5$ in access but cost $6$ in storage — a net loss. This tradeoff between placement cost and proximity drives the problem's NP-hardness. #pred-commands( "pred create --example MultipleCopyFileAllocation -o multiple-copy-file-allocation.json", @@ -3247,7 +3479,7 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], let gray = luma(200) canvas(length: 1cm, { import draw: * - let verts = ((0, 1.6), (1.35, 0.8), (1.35, -0.8), (0, -1.6), (-1.35, -0.8), (-1.35, 0.8)) + let verts = range(nv).map(i => (i * 1.5, 0)) for (u, v) in edges { g-edge(verts.at(u), verts.at(v), stroke: 1pt + gray) } @@ -3257,9 +3489,14 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], fill: if has-copy { blue } else { white }, label: if has-copy { text(fill: white)[$v_#k$] } else { [$v_#k$] }) } + // Show usage/storage labels below each vertex + for (k, pos) in verts.enumerate() { + draw.content((pos.at(0), pos.at(1) - 0.65), + text(6.5pt, fill: luma(100))[$u=#(usage.at(k)), s=#(storage.at(k))$]) + } }) }, - caption: [Multiple Copy File Allocation on a 6-cycle. All vertices (shown in blue) host copies; total cost is $#sol.metric$.], + caption: [Multiple Copy File Allocation on $P_#nv$. Copy vertices #copies.map(i => $v_#i$).join(", ") (blue) have cheap storage ($s = #storage.at(copies.at(0))$); endpoints pay access cost instead. Total cost $= #opt$.], ) ] ] @@ -3434,7 +3671,7 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], #problem-def("SetSplitting")[ Given a finite universe $U$ and a collection $cal(C) = {C_1, dots, C_m}$ of subsets of $U$ each of size $gt.eq 2$, does there exist a 2-coloring $chi: U -> {0, 1}$ such that every $C_i$ is non-monochromatic — i.e., contains at least one element of each color? ][ - One of Garey and Johnson's NP-complete problems (SP4 in @garey1979), shown NP-complete by reduction from 3-SAT. It is equivalent to deciding whether a hypergraph is 2-colorable (also called Property B). The problem is trivially satisfiable when every subset has size exactly 2, reducing to 2-colorability of the corresponding graph; it becomes NP-complete for subsets of size $gt.eq 3$. The best known exact algorithm runs in $O^*(2^n)$ by brute-force enumeration over the $n = |U|$ elements. + One of Garey and Johnson's NP-complete problems (SP4 in @garey1979), shown NP-complete by #cite(, form: "prose") via reduction from Not-All-Equal 3-Satisfiability. It is equivalent to deciding whether a hypergraph is 2-colorable (also called Property B). The problem is trivially satisfiable when every subset has size exactly 2, reducing to 2-colorability of the corresponding graph; it becomes NP-complete for subsets of size $gt.eq 3$. The best known exact algorithm runs in $O^*(2^n)$ by brute-force enumeration over the $n = |U|$ elements. *Example.* Let $U = {1, 2, dots, #n}$ and $cal(C) = {C_1, dots, C_#m}$ with #range(m).map(i => $C_#(i + 1) = #fmt-set(subsets.at(i))$).join(", "). Coloring $S_1 = #fmt-set(part0)$ and $S_2 = #fmt-set(part1)$ splits all subsets: each $C_i$ has at least one element in each part. @@ -3499,6 +3736,39 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], "pred solve consecutive-sets.json", "pred evaluate consecutive-sets.json --config " + x.optimal_config.map(str).join(","), ) + + // Subset span data: (start_pos, end_pos) in the solution string + // Σ1={0,4} at 0–1, Σ2={2,4} at 1–2, Σ3={2,5} at 2–3, Σ4={1,5} at 3–4, Σ5={1,3} at 4–5 + #let spans = ((0, 1), (1, 2), (2, 3), (3, 4), (4, 5)) + #let span-colors = (rgb("#4e79a7"), rgb("#e15759"), rgb("#59a14f"), rgb("#f28e2b"), rgb("#b07aa1")) + + #figure( + canvas(length: 1cm, { + import draw: * + let cell = 1.0 + // String positions as boxes + for (pos, sym) in sol.enumerate() { + let x = pos * cell + rect((x - cell / 2, -0.3), (x + cell / 2, 0.3), stroke: 0.6pt + black) + content((x, 0), text(10pt, weight: "bold", str(sym))) + // Position label above + content((x, 0.55), text(7pt, fill: luma(120), str(pos))) + } + // Subset spans as colored brackets below + for (si, ((s, e), color)) in spans.zip(span-colors).enumerate() { + let y = -0.65 - si * 0.4 + let x0 = s * cell + let x1 = e * cell + line((x0, y), (x1, y), stroke: 1.5pt + color) + // Tick marks at endpoints + line((x0, y - 0.08), (x0, y + 0.08), stroke: 1.2pt + color) + line((x1, y - 0.08), (x1, y + 0.08), stroke: 1.2pt + color) + // Label + content((x1 + 0.45, y), text(7pt, fill: color, $Sigma_#(si + 1)$)) + } + }), + caption: [Consecutive Sets: the string $w = (#sol.map(str).join(", "))$ with each subset $Sigma_i$ occupying a contiguous block. Colored bars below indicate the span of each subset.] + ) ] ] } @@ -3528,6 +3798,43 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], "pred solve exact-cover-by-3-sets.json", "pred evaluate exact-cover-by-3-sets.json --config " + x3c.optimal_config.map(str).join(","), ) + + #figure( + canvas(length: 1cm, { + import draw: * + // Element nodes (top row, 1-indexed labels) + let elem-pos = range(n).map(i => ((i - (n - 1) / 2) * 0.9, 1.2)) + // Subset nodes (bottom row) + let sub-pos = range(m).map(j => ((j - (m - 1) / 2) * 1.3, -1.2)) + // Edges: element ∈ subset + for (j, subset) in subs.enumerate() { + let is-sel = selected.contains(j) + for i in subset { + line(elem-pos.at(i), sub-pos.at(j), + stroke: if is-sel { 1pt + graph-colors.at(0) } else { 0.5pt + luma(190) }) + } + } + // Element nodes + for (k, pos) in elem-pos.enumerate() { + // Find which selected subset covers this element + let covered-by = selected.filter(j => subs.at(j).contains(k)) + let covered = covered-by.len() > 0 + circle(pos, radius: 0.22, + fill: if covered { graph-colors.at(0) } else { white }, + stroke: 0.8pt + black) + content(pos, text(7pt, fill: if covered { white } else { black }, [#(k + 1)])) + } + // Subset nodes + for (j, pos) in sub-pos.enumerate() { + let is-sel = selected.contains(j) + circle(pos, radius: 0.26, + fill: if is-sel { graph-colors.at(0).lighten(70%) } else { luma(240) }, + stroke: if is-sel { 1pt + graph-colors.at(0) } else { 0.8pt + black }) + content(pos, text(7pt, $S_#(j + 1)$)) + } + }), + caption: [Exact Cover by 3-Sets: the selected cover $cal(C)' = {#selected.map(i => $S_#(i + 1)$).join(", ")}$ (blue) partitions the universe $X = {1, dots, #n}$ into $q = #q$ disjoint triples. Every element (top) is covered by exactly one selected subset (bottom).] + ) ] ] } @@ -3556,6 +3863,43 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], "pred solve three-dimensional-matching.json", "pred evaluate three-dimensional-matching.json --config " + tdm.optimal_config.map(str).join(","), ) + + // Tripartite layout: W (left), X (center), Y (right) with triples as hyperedges + #figure( + canvas(length: 1cm, { + import draw: * + let col-x = (-2.0, 0.0, 2.0) // W, X, Y column positions + let col-labels = ($W$, $X$, $Y$) + let spacing = 0.9 + // Node positions for each dimension + let node-pos(dim, idx) = (col-x.at(dim), (q - 1) / 2 * spacing - idx * spacing) + // Draw triples as colored lines connecting W, X, Y nodes + let triple-colors = (graph-colors.at(0), rgb("#e15759"), rgb("#59a14f"), luma(180), luma(180)) + for (ti, triple) in triples.enumerate() { + let is-sel = selected.contains(ti) + let color = if is-sel { triple-colors.at(ti) } else { luma(200) } + let sw = if is-sel { 1.2pt } else { 0.5pt } + // W→X, X→Y lines + line(node-pos(0, triple.at(0)), node-pos(1, triple.at(1)), stroke: sw + color) + line(node-pos(1, triple.at(1)), node-pos(2, triple.at(2)), stroke: sw + color) + } + // Nodes + for dim in range(3) { + for idx in range(q) { + let pos = node-pos(dim, idx) + // Check if this node is used by a selected triple in this dimension + let used = selected.any(ti => triples.at(ti).at(dim) == idx) + circle(pos, radius: 0.22, + fill: if used { graph-colors.at(0) } else { white }, + stroke: 0.8pt + black) + content(pos, text(8pt, fill: if used { white } else { black }, [#(idx + 1)])) + } + // Column label + content((col-x.at(dim), (q - 1) / 2 * spacing + 0.65), text(9pt, col-labels.at(dim))) + } + }), + caption: [Three-Dimensional Matching: tripartite layout with $W$, $X$, $Y$ columns. The matching $M' = {#selected.map(i => $t_#(i + 1)$).join(", ")}$ (colored paths) covers every element exactly once.] + ) ] ] } @@ -3588,6 +3932,39 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], "pred solve three-matroid-intersection.json", "pred evaluate three-matroid-intersection.json --config " + tmi.optimal_config.map(str).join(","), ) + + // Three rows of partition groups, elements shown in each + #figure( + canvas(length: 1cm, { + import draw: * + let matroid-labels = ($cal(F)_1$, $cal(F)_2$, $cal(F)_3$) + let row-y = (1.6, 0.0, -1.6) + let group-colors = (rgb("#4e79a7"), rgb("#e15759"), rgb("#59a14f")) + for (mi, partition) in parts.enumerate() { + let y = row-y.at(mi) + let total-groups = partition.len() + // Label + content((-3.2, y), text(9pt, matroid-labels.at(mi)), anchor: "east") + // Draw each group as a rounded rectangle with elements inside + for (gi, group) in partition.enumerate() { + let gx = (gi - (total-groups - 1) / 2) * 2.2 + let w = group.len() * 0.55 + 0.3 + rect((gx - w / 2, y - 0.35), (gx + w / 2, y + 0.35), + stroke: 0.8pt + group-colors.at(mi), radius: 4pt) + // Elements inside the group + for (ei, elem) in group.enumerate() { + let ex = gx + (ei - (group.len() - 1) / 2) * 0.5 + let is-sel = selected.contains(elem) + circle((ex, y), radius: 0.18, + fill: if is-sel { graph-colors.at(0) } else { white }, + stroke: 0.6pt + black) + content((ex, y), text(7pt, fill: if is-sel { white } else { black }, str(elem))) + } + } + } + }), + caption: [Three-Matroid Intersection: each row shows one partition matroid's groups (rounded boxes). The selected elements $E' = #fmt-set(selected)$ (blue) place at most one element per group in all three matroids.] + ) ] ] } @@ -3763,7 +4140,7 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], ][ A functional dependency $X arrow Y$ on attribute set $A$ means: whenever two database rows agree on every attribute in $X$, they must also agree on every attribute in $Y$. The _closure_ $X^+_F$ of a subset $X subset.eq A$ under a set $F$ of functional dependencies is the largest set of attributes determined by $X$: start with $X^+_F = X$, then repeatedly apply every rule $L arrow R in F$ for which $L subset.eq X^+_F$, adding $R$ to $X^+_F$, until no more attributes can be added. A _superkey_ is any $K subset.eq A$ with $K^+_F = A$ (knowing $K$ determines everything). A _candidate key_ is a minimal superkey — no proper subset of $K$ is itself a superkey. An attribute $x$ is _prime_ if it belongs to at least one candidate key. - Determining whether an attribute is prime is NP-complete (Lucchesi and Osborn, 1978; Garey & Johnson SR28). The brute-force approach enumerates all $2^n$ subsets of $A$ containing $x$ and checks each for the key property; no algorithm significantly improving on this is known for the general problem. + Determining whether an attribute is prime is NP-complete @lucchesi1978keys (Garey & Johnson SR28 @garey1979). The brute-force approach enumerates all $2^n$ subsets of $A$ containing $x$ and checks each for the key property; no algorithm significantly improving on this is known for the general problem. *Example.* Let $A = {0, 1, ..., #(n - 1)}$ ($n = #n$), query attribute $x = #q$, and $F = {#deps.enumerate().map(((i, d)) => $#fmt-set-math(d.at(0)) arrow #fmt-set-math(d.at(1))$).join(", ")}$. @@ -3850,6 +4227,47 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], "pred solve minimum-cardinality-key.json", "pred evaluate minimum-cardinality-key.json --config " + x.optimal_config.map(str).join(","), ) + + #figure( + canvas(length: 1cm, { + import draw: * + // Attribute nodes in a single row + let spacing = 1.0 + let attr-pos = range(n).map(i => (i * spacing, 0)) + // FD colors + let fd-colors = (rgb("#e15759"), rgb("#59a14f"), rgb("#b07aa1"), rgb("#f28e2b"), rgb("#76b7b2")) + // Junction y-levels for each FD + let fd-y = range(m).map(i => -1.0 - i * 0.9) + // Draw FDs: LHS → junction dot → arrows to RHS + for (fi, (lhs, rhs)) in deps.enumerate() { + let color = fd-colors.at(calc.rem(fi, fd-colors.len())) + let y = fd-y.at(fi) + let jx = lhs.map(a => attr-pos.at(a).at(0)).sum() / lhs.len() + let junc = (jx, y) + for a in lhs { + line(attr-pos.at(a), junc, stroke: 0.8pt + color) + } + for a in rhs { + line(junc, attr-pos.at(a), stroke: 0.8pt + color, mark: (end: "straight")) + } + circle(junc, radius: 0.08, fill: color, stroke: none) + on-layer(1, { + content((jx - 0.5, y), + text(6.5pt, fill: color)[FD#(fi + 1)], + anchor: "east") + }) + } + // Attribute nodes (drawn on top layer) + for (k, pos) in attr-pos.enumerate() { + let is-key = key-attrs.contains(k) + circle(pos, radius: 0.22, + fill: if is-key { graph-colors.at(0) } else { white }, + stroke: 0.8pt + black) + content(pos, text(8pt, fill: if is-key { white } else { black }, [$#k$])) + } + }), + caption: [Minimum Cardinality Key: optimal key $K = #fmt-set(key-attrs)$ shown in blue. Each FD is drawn as lines converging to a dot (LHS) with arrows fanning out to RHS attributes. Chaining all FDs from $K$ reaches every attribute in $A$.] + ) ] ] } @@ -4137,8 +4555,8 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], $ min quad & bold(c)^top bold(x) \ "subject to" quad & A bold(x) <= bold(b) \ - & bold(x) in cal(D)^n - $. + & bold(x) in cal(D)^n. + $ ][ Integer Linear Programming is a universal modeling framework: virtually every NP-hard combinatorial optimization problem admits an ILP formulation. Relaxing integrality to $bold(x) in RR^n$ yields a linear program solvable in polynomial time, forming the basis of branch-and-bound solvers. When the number of integer variables $n$ is fixed, ILP is solvable in polynomial time by Lenstra's algorithm @lenstra1983 using the geometry of numbers, making it fixed-parameter tractable in $n$. The best known general algorithm achieves $O^*(n^n)$ via an FPT algorithm based on lattice techniques @dadush2012. @@ -10317,8 +10735,8 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead max quad & sum_(j=0)^(m-1) z_j \ "subject to" quad & z_j <= ell_1' + ell_2' quad forall j in {0, dots, m - 1} \ & y_i in {0, 1} quad forall i in {0, dots, n - 1} \ - & z_j in {0, 1} quad forall j in {0, dots, m - 1} - $. + & z_j in {0, 1} quad forall j in {0, dots, m - 1}. + $ The target has $n + m$ variables and $m$ constraints. _Correctness._ ($arrow.r.double$) Any truth assignment $bold(y)$ satisfying $k$ clauses yields a feasible ILP solution by setting $z_j = 1$ iff clause $j$ is satisfied, achieving objective $k$. ($arrow.l.double$) Any feasible ILP solution with $z_j = 1$ has clause $j$ satisfied by the constraint, so the truth assignment satisfies at least $sum z_j$ clauses. Thus optimal values coincide. @@ -10365,8 +10783,8 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead & z_(t,v,x,x') <= y_(v,b,x') quad forall t in cal(T), v in V, (x, x') in D_a times D_b \ & z_(t,v,x,x') >= y_(v,a,x) + y_(v,b,x') - 1 quad forall t in cal(T), v in V, (x, x') in D_a times D_b \ & sum_(v in V) z_(t,v,x,x') = f_t(x, x') quad forall t in cal(T), (x, x') in D_a times D_b \ - & y_(v,a,x), z_(t,v,x,x') in {0, 1} - $. + & y_(v,a,x), z_(t,v,x,x') in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A consistent assignment defines one-hot indicators and their products; all constraints hold by construction, and the frequency equalities match the published counts. ($arrow.l.double$) Any feasible binary solution assigns exactly one value per object-attribute (one-hot), respects known values, and the McCormick constraints force $z_(t,v,x,x') = y_(v,a,x) dot y_(v,b,x')$ for binary variables, so the frequency equalities certify consistency. @@ -11482,8 +11900,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m "subject to" quad & y_(i j) <= x_i quad forall i < j, Q_(i j) != 0 \ & y_(i j) <= x_j quad forall i < j, Q_(i j) != 0 \ & y_(i j) >= x_i + x_j - 1 quad forall i < j, Q_(i j) != 0 \ - & x_i, y_(i j) in {0, 1} - $. + & x_i, y_(i j) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) For binary $x_i, x_j$, the three McCormick inequalities are tight: $y_(i j) = x_i x_j$ is the unique feasible value. Hence the ILP objective equals $bold(x)^top Q bold(x)$, and any ILP minimizer is a QUBO minimizer. ($arrow.l.double$) Given a QUBO minimizer $bold(x)^*$, setting $y_(i j) = x_i^* x_j^*$ satisfies all constraints and achieves the same objective value. @@ -11531,8 +11949,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m & c >= a - b quad "for each XOR gate" \ & c >= b - a quad "for each XOR gate" \ & c <= 2 - a - b quad "for each XOR gate" \ - & "all gate and input variables are binary" - $. + & "all gate and input variables are binary". + $ _Correctness._ ($arrow.r.double$) Each gate encoding is the convex hull of the gate's truth table rows (viewed as binary vectors), so a satisfying circuit assignment satisfies all constraints. ($arrow.l.double$) Any binary feasible solution respects every gate's input-output relation, and since gates are composed in topological order, the full circuit evaluates to true. @@ -12002,8 +12420,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m "find" quad & bold(x) \ "subject to" quad & sum_(c=1)^k x_(v,c) = 1 quad forall v in V \ & x_(u,c) + x_(v,c) <= 1 quad forall (u, v) in E, c in {1, dots, k} \ - & x_(v,c) in {0, 1} - $. + & x_(v,c) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A valid $k$-coloring assigns exactly one color per vertex with different colors on adjacent vertices; setting $x_(v,c) = 1$ for the assigned color satisfies all constraints. ($arrow.l.double$) Any feasible ILP solution has exactly one $x_(v,c) = 1$ per vertex; this defines a coloring, and constraint (2) ensures adjacent vertices differ. @@ -12044,8 +12462,8 @@ where $P$ is a penalty weight large enough that any constraint violation costs m & z_(i j) >= p_i + q_j - 1 quad forall i, j \ & sum_(i+j=k) z_(i j) + c_(k-1) = N_k + 2 c_k quad forall k in {0, dots, m + n - 1} \ & c_(m+n-1) = 0 \ - & p_i, q_j, z_(i j) in {0, 1}, c_k in ZZ_(>=0) - $. + & p_i, q_j, z_(i j) in {0, 1}, c_k in ZZ_(>=0). + $ _Correctness._ The McCormick constraints enforce $z_(i j) = p_i dot q_j$ for binary variables. The bit equations encode $p times q = N$ via carry propagation, matching array multiplier semantics. @@ -12063,8 +12481,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ max quad & sum_i w_i x_i \ "subject to" quad & sum_(S_i in.rev e) x_i <= 1 quad forall e in U \ - & x_i in {0, 1} quad forall i - $. + & x_i in {0, 1} quad forall i. + $ _Correctness._ ($arrow.r.double$) A valid packing chooses pairwise disjoint sets, so each element is covered at most once. ($arrow.l.double$) Any feasible binary solution covers each element at most once, hence the chosen sets are pairwise disjoint; the objective maximizes total weight. @@ -12078,8 +12496,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ max quad & sum_e w_e x_e \ "subject to" quad & sum_(e in.rev v) x_e <= 1 quad forall v in V \ - & x_e in {0, 1} quad forall e in E - $. + & x_e in {0, 1} quad forall e in E. + $ _Correctness._ ($arrow.r.double$) A matching has at most one edge per vertex, so all degree constraints hold. ($arrow.l.double$) Any feasible solution is a matching by construction; the objective maximizes total weight. @@ -12093,8 +12511,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ min quad & sum_i w_i x_i \ "subject to" quad & sum_(S_i in.rev u) x_i >= 1 quad forall u in U \ - & x_i in {0, 1} quad forall i - $. + & x_i in {0, 1} quad forall i. + $ _Correctness._ ($arrow.r.double$) A set cover includes at least one set containing each element, satisfying all constraints. ($arrow.l.double$) Any feasible solution covers every element; the objective minimizes total weight. @@ -12108,8 +12526,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ min quad & sum_v w_v x_v \ "subject to" quad & x_v + sum_(u in N(v)) x_u >= 1 quad forall v in V \ - & x_v in {0, 1} quad forall v in V - $. + & x_v in {0, 1} quad forall v in V. + $ _Correctness._ ($arrow.r.double$) A dominating set includes a vertex or one of its neighbors for every vertex, satisfying all constraints. ($arrow.l.double$) Any feasible solution dominates every vertex; the objective minimizes total weight. @@ -12182,8 +12600,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ min quad & sum_v w_v x_v \ "subject to" quad & o_v - o_u >= 1 - n (x_u + x_v) quad forall (u -> v) in A \ - & x_v in {0, 1}, o_v in {0, dots, n - 1} quad forall v in V - $. + & x_v in {0, 1}, o_v in {0, dots, n - 1} quad forall v in V. + $ _Correctness._ ($arrow.r.double$) If $S$ is a feedback vertex set, then $G[V backslash S]$ is a DAG with a topological ordering. Set $x_v = 1$ for $v in S$, $o_v$ to the topological position for kept vertices, and $o_v = 0$ for removed vertices. All constraints are satisfied. ($arrow.l.double$) If the ILP is feasible with all arc constraints satisfied, no directed cycle can exist among kept vertices: a cycle $v_1 -> dots -> v_k -> v_1$ would require $o_(v_1) < o_(v_2) < dots < o_(v_k) < o_(v_1)$, a contradiction. @@ -12227,8 +12645,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ max quad & sum_v x_v \ "subject to" quad & x_u + x_v <= 1 quad forall (u, v) in.not E \ - & x_v in {0, 1} quad forall v in V - $. + & x_v in {0, 1} quad forall v in V. + $ _Correctness._ ($arrow.r.double$) In a clique, every pair of selected vertices is adjacent, so no non-edge constraint is violated. ($arrow.l.double$) Any feasible solution selects only mutually adjacent vertices, forming a clique; the objective maximizes its size. @@ -12258,7 +12676,7 @@ The following reductions to Integer Linear Programming are straightforward formu The objective is $ max #ks_ilp.source.instance.values.enumerate().map(((i, v)) => $#v x_#i$).join($+$) $ subject to the single capacity inequality - $ #ks_ilp.source.instance.weights.enumerate().map(((i, w)) => $#w x_#i$).join($+$) <= #ks_ilp.source.instance.capacity $. + $ #ks_ilp.source.instance.weights.enumerate().map(((i, w)) => $#w x_#i$).join($+$) <= #ks_ilp.source.instance.capacity. $ *Step 3 -- Verify a solution.* The ILP optimum $bold(x)^* = (#ks_ilp_sol.target_config.map(str).join(", "))$ extracts directly to the knapsack selection $bold(x)^* = (#ks_ilp_sol.source_config.map(str).join(", "))$, choosing items $\{#ks_ilp_selected.map(str).join(", ")\}$. Their total weight is $#ks_ilp_selected.map(i => str(ks_ilp.source.instance.weights.at(i))).join(" + ") = #ks_ilp_sel_weight$ and their total value is $#ks_ilp_selected.map(i => str(ks_ilp.source.instance.values.at(i))).join(" + ") = #ks_ilp_sel_value$ #sym.checkmark. @@ -12271,8 +12689,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ max quad & sum_(i=0)^(n-1) v_i x_i \ "subject to" quad & sum_(i=0)^(n-1) w_i x_i <= C \ - & x_i in {0, 1} quad forall i in {0, dots, n - 1} - $. + & x_i in {0, 1} quad forall i in {0, dots, n - 1}. + $ The target therefore has exactly $n$ variables and one linear constraint. _Correctness._ ($arrow.r.double$) Any feasible knapsack solution $bold(x)$ satisfies $sum_i w_i x_i <= C$, so the same binary vector is feasible for the ILP and attains identical objective value $sum_i v_i x_i$. ($arrow.l.double$) Any feasible binary ILP solution selects exactly the items with $x_i = 1$; the single inequality guarantees the chosen set fits in the knapsack, and the ILP objective equals the knapsack value. Therefore optimal solutions correspond one-to-one and preserve the optimum value. @@ -12307,7 +12725,7 @@ The following reductions to Integer Linear Programming are straightforward formu *Step 2 -- Build the ILP.* Introduce one integer variable per item multiplicity: $#range(sizes.len()).map(i => $c_#i$).join(", ") in NN$. The capacity constraint is - $ #sizes.enumerate().map(((i, s)) => $#s c_#i$).join($+$) <= #B $, + $ #sizes.enumerate().map(((i, s)) => $#s c_#i$).join($+$) <= #B, $ and the explicit upper bounds are $(#upper.map(str).join(", "))$, i.e. $c_i <= floor.l B / s_i floor.r$ for every item. *Step 3 -- Verify the canonical witness.* The ILP optimum is $(#ik_ilp_sol.target_config.map(str).join(", "))$, which extracts identically to the source multiplicities $(#ik_ilp_sol.source_config.map(str).join(", "))$. The selected terms contribute total size $#total_size <= B$ and total value $#total_value$ #sym.checkmark. @@ -12376,8 +12794,8 @@ The following reductions to Integer Linear Programming are straightforward formu min quad & sum_(j=0)^(n-1) y_j \ "subject to" quad & sum_(j=0)^(n-1) x_(i j) = 1 quad forall i in {0, dots, n - 1} \ & sum_(i=0)^(n-1) s_i x_(i j) <= C y_j quad forall j in {0, dots, n - 1} \ - & x_(i j), y_j in {0, 1} - $. + & x_(i j), y_j in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A valid packing assigns each item to exactly one bin (satisfying (1)); each bin's load is at most $C$ and $y_j = 1$ for any used bin (satisfying (2)). ($arrow.l.double$) Any feasible solution assigns each item to one bin by (1), respects capacity by (2), and the objective counts the number of open bins. @@ -12406,8 +12824,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(a_i in I_j) x_i <= c_j quad forall j in {1, dots, k} \ & sum_(a_i = (u, v) in A) x_i - sum_(a_i = (v, w) in A) x_i = 0 quad forall v in V backslash {s, t} \ & sum_(a_i = (u, t) in A) x_i - sum_(a_i = (t, w) in A) x_i >= R \ - & x_i in ZZ_(>=0) quad forall i in {0, dots, m - 1} - $. + & x_i in ZZ_(>=0) quad forall i in {0, dots, m - 1}. + $ _Correctness._ ($arrow.r.double$) Any satisfying bundled flow assigns a non-negative integer to each arc, satisfies every bundle inequality by definition, satisfies every nonterminal conservation equality, and yields sink inflow at least $R$, so it is a feasible ILP solution. ($arrow.l.double$) Any feasible ILP solution gives non-negative integral arc values obeying the same bundle, conservation, and sink-inflow constraints, hence it is a satisfying solution to the original Integral Flow with Bundles instance. @@ -12438,8 +12856,8 @@ The following reductions to Integer Linear Programming are straightforward formu & C_j - C_i >= l_j quad forall i prec.eq j \ & C_j - C_i + M (1 - y_(i j)) >= l_j quad forall i < j \ & C_i - C_j + M y_(i j) >= l_i quad forall i < j \ - & y_(i j) in {0, 1}, C_j in ZZ_(>=0) - $. + & y_(i j) in {0, 1}, C_j in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any feasible schedule defines completion times and pairwise order values satisfying the bounds, precedence inequalities, and disjunctive machine constraints; its weighted completion time is exactly the ILP objective. ($arrow.l.double$) Any feasible ILP solution assigns a strict order to every task pair and forbids overlap, so the completion times correspond to a valid single-machine schedule that respects all precedences. Minimizing the ILP objective therefore minimizes the original weighted completion-time objective. @@ -12519,8 +12937,8 @@ The following reductions to Integer Linear Programming are straightforward formu & y_(u,v,k) <= x_(u,k) quad forall (u, v) in E, k in {0, dots, n - 1} \ & y_(u,v,k) <= x_(v,(k+1) mod n) quad forall (u, v) in E, k in {0, dots, n - 1} \ & y_(u,v,k) >= x_(u,k) + x_(v,(k+1) mod n) - 1 quad forall (u, v) in E, k in {0, dots, n - 1} \ - & x_(v,k), y_(u,v,k) in {0, 1} - $. + & x_(v,k), y_(u,v,k) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A valid tour defines a permutation matrix $(x_(v,k))$ satisfying constraints (1)--(2); consecutive vertices are adjacent by construction, so (3) holds; McCormick constraints (4) force $y = x_(u,k) x_(v,k+1)$, making the objective equal to the tour cost. ($arrow.l.double$) Any feasible binary solution defines a permutation (by (1)--(2)) where consecutive positions are connected by edges (by (3)), forming a Hamiltonian tour; the linearized objective equals the tour cost. @@ -12568,8 +12986,8 @@ The following reductions to Integer Linear Programming are straightforward formu & x_(u,v) + x_(v,u) <= 1 quad forall {u, v} in E \ & o_v - o_u >= 1 - n (1 - x_(u,v)) quad forall u -> v \ & o_s = 0 \ - & x_(u,v) in {0, 1}, o_v in {0, dots, n - 1} - $, + & x_(u,v) in {0, 1}, o_v in {0, dots, n - 1}, + $ where $b_s = 1$, $b_t = -1$, and $b_v = 0$ otherwise. _Correctness._ ($arrow.r.double$) Any simple $s$-$t$ path can be oriented from $s$ to $t$, giving exactly one outgoing arc at $s$, one incoming arc at $t$, balanced flow at every internal vertex, and strictly increasing order values along the path. ($arrow.l.double$) Any feasible ILP solution satisfies the flow equations and degree bounds, so the selected arcs form vertex-disjoint directed paths and cycles. The ordering inequalities make every selected arc increase the order value by at least 1, so directed cycles are impossible. The only remaining positive-flow component is therefore a single directed $s$-$t$ path, whose objective is exactly the total selected edge length. @@ -12661,8 +13079,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_(j = 1)^(|r_i|) y_(i, p, j) + x_(p, bot) = 1 quad forall i, p \ & y_(i, p, j) <= x_(p, r_i [j]) quad forall i, p, j \ & y_(i, p, j') + y_(i, p + 1, j) <= 1 quad forall i, p, j' >= j \ - & x_(p, a), y_(i, p, j) in {0, 1} - $. + & x_(p, a), y_(i, p, j) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Given an optimal common subsequence $w$ of length $ell$, set $x_(p, w_p) = 1$ for $p lt.eq ell$ and $x_(p, bot) = 1$ for $p > ell$. For active positions, choose the embedding indices in each source string. All constraints are satisfied and the objective equals $ell$. ($arrow.l.double$) Any optimal ILP solution selects contiguous non-padding positions followed by padding. The active prefix, together with character consistency and ordering constraints, forms a valid common subsequence whose length equals the objective value. @@ -12688,8 +13106,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_(i=0)^(k-1) y_(i v) = 1 quad forall v in V \ & x_e >= y_(i u) - y_(i v) quad forall e = (u, v) in E, i in {0, dots, k - 1} \ & x_e >= y_(i v) - y_(i u) quad forall e = (u, v) in E, i in {0, dots, k - 1} \ - & x_e, y_(i v) in {0, 1} - $. + & x_e, y_(i v) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A multiway cut $C$ partitions $V$ into $k$ components, one per terminal. Setting $y_(i v) = 1$ iff $v$ is in $t_i$'s component and $x_e = 1$ iff $e in C$ satisfies all constraints: partition by construction, terminal fixing by definition, and linking because any edge with endpoints in different components is in $C$. The objective equals the cut weight. ($arrow.l.double$) Any feasible ILP solution defines a valid partition (by constraint (2)) separating all terminals (by constraint (1)). The linking constraints (3) force $x_e = 1$ for all cross-component edges, so the objective is at least the multiway cut weight; minimization ensures optimality. @@ -12746,8 +13164,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(u : (u, v) in A) f^t_(u,v) - sum_(u : (v, u) in A) f^t_(v,u) = b_(t,v) quad forall t in T backslash {r}, v in V \ & f^t_(u,v) <= y_e quad forall t in T backslash {r}, e = {u, v} in E \ & f^t_(v,u) <= y_e quad forall t in T backslash {r}, e = {u, v} in E \ - & y_e, f^t_(u,v) in {0, 1} - $. + & y_e, f^t_(u,v) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) If $S subset.eq E$ is a Steiner tree, set $y_e = 1$ exactly for $e in S$. For each non-root terminal $t$, the unique path from $r$ to $t$ inside the tree defines a binary flow assignment satisfying the conservation equations, and every used arc lies on a selected edge, so all linking inequalities hold. The ILP objective equals $sum_(e in S) w_e$. ($arrow.l.double$) Any feasible ILP solution with edge selector set $Y = {e in E : y_e = 1}$ supports one unit of flow from $r$ to every non-root terminal, so the selected edges contain a connected subgraph spanning all terminals. Because all edge weights are strictly positive, any cycle in the selected subgraph has positive total cost; the optimizer therefore never includes redundant edges, so the selected subgraph is already a Steiner tree. Therefore an optimal ILP solution induces a minimum-cost Steiner tree. @@ -12799,8 +13217,8 @@ The following reductions to Integer Linear Programming are straightforward formu $ min quad & sum_e x_e \ "subject to" quad & sum_(e in S) x_e >= 1 quad forall S in cal(S) \ - & x_e in {0, 1} quad forall e in U - $. + & x_e in {0, 1} quad forall e in U. + $ _Correctness._ ($arrow.r.double$) A hitting set includes at least one element from each set. ($arrow.l.double$) Any feasible solution hits every set. @@ -12815,8 +13233,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_(j : e in T_j) x_j = 1 quad forall e in U \ & sum_j x_j = |U| / 3 \ - & x_j in {0, 1} quad forall j - $. + & x_j in {0, 1} quad forall j. + $ _Correctness._ The equality constraints force each element to appear in exactly one selected triple, which is the definition of an exact cover. @@ -12831,8 +13249,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_i "coeff"_(C,i) x_i >= 1 - "neg"(C) quad "for each clause" C \ & sum_i "coeff"_(C,i) x_i <= |C| - 1 - "neg"(C) quad "for each clause" C \ - & x_i in {0, 1} quad forall i - $. + & x_i in {0, 1} quad forall i. + $ _Correctness._ The two constraints per clause jointly enforce the not-all-equal condition. @@ -12847,8 +13265,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_(j in C) x_j >= 1 quad "for each" C in cal(C) \ & sum_(j in C) x_j <= |C| - 1 quad "for each" C in cal(C) \ - & x_i in {0, 1} quad forall i - $. + & x_i in {0, 1} quad forall i. + $ _Correctness._ ($arrow.r.double$) A valid splitting has at least one element in $S_2$ ($sum >= 1$) and at least one in $S_1$ ($sum <= |C|-1$) for every $C$. ($arrow.l.double$) Any feasible ILP solution defines a valid 2-coloring. @@ -12948,8 +13366,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_v x_v >= k \ & x_u + x_v <= 1 quad forall (u, v) in.not E \ - & x_v in {0, 1} quad forall v in V - $. + & x_v in {0, 1} quad forall v in V. + $ _Correctness._ ($arrow.r.double$) A $k$-clique selects $>= k$ mutually adjacent vertices, satisfying all constraints. ($arrow.l.double$) Any feasible solution selects $>= k$ vertices with no non-edge pair, forming a clique of size $>= k$. @@ -13012,8 +13430,8 @@ The following reductions to Integer Linear Programming are straightforward formu max quad & sum_v w_v x_v \ "subject to" quad & x_u + x_v <= 1 quad forall (u, v) in E \ & x_v + sum_(u in N(v)) x_u >= 1 quad forall v in V \ - & x_v in {0, 1} quad forall v in V - $. + & x_v in {0, 1} quad forall v in V. + $ _Correctness._ Independence constraints prevent adjacent selections; maximality constraints ensure every vertex is either selected or has a selected neighbor. @@ -13028,8 +13446,8 @@ The following reductions to Integer Linear Programming are straightforward formu min quad & sum_e x_e \ "subject to" quad & sum_(e in.rev v) x_e <= 1 quad forall v in V \ & x_j + sum_(i : i ~ j,\ i eq.not j) x_i >= 1 quad forall j in E \ - & x_e in {0, 1} quad forall e in E - $, + & x_e in {0, 1} quad forall e in E, + $ where $i ~ j$ denotes that edges $i$ and $j$ share an endpoint. _Correctness._ Degree constraints enforce the matching property. For each edge $j$, the maximality constraint requires that $j$ itself or at least one adjacent edge is selected, ensuring the matching cannot be extended. ($arrow.r.double$) A minimum maximal matching satisfies both constraints and minimizes cardinality. ($arrow.l.double$) Any feasible solution is a maximal matching; the objective minimizes its size. @@ -13049,8 +13467,8 @@ The following reductions to Integer Linear Programming are straightforward formu & y_({u,v},k) <= x_(v,k) quad forall {u,v} in E,\ forall k \ & y_({u,v},k) >= x_(u,k) + x_(v,k) - 1 quad forall {u,v} in E,\ forall k \ & sum_(k=0)^(m-1) y_(e,k) >= 1 quad forall e in E \ - & x_(v,k), z_k, y_(e,k) in {0, 1} - $. + & x_(v,k), z_k, y_(e,k) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Given an edge-clique cover $C_0, dots, C_(t-1)$ with $t <= m$, map clique $C_k$ to slot $k$: set $z_k = 1$, set $x_(v,k) = 1$ exactly for $v in C_k$, and set $y_(e,k) = 1$ exactly for the edges $e$ whose endpoints both lie in $C_k$. Because each $C_k$ is a clique, no non-edge constraint is violated. Every covered edge satisfies at least one coverage inequality, so the ILP objective is at most $t$. @@ -13067,8 +13485,8 @@ The following reductions to Integer Linear Programming are straightforward formu max quad & sum_i v_i x_i \ "subject to" quad & sum_i w_i x_i <= C \ & x_b <= x_a quad "for each precedence" (a, b) \ - & x_i in {0, 1} quad forall i - $. + & x_i in {0, 1} quad forall i. + $ _Correctness._ Capacity and precedence constraints are directly linear. Any feasible ILP solution is a valid knapsack packing respecting the partial order. @@ -13083,8 +13501,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_(r "covers" (i,j)) x_r >= 1 quad forall (i, j) "with source cell" = 1 \ & sum_r x_r <= B \ - & x_r in {0, 1} quad forall r - $. + & x_r in {0, 1} quad forall r. + $ _Correctness._ Coverage constraints ensure every 1-cell is covered; the cardinality bound limits the number of rectangles. @@ -13103,8 +13521,8 @@ The following reductions to Integer Linear Programming are straightforward formu & a_(u,v) + a_(v,u) <= 1 quad forall {u, v} in E \ & o_v - o_u >= 1 - M (1 - a_(u,v)) quad forall (u, v) in A \ & sum_((u,v) in A) w_(u,v) a_(u,v) <= W \ - & a_(u,v) in {0, 1}, o_v in {0, dots, n - 1} - $, + & a_(u,v) in {0, 1}, o_v in {0, dots, n - 1}, + $ where $b_s = 1$, $b_t = -1$, and $b_v = 0$ otherwise. _Correctness._ Flow balance forces an $s$-$t$ path; the MTZ inequalities apply only on selected arcs and therefore eliminate subtours; the weight constraint enforces the budget; the objective minimizes total path length. @@ -13120,8 +13538,8 @@ The following reductions to Integer Linear Programming are straightforward formu "minimize" quad & sum_v s_v x_v + sum_(v,u) "usage"_v d(v, u) y_(v,u) \ "subject to" quad & sum_u y_(v,u) = 1 quad forall v \ & y_(v,u) <= x_u quad forall v, u \ - & x_v, y_(v,u) in {0, 1} - $. + & x_v, y_(v,u) in {0, 1}. + $ _Correctness._ Assignment constraints ensure each vertex is served by exactly one copy; capacity links prevent assignment to non-copy vertices; the objective linearizes the total cost. @@ -13137,8 +13555,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_j x_j = k \ & y_(i,j) <= x_j quad forall i, j \ & sum_j y_(i,j) = 1 quad forall i \ - & x_j, y_(i,j) in {0, 1} - $. + & x_j, y_(i,j) in {0, 1}. + $ _Correctness._ The assignment structure and cardinality constraint directly encode the $k$-median objective with precomputed shortest-path distances. @@ -13155,8 +13573,8 @@ The following reductions to Integer Linear Programming are straightforward formu & y_(i,j) <= x_j quad forall i, j \ & sum_j y_(i,j) = 1 quad forall i \ & sum_j w_i d(i, j) y_(i,j) <= z quad forall i \ - & x_j, y_(i,j) in {0, 1}, z in bb(Z) - $. + & x_j, y_(i,j) in {0, 1}, z in bb(Z). + $ _Correctness._ Each minimax constraint forces $z$ to be at least the weighted distance from vertex $i$ to its assigned center. Minimizing $z$ yields the optimal maximum weighted distance. @@ -13171,8 +13589,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_p x_(j,p) = 1 quad forall j \ & sum_j l_j x_(j,p) <= D quad forall p \ - & x_(j,p) in {0, 1} - $. + & x_(j,p) in {0, 1}. + $ _Correctness._ One-hot constraints ensure each task is assigned to exactly one processor; load constraints enforce the deadline on every processor. @@ -13187,8 +13605,8 @@ The following reductions to Integer Linear Programming are straightforward formu "minimize" quad & sum_(l,c) "cost"[l][c] x_(l,c) \ "subject to" quad & sum_c x_(l,c) = 1 quad forall l \ & sum_(l,c) "delay"[l][c] x_(l,c) <= J \ - & x_(l,c) in {0, 1} - $. + & x_(l,c) in {0, 1}. + $ _Correctness._ One-hot constraints fix one capacity per link; the delay budget constraint is linear in the indicators; the objective sums the selected costs. @@ -13205,8 +13623,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((r,s),(r',s')) <= x_(r,s) quad forall r, s, r', s' \ & z_((r,s),(r',s')) <= x_(r',s') quad forall r, s, r', s' \ & z_((r,s),(r',s')) >= x_(r,s) + x_(r',s') - 1 quad forall r, s, r', s' \ - & x_(r,s), z_((r,s),(r',s')) in {0, 1} - $. + & x_(r,s), z_((r,s),(r',s')) in {0, 1}. + $ _Correctness._ McCormick constraints force $z$ to equal the product of binary indicators, linearizing the quadratic cost. The ILP objective directly encodes the expected retrieval cost. @@ -13222,8 +13640,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_g x_(v,g) = 1 quad forall v \ & sum_v x_(v,g) = 3 quad forall g in {1, dots, q} \ & x_(u,g) + x_(v,g) <= 1 quad forall g in {1, dots, q}, (u, v) in.not E \ - & x_(v,g) in {0, 1} - $. + & x_(v,g) in {0, 1}. + $ _Correctness._ Size-3 groups with no non-edge pair within any group forces each group to be a triangle. @@ -13242,8 +13660,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((u,v),g) <= x_(u,g) quad forall (u, v) in E, g \ & z_((u,v),g) <= x_(v,g) quad forall (u, v) in E, g \ & z_((u,v),g) >= x_(u,g) + x_(v,g) - 1 quad forall (u, v) in E, g \ - & x_(v,g), z_((u,v),g) in {0, 1} - $. + & x_(v,g), z_((u,v),g) in {0, 1}. + $ _Correctness._ The edge count constraint ensures connectivity within each group. Combined with group size 3, this forces a path of length 2. @@ -13290,8 +13708,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((i,j),g) <= x_(i,g) quad forall i, j, g \ & z_((i,j),g) <= x_(j,g) quad forall i, j, g \ & z_((i,j),g) >= x_(i,g) + x_(j,g) - 1 quad forall i, j, g \ - & x_(i,g), z_((i,j),g) in {0, 1} - $. + & x_(i,g), z_((i,j),g) in {0, 1}. + $ _Correctness._ Product linearization captures the quadratic sum-of-squares objective; the ILP minimizes the linearized form directly. @@ -13307,8 +13725,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_t x_(j,t) = 1 quad forall j \ & sum_j x_(j,t) <= m quad forall t \ & sum_t t x_(j,t) >= sum_t t x_(i,t) + 1 quad "for each precedence" (i, j) \ - & x_(j,t) in {0, 1} - $. + & x_(j,t) in {0, 1}. + $ _Correctness._ One-hot ensures each task is scheduled once; capacity limits processors per slot; precedence is linearized via weighted time indicators. @@ -13324,8 +13742,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(t = 0)^(d_j - 1) x_(j,t) = 1 quad forall j \ & sum_j x_(j,t) <= m quad forall t \ & sum_t t x_(j,t) >= sum_t t x_(i,t) + 1 quad "for each precedence" (i, j) \ - & x_(j,t) in {0, 1} - $. + & x_(j,t) in {0, 1}. + $ _Correctness._ Per-task deadline is enforced by restricting the time domain of each task's indicator variables. @@ -13342,8 +13760,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_t x_(t,u) <= m quad forall u quad "(capacity)" \ & sum_u u dot x_(j,u) - sum_u u dot x_(i,u) >= 1 quad "for each" (i prec j) quad "(precedence)" \ & M - (u+1) dot x_(t,u) >= 0 quad forall t, u quad "(makespan)" \ - & x_(t,u) in {0, 1}, quad M in ZZ_(>= 0) - $. + & x_(t,u) in {0, 1}, quad M in ZZ_(>= 0). + $ _Correctness._ Work constraints enforce each task runs for exactly $ell(t)$ slots. Capacity limits at most $m$ tasks per slot. Precedences are enforced by weighted time indicators. Makespan lower bounds force $M >= u+1$ whenever task $t$ is active at slot $u$. @@ -13358,8 +13776,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_(t = r_j)^(d_j - l_j) x_(j,t) = 1 quad forall j \ & sum_(j, t : t <= tau < t + l_j) x_(j,t) <= 1 quad forall tau \ - & x_(j,t) in {0, 1} - $. + & x_(j,t) in {0, 1}. + $ _Correctness._ One-hot ensures each task starts once within its feasible window; non-overlap prevents simultaneous execution. @@ -13374,8 +13792,8 @@ The following reductions to Integer Linear Programming are straightforward formu min quad & sum_a w_a y_a \ "subject to" quad & o_v - o_u >= 1 - n y_a quad forall a = (u -> v) \ & y_a in {0, 1} quad forall a \ - & o_v in {0, dots, n - 1} quad forall v - $. + & o_v in {0, dots, n - 1} quad forall v. + $ _Correctness._ ($arrow.r.double$) Removing a FAS leaves a DAG with a topological ordering satisfying all constraints. ($arrow.l.double$) Among kept arcs, the ordering variables enforce acyclicity: a cycle would require $o_(v_1) < dots < o_(v_k) < o_(v_1)$, a contradiction. @@ -13392,8 +13810,8 @@ The following reductions to Integer Linear Programming are straightforward formu & f^k_(v,u) <= "cap"_e (1 - d^k_e) quad forall e = {u, v} in E, k in {1, 2} \ & sum_(k=1)^2 (f^k_(u,v) + f^k_(v,u)) <= "cap"_e quad forall e = {u, v} in E \ & sum_(w) f^k_(v,w) - sum_(u) f^k_(u,v) = b^k_v quad forall k in {1, 2}, v in V \ - & d^k_e in {0, 1}, f^k_(u,v) in ZZ_(>=0) - $. + & d^k_e in {0, 1}, f^k_(u,v) in ZZ_(>=0). + $ _Correctness._ Direction indicators linearize the capacity-sharing constraint; flow conservation and demand constraints ensure valid multi-commodity flow. @@ -13409,8 +13827,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & f^1_a + f^2_a <= "cap"(a) quad forall a in A \ & sum_(a in delta^+(v)) f^k_a - sum_(a in delta^-(v)) f^k_a = b^k_v quad forall k in {1, 2}, v in V \ & sum_(a in delta^-(t_k)) f^k_a - sum_(a in delta^+(t_k)) f^k_a >= R_k quad forall k in {1, 2} \ - & f^1_a, f^2_a in ZZ_(>=0) quad forall a in A - $. + & f^1_a, f^2_a in ZZ_(>=0) quad forall a in A. + $ _Correctness._ Joint capacity and conservation constraints directly encode the two-commodity flow problem. @@ -13429,8 +13847,8 @@ The following reductions to Integer Linear Programming are straightforward formu & f_(v,u) >= "lower"_e (1 - z_e) quad forall e = {u, v} in E \ & sum_(a in delta^+(v)) f_a - sum_(a in delta^-(v)) f_a = b_v quad forall v in V \ & sum_(a in delta^-(t)) f_a - sum_(a in delta^+(t)) f_a >= R \ - & z_e in {0, 1}, f_(u,v) in ZZ_(>=0) - $. + & z_e in {0, 1}, f_(u,v) in ZZ_(>=0). + $ _Correctness._ Direction indicators force flow in one direction per edge; bounds enforce both upper and lower capacity limits. @@ -13449,8 +13867,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_(a in delta^-(v)) f_a = sum_(a in delta^+(v)) f_a quad forall v in V backslash {s, t} \ & f_a = f_b quad forall (a, b) \ & sum_(a in delta^-(t)) f_a - sum_(a in delta^+(t)) f_a >= R \ - & f_a in ZZ_(>=0) quad forall a in A - $. + & f_a in ZZ_(>=0) quad forall a in A. + $ _Correctness._ ($arrow.r.double$) Any feasible integral flow already satisfies the capacity, conservation, equality, and sink-demand constraints. ($arrow.l.double$) Any feasible ILP assignment is exactly an integral arc-flow meeting the homologous-pair and requirement conditions. @@ -13466,8 +13884,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & f_a <= c_a quad forall a in A \ & sum_(a in delta^+(v)) f_a = h(v) sum_(a in delta^-(v)) f_a quad forall v in V backslash {s, t} \ & sum_(a in delta^-(t)) f_a - sum_(a in delta^+(t)) f_a >= R \ - & f_a in ZZ_(>=0) quad forall a in A - $. + & f_a in ZZ_(>=0) quad forall a in A. + $ _Correctness._ ($arrow.r.double$) A valid multiplier flow satisfies these linear equalities and inequalities by definition. ($arrow.l.double$) Any feasible ILP solution gives an integral arc flow whose non-terminal outflow equals the prescribed multiple of its inflow and whose sink inflow meets the requirement. @@ -13482,8 +13900,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & (f_i)_(i = 1)^q \ "subject to" quad & sum_(i : a in P_i) f_i <= c_a quad forall a in A \ & sum_i f_i >= R \ - & f_i in ZZ_(>=0) quad forall i in {1, dots, q} - $. + & f_i in ZZ_(>=0) quad forall i in {1, dots, q}. + $ _Correctness._ ($arrow.r.double$) Any valid path-flow assignment respects every arc capacity and delivers at least $R$ units in total. ($arrow.l.double$) Any feasible ILP solution assigns integral flow only to the prescribed paths, and the aggregated arc loads satisfy the network capacities. @@ -13502,8 +13920,8 @@ The following reductions to Integer Linear Programming are straightforward formu & f^k_(u,v) + f^k_(v,u) <= 1 quad forall {u, v} in E, k \ & sum_k sum_(w in N(v)) f^k_(v,w) <= 1 quad forall "non-terminal" v \ & h^k_v >= h^k_u + 1 - M (1 - f^k_(u,v)) quad forall k, u -> v \ - & f^k_(u,v) in {0, 1}, h^k_v in ZZ_(>=0) - $. + & f^k_(u,v) in {0, 1}, h^k_v in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) A family of pairwise internally vertex-disjoint connecting paths orients each path from its source to its sink and satisfies all constraints. ($arrow.l.double$) The conservation, disjointness, and ordering constraints force each commodity to trace one simple path, and different commodities can intersect only at terminals. @@ -13524,8 +13942,8 @@ The following reductions to Integer Linear Programming are straightforward formu & h^k_s = 0 quad forall k \ & h^k_v >= h^k_u + 1 - M (1 - f^k_(u,v)) quad forall k, u -> v \ & h^k_t <= K quad forall k \ - & f^k_(u,v) in {0, 1}, h^k_v in {0, dots, K} - $. + & f^k_(u,v) in {0, 1}, h^k_v in {0, dots, K}. + $ _Correctness._ ($arrow.r.double$) A collection of $J$ internally disjoint $s$-$t$ paths of length at most $K$ yields feasible commodity flows and consistent hop labels. ($arrow.l.double$) The flow and hop constraints force each commodity to be a simple $s$-$t$ path, while the vertex-disjointness inequalities match the source requirement. @@ -13575,8 +13993,8 @@ The following reductions to Integer Linear Programming are straightforward formu & 0 <= f_j, h_j <= (n - 1) y_j quad forall j in {0, dots, L - 1} \ & "forward and reverse root-flow conservation hold on the used support" \ & sum_(j = 0)^(L - 1) ell_j (r_j(d) + g_j) <= B \ - & d_k, y_j, z_v, rho_v in {0, 1}; g_j in {0, dots, G}; f_j, h_j in {0, dots, n - 1}; s, b_v in ZZ_(>=0) - $. + & d_k, y_j, z_v, rho_v in {0, 1}; g_j in {0, dots, G}; f_j, h_j in {0, dots, n - 1}; s, b_v in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) From any feasible mixed-postman tour, set $d_k$ from the direction in which edge $e_k$ is first required, let $g_j$ be the number of extra copies of $b_j$ beyond the required multiplicity, and let $y_j$ mark the positive-support arcs. The tour itself visits exactly the active vertices, so some active vertex can be chosen as the root. Taking one outgoing spanning arborescence and one incoming spanning arborescence of the used Eulerian digraph gives feasible $f$- and $h$-flows. The walk length is exactly $sum_j ell_j (r_j(d) + g_j)$, hence the ILP is feasible. ($arrow.l.double$) A feasible ILP solution chooses one direction for every undirected edge, and the balance equations make the directed multigraph with multiplicities $r_j(d) + g_j$ Eulerian. The two root-flow systems imply that the positive-support digraph on the active vertices is strongly connected. Therefore the used multigraph admits an Euler tour, and its total length is exactly the bounded linear form above, so the source instance is a YES-instance. @@ -13599,8 +14017,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_(w : {r, w} in E) f_(r,w) - sum_(u : {u, r} in E) f_(u,r) = sum_v z_v - 1 \ & sum_(u : {u, v} in E) f_(u,v) - sum_(w : {v, w} in E) f_(v,w) = z_v quad forall v in V backslash {r} \ & sum_e ell_e t_e <= B \ - & y_e, z_v in {0, 1}, t_e in {0, 1, 2}, q_v, f_(u,v) in ZZ_(>=0) - $. + & y_e, z_v in {0, 1}, t_e in {0, 1, 2}, q_v, f_(u,v) in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any feasible rural-postman circuit uses each edge at most twice, has even degrees, is connected on its positive-support edges, and satisfies the bound. ($arrow.l.double$) A feasible ILP solution defines a connected Eulerian multigraph containing every required edge, hence an Eulerian circuit of total length at most $B$. @@ -13640,8 +14058,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_(i,j,p) >= x_(i,p) + x_(j,(p + 1) mod m) - 1 quad forall i, j, p \ & z_(i,j,p) = 0 quad "whenever" D["head"_i, "tail"_j] = oo \ & sum_(i = 0)^(m - 1) ell_i + sum_(p = 0)^(m - 1) sum_(i = 0)^(m - 1) sum_(j = 0)^(m - 1) D["head"_i, "tail"_j] z_(i,j,p) <= B \ - & x_(i,p), z_(i,j,p) in {0, 1} - $. + & x_(i,p), z_(i,j,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible Stacker Crane permutation determines a one-hot assignment and consecutive-pair indicators whose connector costs equal the route length. ($arrow.l.double$) Any feasible ILP solution yields a permutation of the required arcs, and the linearized connector term is exactly the sum of shortest paths between consecutive arcs. @@ -13657,8 +14075,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(u) f^t_(u,v) - sum_(w) f^t_(v,w) = b_(t,v) quad forall t in R backslash {r}, v in V \ & f^t_(u,v) <= y_(u,v) quad forall {u, v} in E, t in R backslash {r} \ & f^t_(v,u) <= y_(u,v) quad forall {u, v} in E, t in R backslash {r} \ - & y_(u,v) in {0, 1}, f^t_(u,v) in ZZ_(>=0) - $, + & y_(u,v) in {0, 1}, f^t_(u,v) in ZZ_(>=0), + $ where $b_(t,v) = -1$ if $v = r$, $b_(t,v) = 1$ if $v = t$, and $b_(t,v) = 0$ otherwise. _Correctness._ ($arrow.r.double$) A Steiner tree supports a unit flow from the root to every other terminal using exactly its selected edges, with the same total weight. ($arrow.l.double$) Any feasible ILP solution selects a connected subgraph spanning all terminals, and with nonnegative edge weights an optimum solution is a minimum-weight Steiner tree. @@ -13679,8 +14097,8 @@ The following reductions to Integer Linear Programming are straightforward formu & C_(j,q + 1) >= C_(j,q) + p_(j,q + 1) quad forall j, q in {1, dots, m - 1} \ & C_(j,q) >= C_(i,q) + p_(j,q) - M (1 - y_(i,j)) quad forall i != j, q in {1, dots, m} \ & C_(j,m) <= D quad forall j \ - & y_(i,j) in {0, 1}, C_(j,q) in ZZ_(>=0) - $. + & y_(i,j) in {0, 1}, C_(j,q) in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any feasible flow-shop permutation induces a total order and completion times satisfying the machine and deadline constraints. ($arrow.l.double$) Any feasible ILP solution defines one common order of the jobs on all machines, and the resulting schedule completes by the deadline. @@ -13699,8 +14117,8 @@ The following reductions to Integer Linear Programming are straightforward formu & s_(j,i') - s_(j,i) - M y_(j i i') >= p(j, i) - M quad forall j, i < i' \ & s_(j,i) - s_(j,i') + M y_(j i i') >= p(j, i') quad forall j, i < i' \ & C - s_(j,i) >= p(j, i) quad forall j, i \ - & x_(j k i), y_(j i i') in {0,1},; s_(j,i), C in ZZ_(>=0) - $. + & x_(j k i), y_(j i i') in {0,1},; s_(j,i), C in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any feasible open-shop schedule with the given permutations $sigma_i$ induces valid ordering bits $x_{j k i}$ and $y_{j i i'}$ and start times satisfying all non-overlap constraints. ($arrow.l.double$) Any feasible ILP solution defines non-overlapping start times for all tasks, respecting both machine and job constraints. @@ -13717,8 +14135,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_j x_(j,p) = 1 quad forall p \ & sum_p p x_(i,p) + 1 <= sum_p p x_(j,p) quad "for each precedence" (i, j) \ & sum_p (p + 1) x_(j,p) - d_j <= M u_j quad forall j \ - & x_(j,p), u_j in {0, 1} - $. + & x_(j,p), u_j in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible schedule gives a permutation and tardy bits with objective equal to the number of tardy tasks. ($arrow.l.double$) Any feasible ILP assignment decodes to a precedence-respecting permutation, and each $u_j$ is forced to record whether task $j$ misses its deadline. @@ -13734,8 +14152,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_t x_(j,t) = 1 quad forall j \ & sum_j x_(j,t) <= m quad forall t \ & sum_j r_(j,q) x_(j,t) <= B_q quad forall q, t \ - & x_(j,t) in {0, 1} - $. + & x_(j,t) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible schedule chooses one slot per task while respecting processor and resource capacities in every period. ($arrow.l.double$) Any feasible ILP solution directly gives such a slot assignment. @@ -13752,8 +14170,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_j x_(j,p) = 1 quad forall p \ & sum_p p x_(i,p) + 1 <= sum_p p x_(j,p) quad "for each precedence" (i, j) \ & sum_j sum_(p in {0, dots, q}) c_j x_(j,p) <= K quad forall q \ - & x_(j,p) in {0, 1} - $. + & x_(j,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A feasible permutation satisfies the precedence constraints and keeps every prefix sum at most $K$. ($arrow.l.double$) Any feasible ILP assignment is a permutation whose cumulative cost after each prefix is exactly the linear expression being bounded. @@ -13769,8 +14187,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_p x_(j,p) = 1 quad forall j \ & sum_j x_(j,p) = 1 quad forall p \ & M x_(j,p) + sum_(p' < p) sum_(j') ell_(j') x_(j',p') - M u_j <= d_j - ell_j + M quad forall j, p \ - & x_(j,p) in {0, 1}, u_j in {0, 1} - $. + & x_(j,p) in {0, 1}, u_j in {0, 1}. + $ The third family of constraints enforces: if task $j$ is at position $p$ (so $x_(j,p) = 1$), then its completion time $ell_j + sum_(p' < p) sum_(j') ell_(j') x_(j',p')$ exceeds $d_j$ only when $u_j = 1$. _Correctness._ ($arrow.r.double$) Any schedule induces completion times; for each tardy task the big-$M$ constraint forces $u_j = 1$, so the objective counts exactly the total tardy weight. ($arrow.l.double$) Any feasible ILP assignment is a valid permutation (by the assignment constraints) and the tardy indicators agree with the actual completion times. @@ -13789,8 +14207,8 @@ The following reductions to Integer Linear Programming are straightforward formu & x_(j,p) + x_(j',p-1) - "sw"_p <= 1 quad forall p >= 1, j, j' : k(j) != k(j') \ & a_(j,p) <= x_(j,p), quad a_(j,p) <= "sw"_p, quad x_(j,p) + "sw"_p - a_(j,p) <= 1 quad forall j, p >= 1 \ & M x_(j,p) + sum_(p' < p) sum_(j') ell_(j') x_(j',p') + sum_(p'=1)^(p) sum_(j') s(k(j')) a_(j',p') <= d_j - ell_j + M quad forall j, p \ - & x_(j,p), "sw"_p, a_(j,p) in {0, 1} - $. + & x_(j,p), "sw"_p, a_(j,p) in {0, 1}. + $ The switch-detection row forces $"sw"_p = 1$ whenever the tasks at positions $p-1$ and $p$ use different compilers. The $a_(j,p)$ linearisation then routes the correct per-compiler setup time into the completion-time bound for each position. _Correctness._ ($arrow.r.double$) Any feasible schedule assigns each task to a position; the switch indicator equals one exactly when consecutive compilers differ, and the deadline constraint is satisfied by hypothesis. ($arrow.l.double$) Any feasible ILP solution is a valid permutation and the deadline bound ensures each task finishes on time accounting for all setup penalties. @@ -13810,8 +14228,8 @@ The following reductions to Integer Linear Programming are straightforward formu & T_j >= C_j - d_j quad forall j \ & T_j >= 0 quad forall j \ & sum_j w_j T_j <= K \ - & y_(i,j) in {0, 1}, C_j in ZZ_(>=0), T_j in ZZ_(>=0) - $. + & y_(i,j) in {0, 1}, C_j in ZZ_(>=0), T_j in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any job order induces completion times and tardiness values satisfying the bound exactly when the source instance is feasible. ($arrow.l.double$) Any feasible ILP solution yields a single-machine order whose weighted tardiness equals the encoded linear objective term. @@ -13826,8 +14244,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_(t = r_j)^(d_j - p_j) x_(j,t) = 1 quad forall j \ & sum_(j, t : t <= tau < t + p_j) x_(j,t) <= 1 quad forall tau \ - & x_(j,t) in {0, 1} - $. + & x_(j,t) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible non-preemptive schedule chooses one valid start time per task and never overlaps two active jobs. ($arrow.l.double$) Any feasible ILP solution gives exactly such a start-time assignment, so executing the jobs in increasing start order solves the source instance. @@ -13844,8 +14262,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_t x_(c,t,h) <= 1 quad forall c, h \ & sum_c x_(c,t,h) <= 1 quad forall t, h \ & sum_h x_(c,t,h) = r_(c,t) quad forall c, t \ - & x_(c,t,h) in {0, 1} - $. + & x_(c,t,h) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any valid timetable satisfies availability, exclusivity, and exact requirement counts. ($arrow.l.double$) Any feasible ILP solution is exactly such a timetable because the variable layout matches the source configuration. @@ -13866,8 +14284,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((u,v),p) <= x_(v,p+1) quad forall (u, v), p \ & z_((u,v),p) >= x_(u,p) + x_(v,p+1) - 1 quad forall (u, v), p \ & sum_((u,v) in E) z_((u,v),p) = 1 quad forall p \ - & x_(v,p), z_((u,v),p) in {0, 1} - $. + & x_(v,p), z_((u,v),p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A Hamiltonian path defines a permutation of the vertices and therefore a feasible assignment matrix with one admissible graph edge between every consecutive pair. ($arrow.l.double$) Any feasible ILP solution is a vertex permutation whose consecutive pairs are graph edges, hence a Hamiltonian path. @@ -13883,8 +14301,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_k x_(v,k) = 1 quad forall v \ & sum_v x_(v,k) = 1 quad forall k \ & x_(v,k) + x_(w,k+1) <= 1 quad forall k, (v, w) in.not A \ - & x_(v,k) in {0, 1} - $. + & x_(v,k) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A directed Hamiltonian path yields a permutation where every consecutive pair is a directed arc; the arc-exclusion constraints are satisfied by definition. ($arrow.l.double$) Any feasible ILP solution defines a vertex permutation whose consecutive pairs are all directed arcs, hence a directed Hamiltonian path. @@ -13904,8 +14322,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((u,v),p) >= x_(u,p) + x_(v,(p+1) mod n) - 1 quad forall (u, v), p \ & sum_((u,v) in E) z_((u,v),p) = 1 quad forall p \ & b >= w_(u,v) z_((u,v),p) quad forall (u, v), p \ - & x_(v,p), z_((u,v),p) in {0, 1}, b in ZZ_(>=0) - $. + & x_(v,p), z_((u,v),p) in {0, 1}, b in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any Hamiltonian tour yields a feasible assignment and sets $b$ to the maximum selected edge weight. ($arrow.l.double$) Any feasible ILP solution encodes a Hamiltonian cycle, and the minimax constraints force $b$ to equal its bottleneck edge weight. @@ -13958,8 +14376,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_e y_e >= 3 \ & sum_e l_e y_e >= K \ & "root-flow connectivity constraints hold on the selected edges" \ - & y_e, s_v in {0, 1} - $. + & y_e, s_v in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A simple circuit has degree 2 at each used vertex, is connected, and meets the length bound $K$. ($arrow.l.double$) The degree and connectivity constraints force the selected edges to form exactly one simple circuit, and the final inequality enforces the required total length. @@ -13977,8 +14395,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((i,p),(j,q)) <= x_(i,p) quad forall i, p, j, q \ & z_((i,p),(j,q)) <= x_(j,q) quad forall i, p, j, q \ & z_((i,p),(j,q)) >= x_(i,p) + x_(j,q) - 1 quad forall i, p, j, q \ - & x_(i,p), z_((i,p),(j,q)) in {0, 1} - $. + & x_(i,p), z_((i,p),(j,q)) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any injective facility placement gives a feasible ILP assignment with exactly the same quadratic cost. ($arrow.l.double$) Any feasible ILP solution decodes to an injective facility-to-location map, and the linearized objective equals the source objective term by term. @@ -13996,8 +14414,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_(u,v) >= p_u - p_v quad forall {u, v} in E \ & z_(u,v) >= p_v - p_u quad forall {u, v} in E \ & sum_({u,v} in E) z_(u,v) <= K \ - & x_(v,p) in {0, 1}, z_(u,v) in ZZ_(>=0) - $. + & x_(v,p) in {0, 1}, z_(u,v) in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any valid linear arrangement satisfies the permutation constraints and gives edge lengths $|p_u - p_v|$ within the bound. ($arrow.l.double$) Any feasible ILP solution is a bijection from vertices to positions, and the auxiliary variables exactly upper-bound the edge lengths, so the total arrangement cost is at most $K$. @@ -14014,8 +14432,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_v x_(v,u) <= 1 quad forall u \ & x_(v,u) + x_(w,u') <= 1 quad forall {v, w} in E_"pat", {u, u'} in.not E_"host" \ & x_(v,u') + x_(w,u) <= 1 quad forall {v, w} in E_"pat", {u, u'} in.not E_"host" \ - & x_(v,u) in {0, 1} - $. + & x_(v,u) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any injective edge-preserving embedding satisfies the assignment and non-edge constraints. ($arrow.l.double$) Any feasible ILP solution is an injective vertex map, and the non-edge inequalities ensure every pattern edge is sent to a host edge. @@ -14033,8 +14451,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(v in V) x_v = n / 2 \ & y_e >= x_u - x_v quad forall e = {u, v} in E \ & y_e >= x_v - x_u quad forall e = {u, v} in E \ - & x_v, y_e in {0, 1} - $. + & x_v, y_e in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any balanced partition assigns $n\/2$ vertices to each side; setting $y_e = |x_u - x_v|$ for each edge gives a feasible ILP solution whose objective equals the cut size. ($arrow.l.double$) The balance constraint forces an equal partition, and the two linking inequalities force $y_e >= |x_u - x_v|$; minimization then drives $y_e = |x_u - x_v|$, so the objective equals the number of crossing edges. @@ -14080,8 +14498,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_(t = 0)^(m - 1) "cost"(a_t) y_t <= K \ & p_v - o_c <= (n - 1) (1 - x_(v,c)), o_c - p_v <= (n - 1) (1 - x_(v,c)) quad forall v, c \ & p_(v_t) - p_(u_t) >= 1 - n sum_(c = 0)^(n - 1) s_(t,c) quad forall t in {0, dots, m - 1} \ - & x_(v,c), s_(t,c), y_t in {0, 1}; o_c, p_v in {0, dots, n - 1} - $. + & x_(v,c), s_(t,c), y_t in {0, 1}; o_c, p_v in {0, dots, n - 1}. + $ _Correctness._ ($arrow.r.double$) Any valid acyclic partition gives a class assignment whose quotient arcs respect some topological ordering, with the same class weights and crossing cost. ($arrow.l.double$) Any feasible ILP solution partitions the vertices, keeps every class within the weight bound, charges exactly the inter-class arcs, and the order variables force the quotient digraph to be acyclic. @@ -14097,8 +14515,8 @@ The following reductions to Integer Linear Programming are straightforward formu "subject to" quad & sum_(l in L) x_l = k \ & sum_(r in R) y_r = k \ & x_l + y_r <= 1 quad forall (l, r) in.not E \ - & x_l, y_r in {0, 1} - $. + & x_l, y_r in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A balanced complete bipartite subgraph of size $k + k$ satisfies the cardinality constraints and has no selected non-edge pair. ($arrow.l.double$) Any feasible ILP solution selects $k$ left vertices and $k$ right vertices with every cross-pair present, hence a balanced biclique. @@ -14116,8 +14534,8 @@ The following reductions to Integer Linear Programming are straightforward formu & z_((l,r),b) >= x_(l,b) + y_(r,b) - 1 quad forall l, r, b \ & sum_b z_((l,r),b) >= 1 quad forall (l, r) in E \ & x_(l,b) + y_(r,b) <= 1 quad forall (l, r) in.not E, b \ - & x_(l,b), y_(r,b), z_((l,r),b) in {0, 1} - $. + & x_(l,b), y_(r,b), z_((l,r),b) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any valid $k$-biclique cover assigns each covered edge to a biclique containing both endpoints, with objective equal to the total biclique size. ($arrow.l.double$) Any feasible ILP solution defines $k$ complete bipartite subgraphs whose union covers every edge, and the objective is exactly the source objective. @@ -14158,8 +14576,8 @@ The following reductions to Integer Linear Programming are straightforward formu & g^(q,t)_(j,eta) = 0 quad "whenever" t in {q, r_q} "or" f_j "is incident to" q \ & g^(q,t)_(j,eta) <= y_j quad forall q, t in {0, dots, n - 1}, j in {0, dots, p - 1}, eta in {0, 1} \ & "for each valid pair" (q,t) ", unit-flow conservation from" r_q "to" t "holds in" G - q \ - & y_j, f^(q,t)_(i,eta), g^(q,t)_(j,eta) in {0, 1} - $. + & y_j, f^(q,t)_(i,eta), g^(q,t)_(j,eta) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) If the chosen augmentation makes the graph biconnected, then every vertex-deleted graph is connected and therefore supports the required flows. ($arrow.l.double$) If the ILP is feasible, then removing any single vertex leaves a connected graph, which is exactly the definition of biconnectivity for the augmented graph. @@ -14208,8 +14626,8 @@ The following reductions to Integer Linear Programming are straightforward formu & "the standard product linearization enforces" b_(v,c) = s_c r_(v,c) quad forall v, c \ & 0 <= f_(i,eta,c) <= (n - 1) x_(u_i,c), 0 <= f_(i,eta,c) <= (n - 1) x_(v_i,c) quad forall i, eta, c \ & sum_"out of v in c" f - sum_"into v in c" f = b_(v,c) - x_(v,c) quad forall v, c \ - & x_(v,c), u_c, r_(v,c) in {0, 1}; s_c in {0, dots, n}; b_(v,c), f_(i,eta,c) in ZZ_(>=0) - $. + & x_(v,c), u_c, r_(v,c) in {0, 1}; s_c in {0, dots, n}; b_(v,c), f_(i,eta,c) in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any valid bounded-component partition assigns each component a connected supporting subgraph and respects the weight bound. ($arrow.l.double$) Any feasible ILP solution partitions the vertices into at most $K$ connected sets, each of total weight at most $B$, exactly as required by the source problem. @@ -14229,8 +14647,8 @@ The following reductions to Integer Linear Programming are straightforward formu & y_e >= x_u - x_v quad forall e = {u, v} in E \ & y_e >= x_v - x_u quad forall e = {u, v} in E \ & sum_e w_e y_e <= K \ - & x_v, y_e in {0, 1} - $. + & x_v, y_e in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible bounded cut determines a 0/1 side assignment, and the edge indicators are 1 exactly on the cut edges. ($arrow.l.double$) Any feasible ILP solution partitions the vertices into two bounded sets with $s$ and $t$ separated and total cut weight at most $K$. @@ -14276,8 +14694,8 @@ The following reductions to Integer Linear Programming are straightforward formu & bar(f)^t_j <= y_j, bar(g)^t_j <= y_j quad forall t in {0, dots, n - 1}, j in {0, dots, p - 1} \ & "root-to-target unit-flow conservation holds on" f^t, bar(f)^t quad forall t != r \ & "target-to-root unit-flow conservation holds on" g^t, bar(g)^t quad forall t != r \ - & y_j, f^t_i, bar(f)^t_j, g^t_i, bar(g)^t_j in {0, 1} - $. + & y_j, f^t_i, bar(f)^t_j, g^t_i, bar(g)^t_j in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A strongly connected augmentation provides both directions of reachability between the root and every other vertex, hence all required flows. ($arrow.l.double$) If those flows exist for every vertex, then every vertex is reachable from the root and can reach the root, so the augmented digraph is strongly connected. @@ -14299,8 +14717,8 @@ The following reductions to Integer Linear Programming are straightforward formu & w_(i,j) <= sum_r p_(i,r,j) quad forall i, j \ & e_(i,j) >= A_(i,j) - w_(i,j) quad forall i, j \ & e_(i,j) >= w_(i,j) - A_(i,j) quad forall i, j \ - & b_(i,r), c_(r,j), p_(i,r,j), w_(i,j) in {0, 1}, e_(i,j) in ZZ_(>=0) - $. + & b_(i,r), c_(r,j), p_(i,r,j), w_(i,j) in {0, 1}, e_(i,j) in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any choice of factor matrices induces the same Boolean product and Hamming error in the ILP. ($arrow.l.double$) Any feasible ILP assignment determines factor matrices $B$ and $C$, and the linearization forces the objective to equal the Hamming distance between $A$ and $B dot C$. @@ -14319,8 +14737,8 @@ The following reductions to Integer Linear Programming are straightforward formu & b_(r,0) = a_(r,0) quad forall r \ & b_(r,p) >= a_(r,p) - a_(r,p-1) quad forall r, p > 0 \ & sum_(r,p) b_(r,p) <= K \ - & x_(c,p), a_(r,p), b_(r,p) in {0, 1} - $. + & x_(c,p), a_(r,p), b_(r,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any column permutation determines exactly one block-start variable for each maximal run of 1s in every row. ($arrow.l.double$) A feasible ILP solution is a column permutation whose counted block starts sum to at most $K$, which is precisely the source criterion. @@ -14374,8 +14792,8 @@ The following reductions to Integer Linear Programming are straightforward formu & h_(r,p) >= sum_(q = 0)^p ell_(r,q) + sum_(q = p)^(n - 1) u_(r,q) - 1 quad forall r, p \ & a_(r,p) <= h_(r,p); h_(r,p) <= a_(r,p) + f_(r,p); f_(r,p) <= h_(r,p); f_(r,p) + a_(r,p) <= 1 quad forall r, p \ & sum_(r = 0)^(m - 1) sum_(p = 0)^(n - 1) f_(r,p) <= K \ - & x_(c,p), a_(r,p), ell_(r,p), u_(r,p), h_(r,p), f_(r,p) in {0, 1} - $. + & x_(c,p), a_(r,p), ell_(r,p), u_(r,p), h_(r,p), f_(r,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A feasible augmentation chooses a permutation and flips exactly the zeros lying inside each row's final consecutive-ones interval. ($arrow.l.double$) Any feasible ILP solution yields a permuted matrix whose rows become consecutive-ones after the encoded zero-to-one augmentations, with total augmentation cost at most $K$. @@ -14392,8 +14810,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_p x_(c,p) = s_c quad forall c \ & sum_c x_(c,p) = 1 quad forall p in {1, dots, K} \ & "the selected rows satisfy the consecutive-ones interval constraints" \ - & s_c, x_(c,p) in {0, 1} - $. + & s_c, x_(c,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any feasible column subset with a valid permutation satisfies the selection and interval constraints. ($arrow.l.double$) Any feasible ILP solution chooses exactly $K$ columns whose induced submatrix admits a consecutive-ones permutation. @@ -14408,8 +14826,8 @@ The following reductions to Integer Linear Programming are straightforward formu "find" quad & bold(x) \ "subject to" quad & sum_g x_(r,g) = 1 quad forall r \ & x_(r,g) + x_(s,h) <= 1 quad "whenever" A_(r,i) = A_(s,j) = 1 "and" i + g = j + h \ - & x_(r,g) in {0, 1} - $. + & x_(r,g) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) A valid compression chooses one shift per row and never overlays 1-entries from different rows in the same storage position. ($arrow.l.double$) Any feasible ILP solution gives exactly such a collision-free shift assignment, hence a valid storage vector of length $n + K$. @@ -14428,8 +14846,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_p m_(s,j,p) = 1 quad forall s, j \ & m_(s,j,p) <= x_(p,a) quad forall s, j, p " with symbol " a \ & "matching positions are strictly increasing in j for every string s" \ - & x_(p,a), m_(s,j,p) in {0, 1} - $. + & x_(p,a), m_(s,j,p) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any common supersequence of length at most $B$ induces a one-hot symbol assignment and a monotone match of every input string. ($arrow.l.double$) Any feasible ILP solution yields a length-$B$ string into which every source string embeds as a subsequence. @@ -14502,8 +14920,8 @@ The following reductions to Integer Linear Programming are straightforward formu & "the exact M = 1 state-update equations enforce no-op, delete, and adjacent-swap transitions" \ & sum_(i : x_i = y_p) z_(K,p,i) = 1 quad forall p in {0, dots, m - 1} \ & e_(K,p) = 1 quad forall p in {m, dots, n - 1} \ - & z_(t,p,i), e_(t,p), d_(t,j), s_(t,j), nu_t in {0, 1} - $. + & z_(t,p,i), e_(t,p), d_(t,j), s_(t,j), nu_t in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any valid length-$K$ edit script yields a feasible sequence of operations and states ending at the target. ($arrow.l.double$) Any feasible ILP solution traces a legal sequence of deletes, adjacent swaps, and no-ops whose final string is the target. @@ -14566,8 +14984,8 @@ The following reductions to Integer Linear Programming are straightforward formu & k_p = 1 - x_i quad "otherwise" \ & c_p >= k_p - k_(p-1) quad forall p > 0 \ & c_p >= k_(p-1) - k_p quad forall p > 0 \ - & x_i, k_p, c_p in {0, 1} - $. + & x_i, k_p, c_p in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any first-occurrence coloring determines the whole paint sequence and induces exactly the same number of switches in the ILP. ($arrow.l.double$) Any ILP assignment is already a valid source witness, and the switch variables are forced to count adjacent color changes. @@ -14584,8 +15002,8 @@ The following reductions to Integer Linear Programming are straightforward formu & sum_u x_(u,v) = 1 quad forall v \ & x_(u,v) + x_(w,z) <= 1 quad forall {u, w} in E_"tree", {v, z} in.not E_"graph" \ & x_(u,z) + x_(w,v) <= 1 quad forall {u, w} in E_"tree", {v, z} in.not E_"graph" \ - & x_(u,v) in {0, 1} - $. + & x_(u,v) in {0, 1}. + $ _Correctness._ ($arrow.r.double$) Any isomorphism from the given tree to a spanning tree of the graph satisfies the bijection and non-edge constraints. ($arrow.l.double$) Any feasible ILP solution is a bijection that preserves every tree edge, so the image edges form a spanning tree of the graph isomorphic to the source tree. @@ -14707,8 +15125,8 @@ The following reductions to Integer Linear Programming are straightforward formu & B_s - d_v <= (n - 1) (1 - b_(s,v)), d_v - B_s <= (n - 1) (1 - b_(s,v)) quad forall s, v \ & c_s = B_s - T_s + 1 - |S_(k_s)|, c_s >= 0 quad forall s; sum_s c_s <= K \ & p_(v,u), a_(u,v), h_(u,v,w), t_(s,u), b_(s,v), m_(s,u,v) in {0, 1} \ - & d_v, T_s, B_s, c_s in ZZ_(>=0) - $. + & d_v, T_s, B_s, c_s in ZZ_(>=0). + $ _Correctness._ ($arrow.r.double$) Any rooted tree satisfying all subset-path conditions induces parent, depth, and path-endpoint variables with the same total extension cost. ($arrow.l.double$) Any feasible ILP solution defines a rooted tree in which every subset lies on one ancestor chain, and the encoded path lengths keep the total extension cost within the bound. @@ -14767,7 +15185,7 @@ The following reductions to Integer Linear Programming are straightforward formu *Step 1 -- Source instance.* The source digraph has vertices ${#range(mfas_mlr.source.instance.graph.num_vertices).map(str).join(", ")}$ and arcs #{source-arcs.map(a => $(#(a.at(0)) arrow #(a.at(1)))$).join(", ")}, all with unit weight. The extracted optimal feedback arc set removes #{removed-arcs.map(a => $(#(a.at(0)) arrow #(a.at(1)))$).join(" and ")}, so $|F| = #removed-arcs.len()$. *Step 2 -- Build the comparison matrix.* The reduction keeps the same item set and writes $M_(i j) = 1$ when only $i arrow j$ exists, $M_(i j) = -1$ when only $j arrow i$ exists, and $M_(i j) = 0$ otherwise. For this instance, - $ M = mat(#fmt-mat(target-matrix)) $. + $ M = mat(#fmt-mat(target-matrix)). $ Every off-diagonal pair sums to $0$, so the target is a valid Maximum Likelihood Ranking instance with $c = 0$. *Step 3 -- Verify a solution.* The stored ranking vector is $(#ranking.map(str).join(", "))$, interpreted as the map from items to ranks. The target disagreement cost is $#target-cost = 2 dot #removed-arcs.len() - #source-arcs.len()$, and the extracted source witness is exactly the backward-arc set #{removed-arcs.map(a => $(#(a.at(0)) arrow #(a.at(1)))$).join(" and ")} #sym.checkmark @@ -17324,7 +17742,7 @@ The following table shows concrete variable overhead for example instances, take _Construction._ Let the source instance have universe size $q$ and triples $m_l = (w_(a_l), x_(b_l), y_(c_l))$ for $l = 0, dots, t - 1$. If some coordinate of $W union X union Y$ is absent from all triples, the source instance is trivially NO, so the implementation returns a fixed infeasible 3-Partition instance with sizes $(6, 6, 6, 6, 7, 9)$ and bound $20$. Otherwise set $r = 32 q$ and $T_1 = 40 r^4$. For each triple create - $ u_l = 10 r^4 - c_l r^3 - b_l r^2 - a_l r $, + $ u_l = 10 r^4 - c_l r^3 - b_l r^2 - a_l r, $ one $B$-item $10 r^4 + a_l r$ on the first occurrence of coordinate $a_l$ and $11 r^4 + a_l r$ on later occurrences, one $C$-item $10 r^4 + b_l r^2$ on the first occurrence of $b_l$ and $11 r^4 + b_l r^2$ later, and one $D$-item $10 r^4 + c_l r^3$ on the first occurrence of $c_l$ and $8 r^4 + c_l r^3$ later. This is the ABCD-Partition instance. Tag the four classes modulo 16: @@ -17334,7 +17752,7 @@ The following table shows concrete variable overhead for example instances, take For every tagged number create one regular element $w_i = 4(5 T_2 + a_i) + 1$. For every unordered pair $i < j$, create pairing elements $ u_(i j) = 4(6 T_2 - a_i - a_j) + 2 $ and - $ u'_(i j) = 4(5 T_2 + a_i + a_j) + 2 $. + $ u'_(i j) = 4(5 T_2 + a_i + a_j) + 2. $ Finally add $8 t^2 - 3 t$ filler elements of size $20 T_2$ and set the 3-Partition bound to $B = 64 T_2 + 4$. _Correctness._ The fixed preprocessing case is immediate: an uncovered coordinate makes the 3DM instance infeasible, and $(6, 6, 6, 6, 7, 9; 20)$ is a valid infeasible 3-Partition instance. @@ -17385,8 +17803,8 @@ The following table shows concrete variable overhead for example instances, take "subject to" quad & sum_(l : a_l = e) x_l = 1 quad forall e in {0, dots, q - 1} quad "(W-coverage)" \ & sum_(l : b_l = e) x_l = 1 quad forall e in {0, dots, q - 1} quad "(X-coverage)" \ & sum_(l : c_l = e) x_l = 1 quad forall e in {0, dots, q - 1} quad "(Y-coverage)" \ - & x_l in {0, 1} quad forall l in {0, dots, t - 1} - $. + & x_l in {0, 1} quad forall l in {0, dots, t - 1}. + $ _Correctness._ ($arrow.r.double$) A perfect 3-dimensional matching selects $q$ triples covering every element exactly once. Setting $x_l = 1$ for selected triples satisfies all $3q$ equality constraints. ($arrow.l.double$) Any binary feasible solution selects a set of triples in which every element of $W$, $X$, and $Y$ appears exactly once, which is a perfect 3-dimensional matching. diff --git a/docs/paper/references.bib b/docs/paper/references.bib index fc9cd0a8..bb99fc9c 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -573,6 +573,16 @@ @article{xiao2017 doi = {10.1016/j.ic.2017.06.001} } +@article{xiao2014, + author = {Mingyu Xiao and Hiroshi Nagamochi}, + title = {A Refined Exact Algorithm for Edge Dominating Set}, + journal = {Theoretical Computer Science}, + volume = {560}, + pages = {207--216}, + year = {2014}, + doi = {10.1016/j.tcs.2014.03.035} +} + @article{robson1986, author = {J. M. Robson}, title = {Algorithms for Maximum Independent Sets}, @@ -602,6 +612,48 @@ @article{vanrooij2013 doi = {10.1007/s00224-012-9412-5} } +@article{karivhakimi1979, + author = {Oded Kariv and S. Louis Hakimi}, + title = {An Algorithmic Approach to Network Location Problems. {II}: The $p$-Medians}, + journal = {SIAM Journal on Applied Mathematics}, + volume = {37}, + number = {3}, + pages = {539--560}, + year = {1979}, + doi = {10.1137/0137041} +} + +@inproceedings{cohenaddad2022, + author = {Vincent Cohen-Addad and Anupam Gupta and Lunjia Hu and Hoon Oh and David Saulpic}, + title = {An Improved Local Search Algorithm for $k$-Median}, + booktitle = {Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)}, + pages = {1556--1612}, + year = {2022}, + doi = {10.1137/1.9781611977073.65} +} + +@article{hochbaumshmoys1985, + author = {Dorit S. Hochbaum and David B. Shmoys}, + title = {A Best Possible Heuristic for the $k$-Center Problem}, + journal = {Mathematics of Operations Research}, + volume = {10}, + number = {2}, + pages = {180--184}, + year = {1985}, + doi = {10.1287/moor.10.2.180} +} + +@article{hsunemhauser1979, + author = {Wen-Lian Hsu and George L. Nemhauser}, + title = {Easy and Hard Bottleneck Location Problems}, + journal = {Discrete Applied Mathematics}, + volume = {1}, + number = {3}, + pages = {209--215}, + year = {1979}, + doi = {10.1016/0166-218X(79)90044-1} +} + @article{vanrooij2011, author = {Johan M. M. van Rooij and Hans L. Bodlaender}, title = {Exact algorithms for dominating set}, @@ -1287,6 +1339,17 @@ @article{even1976 doi = {10.1137/0205048} } +@article{fredericksonjaja1981, + author = {Greg N. Frederickson and Joseph Ja'Ja'}, + title = {Approximation Algorithms for Several Graph Augmentation Problems}, + journal = {SIAM Journal on Computing}, + volume = {10}, + number = {2}, + pages = {270--283}, + year = {1981}, + doi = {10.1137/0210019} +} + @article{frederickson1979, author = {Greg N. Frederickson}, title = {Approximation Algorithms for Some Postman Problems}, @@ -1707,3 +1770,78 @@ @article{fomin2019 year = {2019}, doi = {10.1145/3277568} } + +@book{vonNeumannMorgenstern1944, + author = {John von Neumann and Oskar Morgenstern}, + title = {Theory of Games and Economic Behavior}, + publisher = {Princeton University Press}, + year = {1944} +} + +@article{chvatal1973, + author = {Václav Chvátal}, + title = {On the computational complexity of finding a kernel}, + journal = {Report CRM-300, Centre de Recherches Mathématiques, Université de Montréal}, + year = {1973} +} + +@article{richardson1953, + author = {Moses Richardson}, + title = {Solutions of Irreflexive Relations}, + journal = {Annals of Mathematics}, + volume = {58}, + number = {3}, + pages = {573--590}, + year = {1953}, + doi = {10.2307/1969755} +} + +@article{galvin1995, + author = {Fred Galvin}, + title = {The List Chromatic Index of a Bipartite Multigraph}, + journal = {Journal of Combinatorial Theory, Series B}, + volume = {63}, + number = {1}, + pages = {153--158}, + year = {1995}, + doi = {10.1006/jctb.1995.1011} +} + +@article{clark1990, + author = {Brent N. Clark and Charles J. Colbourn and David S. Johnson}, + title = {Unit Disk Graphs}, + journal = {Discrete Mathematics}, + volume = {86}, + number = {1--3}, + pages = {165--177}, + year = {1990}, + doi = {10.1016/0012-365X(90)90358-O} +} + +@article{erdosgoodmanposa1966, + author = {Paul Erd{\H{o}}s and A. W. Goodman and Louis P{\'o}sa}, + title = {The Representation of a Graph by Set Intersections}, + journal = {Canadian Journal of Mathematics}, + volume = {18}, + pages = {106--112}, + year = {1966}, + doi = {10.4153/CJM-1966-014-3} +} + +@article{gramm2009, + author = {Jens Gramm and Jiong Guo and Falk H{\"u}ffner and Rolf Niedermeier}, + title = {Data Reduction and Exact Algorithms for Clique Cover}, + journal = {ACM Journal of Experimental Algorithmics}, + volume = {13}, + pages = {2.2:1--2.2:30}, + year = {2009}, + doi = {10.1145/1412228.1412236} +} + +@inproceedings{lovasz1973, + author = {László Lovász}, + title = {Coverings and Colorings of Hypergraphs}, + booktitle = {Proceedings of the 4th Southeastern Conference on Combinatorics, Graph Theory, and Computing (Congressus Numerantium 8)}, + pages = {3--12}, + year = {1973} +} diff --git a/problemreductions-cli/src/problem_name.rs b/problemreductions-cli/src/problem_name.rs index 453bfe6b..d5191878 100644 --- a/problemreductions-cli/src/problem_name.rs +++ b/problemreductions-cli/src/problem_name.rs @@ -310,6 +310,8 @@ mod tests { "BiconnectivityAugmentation" ); assert_eq!(resolve_alias("DMVC"), "DecisionMinimumVertexCover"); + assert_eq!(resolve_alias("VC"), "DecisionMinimumVertexCover"); + assert_eq!(resolve_alias("VertexCover"), "DecisionMinimumVertexCover"); // Pass-through for full names assert_eq!( resolve_alias("MaximumIndependentSet"), diff --git a/src/models/graph/minimum_vertex_cover.rs b/src/models/graph/minimum_vertex_cover.rs index ae74aefa..f33b9313 100644 --- a/src/models/graph/minimum_vertex_cover.rs +++ b/src/models/graph/minimum_vertex_cover.rs @@ -186,7 +186,7 @@ crate::register_decision_variant!( MinimumVertexCover, "DecisionMinimumVertexCover", "1.1996^num_vertices", - &["DMVC"], + &["DMVC", "VC", "VertexCover"], "Decision version: does a vertex cover of cost <= bound exist?", dims: [ VariantDimension::new("graph", "SimpleGraph", &["SimpleGraph"]), diff --git a/src/models/graph/multiple_copy_file_allocation.rs b/src/models/graph/multiple_copy_file_allocation.rs index 1e06010b..c54269d3 100644 --- a/src/models/graph/multiple_copy_file_allocation.rs +++ b/src/models/graph/multiple_copy_file_allocation.rs @@ -191,12 +191,12 @@ pub(crate) fn canonical_model_example_specs() -> Vec Vec