reductions.typ

// Problem Reductions: A Mathematical Reference
#let graph-data = json("../src/reductions/reduction_graph.json")
#import "@preview/cetz:0.4.2": canvas, draw
#import "@preview/ctheorems:1.1.3": thmbox, thmplain, thmproof, thmrules
#import "lib.typ": g-node, g-edge, petersen-graph, house-graph, octahedral-graph, draw-grid-graph, draw-triangular-graph, graph-colors, selem, sregion, draw-node-highlight, draw-edge-highlight, draw-node-colors, sregion-selected, sregion-dimmed, gate-and, gate-or, gate-xor

#set page(paper: "a4", margin: (x: 2cm, y: 2.5cm))
#set text(font: "New Computer Modern", size: 10pt)
#set par(justify: true)
#set heading(numbering: "1.1")

#show link: set text(blue)

// Set up theorem environments with ctheorems
#show: thmrules.with(qed-symbol: $square$)

// === Example JSON helpers ===
// Load example JSON files generated by `make examples`.
// Unified schema: { source: { problem, variant, instance }, target: { ... }, overhead: [...] }
#let load-example(name) = json("examples/" + name + ".json")

// Load result JSON: { solutions: [{ source_config, target_config }, ...] }
#let load-results(name) = json("examples/" + name + ".result.json")

#let problem-schemas = json("../src/reductions/problem_schemas.json")

// Problem display names for theorem headers
#let display-name = (
  "MaximumIndependentSet": [Maximum Independent Set],
  "MinimumVertexCover": [Minimum Vertex Cover],
  "MaxCut": [Max-Cut],
  "KColoring": [$k$-Coloring],
  "MinimumDominatingSet": [Minimum Dominating Set],
  "MaximumMatching": [Maximum Matching],
  "TravelingSalesman": [Traveling Salesman],
  "MaximumClique": [Maximum Clique],
  "MaximumSetPacking": [Maximum Set Packing],
  "MinimumSetCovering": [Minimum Set Covering],
  "SpinGlass": [Spin Glass],
  "QUBO": [QUBO],
  "ILP": [Integer Linear Programming],
  "Satisfiability": [SAT],
  "KSatisfiability": [$k$-SAT],
  "CircuitSAT": [CircuitSAT],
  "Factoring": [Factoring],
  "KingsSubgraph": [King's Subgraph MIS],
  "TriangularSubgraph": [Triangular Subgraph MIS],
  "MaximalIS": [Maximal Independent Set],
  "BMF": [Boolean Matrix Factorization],
  "PaintShop": [Paint Shop],
  "BicliqueCover": [Biclique Cover],
  "BinPacking": [Bin Packing],
  "ClosestVectorProblem": [Closest Vector Problem],
)

// Definition label: "def:<ProblemName>" — each definition block must have a matching label


// Generate theorem label from source/target names (uses full names for consistency)
#let reduction-label(source, target) = {
  label("thm:" + source + "-to-" + target)
}

// State for tracking which reduction rules are described in the paper
#let covered-rules = state("covered-rules", ())

// Extract reductions for a problem from graph-data (returns (name, label) pairs)
#let get-reductions-to(problem-name) = {
  graph-data.edges
    .filter(e => graph-data.nodes.at(e.source).name == problem-name)
    .map(e => (name: graph-data.nodes.at(e.target).name, lbl: reduction-label(graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name)))
    .dedup(key: e => e.name)
}

#let get-reductions-from(problem-name) = {
  graph-data.edges
    .filter(e => graph-data.nodes.at(e.target).name == problem-name)
    .map(e => (name: graph-data.nodes.at(e.source).name, lbl: reduction-label(graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name)))
    .dedup(key: e => e.name)
}

// Render a single reduction with link (uses context to skip broken links gracefully)
#let render-reduction-link(r) = {
  context {
    if query(r.lbl).len() > 0 { link(r.lbl)[#r.name] }
    else { r.name }
  }
}

// Render complexity from graph-data nodes
#let render-complexity(name) = {
  let nodes = graph-data.nodes.filter(n => n.name == name)
  if nodes.len() == 0 { return }
  let seen = ()
  let entries = ()
  for node in nodes {
    if node.complexity not in seen {
      seen.push(node.complexity)
      entries.push(node.complexity)
    }
  }
  block(above: 0.5em)[
    #set text(size: 9pt)
    - Complexity: #entries.map(e => raw(e)).join("; ").
  ]
}

// Render the "Reduces to/from" lines for a problem
#let render-reductions(problem-name) = {
  let reduces-to = get-reductions-to(problem-name)
  let reduces-from = get-reductions-from(problem-name)
  if reduces-to.len() > 0 or reduces-from.len() > 0 {
    block(above: 0.5em)[
    #set text(size: 9pt)
      #if reduces-to.len() > 0 [
        - Reduces to: #reduces-to.map(render-reduction-link).join(", "). \
      ]
      #if reduces-from.len() > 0 [
        - Reduces from: #reduces-from.map(render-reduction-link).join(", ").
      ]
    ]
  }
}

// Render a problem's JSON schema as a field table (subtle styling)
#let render-schema(name) = {
  let schema = problem-schemas.find(s => s.name == name)
  if schema == none { return }
  block(
    stroke: (left: 2pt + luma(180)),
    inset: (left: 8pt),
  )[
    #set text(size: 9pt)
    #table(
      columns: (auto, 1fr),
      inset: (x: 2pt, y: 3pt),
      align: (left, left),
      stroke: none,
      table.header(
        text(fill: luma(30), raw(name)),
      ),
      table.hline(stroke: 0.3pt + luma(200)),
      ..schema.fields.map(f => (
        text(fill: luma(60), raw(f.name)),
        text(fill: luma(60), raw(f.description))
      )).flatten()
    )
  ]
}

// Render a concrete example box from JSON data (unified schema)
#let reduction-example(data, caption: none, body) = {
  block(
    width: 100%,
    inset: (x: 1em, y: 0.8em),
    fill: rgb("#f0f7ff"),
    stroke: (left: 2pt + rgb("#4a86e8")),
  )[
    #if caption != none {
      text(weight: "bold")[Example: #caption]
      parbreak()
    }
    *Source:* #data.source.problem
    #h(1em)
    *Target:* #data.target.problem
    #if body != none { parbreak(); body }
  ]
}

#let theorem = thmplain("theorem", [#h(-1.2em)Rule], base_level: 1)
#let proof = thmproof("proof", "Proof")
#let definition = thmbox(
  "definition",
  "Definition",
  fill: rgb("#f8f8f8"),
  stroke: (left: 2pt + rgb("#4a86e8")),
  inset: (x: 1em, y: 0.8em),
  breakable: true,
  base_level: 1,
)

// Problem definition wrapper: auto-adds schema, complexity, reductions list, and label
#let problem-def(name, def, body) = {
  let lbl = label("def:" + name)
  let title = display-name.at(name)
  [#definition(title)[
    #def
    #render-complexity(name)
    #render-reductions(name)
    #render-schema(name)

    #body
  ]
  #lbl]
}

// Find edge in graph-data by source/target names
#let find-edge(source, target) = {
  let edge = graph-data.edges.find(e => graph-data.nodes.at(e.source).name == source and graph-data.nodes.at(e.target).name == target)
  if edge == none {
    edge = graph-data.edges.find(e => graph-data.nodes.at(e.source).name == target and graph-data.nodes.at(e.target).name == source)
  }
  edge
}

// Build display name from a graph-data node (name + variant)
#let variant-display(node) = {
  let base = display-name.at(node.name)
  if node.variant.len() == 0 { return base }
  let parts = ()
  if "graph" in node.variant and node.variant.graph != "SimpleGraph" {
    parts.push(node.variant.graph)
  }
  if "weight" in node.variant {
    if node.variant.weight == "i32" { parts.push("weighted") }
    else if node.variant.weight == "f64" { parts.push("real-weighted") }
  }
  if "k" in node.variant { parts.push[$k$-ary] }
  if parts.len() > 0 { [#base (#parts.join(", "))] } else { base }
}

// Format overhead fields as inline text
#let format-overhead(overhead) = {
  let parts = overhead.map(o => raw(o.field + " = " + o.formula))
  [_Overhead:_ #parts.join(", ").]
}

// Unified function for reduction rules: theorem + proof + optional example
#let reduction-rule(
  source, target,
  example: false,
  example-caption: none,
  extra: none,
  theorem-body, proof-body,
) = {
  let arrow = sym.arrow.r
  let edge = find-edge(source, target)
  let src-disp = if edge != none { variant-display(graph-data.nodes.at(edge.source)) }
                 else { display-name.at(source) }
  let tgt-disp = if edge != none { variant-display(graph-data.nodes.at(edge.target)) }
                 else { display-name.at(target) }
  let src-lbl = label("def:" + source)
  let tgt-lbl = label("def:" + target)
  let overhead = if edge != none and edge.overhead.len() > 0 { edge.overhead } else { none }
  let thm-lbl = label("thm:" + source + "-to-" + target)
  // Derive example filename from source/target: "Source" → "source", then "source_to_target"
  let example-name = lower(source) + "_to_" + lower(target)

  covered-rules.update(old => old + ((source, target),))

  [
    #v(1em)
    #theorem[
    *(*#context { if query(src-lbl).len() > 0 { link(src-lbl)[#src-disp] } else [#src-disp] }* #arrow *#context { if query(tgt-lbl).len() > 0 { link(tgt-lbl)[#tgt-disp] } else [#tgt-disp] }*)* #theorem-body
    #if overhead != none { linebreak(); format-overhead(overhead) }
  ] #thm-lbl]

  proof[#proof-body]

  if example {
    let data = load-example(example-name)
    pad(left: 1.5em, reduction-example(data, caption: example-caption)[#extra])
  }
}

#align(center)[
  #text(size: 16pt, weight: "bold")[Problem Reductions: Models and Transformations]
  #v(0.5em)
  #text(size: 11pt)[Jin-Guo Liu#super[1] #h(1em) Xi-Wei Pan#super[1]]
  #v(0.3em)
  #text(size: 9pt)[#super[1]Hong Kong University of Science and Technology (Guangzhou)]
  #v(0.3em)
  #text(size: 10pt, style: "italic")[github.com/CodingThrust/problem-reductions]
  #v(1em)
]

#block(width: 100%, inset: (x: 2em, y: 1em))[
  *Abstract.* We present formal definitions for computational problems and polynomial-time reductions implemented in the `problem-reductions` library. For each reduction, we state theorems with constructive proofs that preserve solution structure.
]


// Table of contents
#outline(title: "Contents", indent: 1.5em, depth: 2)

#pagebreak()

= Introduction

A _reduction_ from problem $A$ to problem $B$, denoted $A arrow.long B$, is a polynomial-time transformation of $A$-instances into $B$-instances such that: (1) the transformation runs in polynomial time, (2) solutions to $B$ can be efficiently mapped back to solutions of $A$, and (3) optimal solutions are preserved. The library implements #graph-data.edges.len() reductions connecting #graph-data.nodes.len() problem types.

== Notation

We use the following notation throughout. An _undirected graph_ $G = (V, E)$ consists of a vertex set $V$ and edge set $E subset.eq binom(V, 2)$. For a set $S$, $overline(S)$ or $V backslash S$ denotes its complement. We write $|S|$ for cardinality. A _clique_ in $G$ is a subset $K subset.eq V$ where every pair of distinct vertices is adjacent: $(u, v) in E$ for all distinct $u, v in K$. A _unit disk graph_ is a graph where vertices are points on a 2D lattice and $(u, v) in E$ iff $d(u, v) <= r$ for some radius $r$; a _King's subgraph_ uses the 8-connectivity square grid with $r approx 1.5$. For Boolean variables, $overline(x)$ denotes negation ($not x$). A _literal_ is a variable $x$ or its negation $overline(x)$. A _clause_ is a disjunction of literals. A formula in _conjunctive normal form_ (CNF) is a conjunction of clauses. We abbreviate Independent Set as IS, Vertex Cover as VC, and use $n$ for problem size, $m$ for number of clauses, and $k_j = |C_j|$ for clause size.

= Problem Definitions <sec:problems>

Each problem definition follows this structure:

#block(
  inset: (x: 1em, y: 0.8em),
  fill: rgb("#f8f8f8"),
  stroke: (left: 2pt + rgb("#4a86e8")),
)[
  *Definition N (Problem Name).* Formal problem statement defining input, constraints, and objective.

  #block(
    stroke: (left: 2pt + luma(180)),
    inset: (left: 8pt),
  )[
    #set text(size: 9pt)
    #table(
      columns: (auto, 1fr),
      inset: (x: 6pt, y: 3pt),
      align: (left, left),
      stroke: none,
      table.header(text(fill: luma(30), raw("ProblemName"))),
      table.hline(stroke: 0.3pt + luma(200)),
      text(fill: luma(60), raw("field_name")), text(fill: luma(60), raw("Field description from JSON schema")),
    )
  ]

  #set text(size: 9pt, fill: luma(60))
  _Reduces to:_ ProblemA, ProblemB. \
  _Reduces from:_ ProblemC.
]

The gray schema table shows the JSON field names used in the library's data structures. The reduction links at the bottom connect to the corresponding theorems in @sec:reductions.



== Graph Problems

In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| = n$ vertices and $|E|$ edges.

#problem-def("MaximumIndependentSet")[
  Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that no two vertices in $S$ are adjacent: $forall u, v in S: (u, v) in.not E$.
][
One of Karp's 21 NP-complete problems @karp1972, MIS appears in wireless network scheduling, register allocation, and coding theory @shannon1956. Solvable in polynomial time on bipartite graphs (König's theorem), interval graphs, chordal graphs, and cographs. The best known algorithm runs in $O^*(1.1996^n)$ time via measure-and-conquer branching @xiao2017.

*Example.* Consider the Petersen graph $G$ with $n = 10$ vertices, $|E| = 15$ edges, and unit weights $w(v) = 1$ for all $v in V$. The graph is 3-regular (every vertex has degree 3). A maximum independent set is $S = {v_1, v_3, v_5, v_9}$ with $w(S) = sum_(v in S) w(v) = 4 = alpha(G)$. No two vertices in $S$ share an edge, and no vertex can be added without violating independence.

#figure({
  let pg = petersen-graph()
  draw-node-highlight(pg.vertices, pg.edges, (1, 3, 5, 9))
},
caption: [The Petersen graph with a maximum independent set $S = {v_1, v_3, v_5, v_9}$ shown in blue ($alpha(G) = 4$). Outer vertices $v_0, ..., v_4$ form a pentagon; inner vertices $v_5, ..., v_9$ form a pentagram. Unit weights $w(v_i) = 1$.],
) <fig:petersen-mis>
]

#problem-def("MinimumVertexCover")[
  Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ minimizing $sum_(v in S) w(v)$ such that every edge has at least one endpoint in $S$: $forall (u, v) in E: u in S or v in S$.
][
One of Karp's 21 NP-complete problems @karp1972. Vertex Cover is the complement of Independent Set: $S$ is a vertex cover iff $V backslash S$ is an independent set, so $|"VC"| + |"IS"| = n$. Central to parameterized complexity, admitting FPT algorithms in $O^*(1.2738^k)$ time parameterized by solution size $k$. The best known exact algorithm runs in $O^*(1.1996^n)$ via the MIS complement @xiao2017.

*Example.* Consider the house graph $G$ with $n = 5$ vertices, $|E| = 6$ edges, and unit weights $w(v) = 1$. A minimum vertex cover is $S = {v_0, v_3, v_4}$ with $w(S) = 3$: edge $(v_0, v_1)$ is covered by $v_0$; $(v_0, v_2)$ by $v_0$; $(v_1, v_3)$ by $v_3$; $(v_2, v_3)$ by $v_3$; $(v_2, v_4)$ by $v_4$; $(v_3, v_4)$ by both. The complement ${v_1, v_2}$ is a maximum independent set ($alpha(G) = 2$, confirming $|"VC"| = n - alpha = 3$).

#figure({
  let hg = house-graph()
  draw-node-highlight(hg.vertices, hg.edges, (0, 3, 4))
},
caption: [The house graph with a minimum vertex cover $S = {v_0, v_3, v_4}$ shown in blue ($w(S) = 3$). Every edge is incident to at least one blue vertex.],
) <fig:house-vc>
]

#problem-def("MaxCut")[
  Given $G = (V, E)$ with weights $w: E -> RR$, find partition $(S, overline(S))$ maximizing $sum_((u,v) in E: u in S, v in overline(S)) w(u, v)$.
][
Max-Cut is NP-hard on general graphs @barahona1982 but polynomial-time solvable on planar graphs. The Goemans-Williamson SDP relaxation achieves a 0.878-approximation ratio @goemans1995, which is optimal assuming the Unique Games Conjecture. The best known exact algorithm runs in $O^*(2^(omega n slash 3))$ time via algebraic 2-CSP techniques @williams2005, where $omega < 2.372$ is the matrix multiplication exponent.

*Example.* Consider the house graph $G$ with $n = 5$ vertices, $|E| = 6$ edges, and unit weights $w(e) = 1$. The partition $S = {v_0, v_3}$, $overline(S) = {v_1, v_2, v_4}$ cuts 5 of 6 edges: $(v_0, v_1)$, $(v_0, v_2)$, $(v_1, v_3)$, $(v_2, v_3)$, $(v_3, v_4)$. Only the edge $(v_2, v_4)$ is uncut (both endpoints in $overline(S)$). The cut value is $sum w(e) = 5$.

#figure({
  let hg = house-graph()
  let side-s = (0, 3)
  let cut-edges = hg.edges.filter(e => side-s.contains(e.at(0)) != side-s.contains(e.at(1)))
  draw-edge-highlight(hg.vertices, hg.edges, cut-edges, side-s)
},
caption: [The house graph with max cut $S = {v_0, v_3}$ (blue) vs $overline(S) = {v_1, v_2, v_4}$ (white). Cut edges shown in bold blue; 5 of 6 edges are cut.],
) <fig:house-maxcut>
]
#problem-def("KColoring")[
  Given $G = (V, E)$ and $k$ colors, find $c: V -> {1, ..., k}$ minimizing $|{(u, v) in E : c(u) = c(v)}|$.
][
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.

*Example.* Consider the house graph $G$ with $k = 3$ colors. The coloring $c(v_0) = 1$, $c(v_1) = 2$, $c(v_2) = 2$, $c(v_3) = 1$, $c(v_4) = 3$ is proper: no adjacent pair shares a color, so the number of conflicts is 0. The house graph has chromatic number $chi(G) = 3$ because the triangle $(v_2, v_3, v_4)$ requires 3 colors.

#figure({
  let hg = house-graph()
  draw-node-colors(hg.vertices, hg.edges, (0, 1, 1, 0, 2))
},
caption: [A proper 3-coloring of the house graph. Colors: $c(v_0) = c(v_3) = 1$ (blue), $c(v_1) = c(v_2) = 2$ (red), $c(v_4) = 3$ (teal). Zero conflicts.],
) <fig:house-coloring>
]
#problem-def("MinimumDominatingSet")[
  Given $G = (V, E)$ with weights $w: V -> RR$, find $S subset.eq V$ minimizing $sum_(v in S) w(v)$ s.t. $forall v in V: v in S or exists u in S: (u, v) in E$.
][
Dominating Set models facility location: each vertex in $S$ "covers" itself and its neighbors. Applications include wireless sensor placement and social network influence maximization. W[2]-complete when parameterized by solution size $k$, making it strictly harder than Vertex Cover in the parameterized hierarchy. The best known exact algorithm runs in $O^*(1.4969^n)$ via measure-and-conquer @vanrooij2011.

*Example.* Consider the house graph $G$ with $n = 5$ vertices and unit weights $w(v) = 1$. The set $S = {v_2, v_3}$ is a minimum dominating set with $w(S) = 2$: vertex $v_2$ dominates ${v_0, v_4}$ and $v_3$ dominates ${v_1}$ (both also dominate each other). No single vertex can dominate all others, so $gamma(G) = 2$.

#figure({
  let hg = house-graph()
  draw-node-highlight(hg.vertices, hg.edges, (2, 3))
},
caption: [The house graph with minimum dominating set $S = {v_2, v_3}$ (blue, $gamma(G) = 2$). Every white vertex is adjacent to at least one blue vertex.],
) <fig:house-ds>
]
#problem-def("MaximumMatching")[
  Given $G = (V, E)$ with weights $w: E -> RR$, find $M subset.eq E$ maximizing $sum_(e in M) w(e)$ s.t. $forall e_1, e_2 in M: e_1 inter e_2 = emptyset$.
][
Unlike most combinatorial optimization problems on general graphs, maximum matching is solvable in polynomial time $O(n^3)$ by Edmonds' blossom algorithm @edmonds1965, which introduced the technique of shrinking odd cycles into pseudo-nodes. Matching theory underpins assignment problems, network flows, and the Tutte-Berge formula for matching deficiency.

*Example.* Consider the house graph $G$ with $n = 5$ vertices, $|E| = 6$ edges, and unit weights $w(e) = 1$. A maximum matching is $M = {(v_0, v_1), (v_2, v_4)}$ with $w(M) = 2$. Each matched edge is vertex-disjoint from the others. Vertex $v_3$ is unmatched; since $n$ is odd, no perfect matching exists.

#figure({
  let hg = house-graph()
  draw-edge-highlight(hg.vertices, hg.edges, ((0, 1), (2, 4)), (0, 1, 2, 4))
},
caption: [The house graph with a maximum matching $M = {(v_0, v_1), (v_2, v_4)}$ (blue edges, $w(M) = 2$). Matched vertices shown in blue; $v_3$ is unmatched.],
) <fig:house-matching>
]

#problem-def("TravelingSalesman")[
  Given an undirected graph $G=(V,E)$ with edge weights $w: E -> RR$, find an edge set $C subset.eq E$ that forms a cycle visiting every vertex exactly once and minimizes $sum_(e in C) w(e)$.
][
One of the most intensely studied NP-hard problems, with applications in logistics, circuit board drilling, and DNA sequencing. The best known exact algorithm runs in $O^*(2^n)$ time and space via Held-Karp dynamic programming @heldkarp1962. No $O^*((2-epsilon)^n)$ algorithm is known, and improving the exponential space remains open.

*Example.* Consider the complete graph $K_4$ with vertices ${v_0, v_1, v_2, v_3}$ and edge weights $w(v_0, v_1) = 1$, $w(v_1, v_2) = 2$, $w(v_2, v_3) = 1$, $w(v_0, v_3) = 2$, $w(v_0, v_2) = 3$, $w(v_1, v_3) = 3$. The optimal tour is $v_0 -> v_1 -> v_2 -> v_3 -> v_0$ with cost $1 + 2 + 1 + 2 = 6$. The tour using diagonals, $v_0 -> v_2 -> v_1 -> v_3 -> v_0$, costs $3 + 2 + 3 + 2 = 10$.

#figure({
  let verts = ((0, 0), (1.5, 0), (1.5, 1.5), (0, 1.5))
  let all-edges = ((0,1),(1,2),(2,3),(0,3),(0,2),(1,3))
  let tour = ((0,1),(1,2),(2,3),(0,3))
  let weights = ("1", "2", "1", "2", "3", "3")
  canvas(length: 1cm, {
    for (idx, (u, v)) in all-edges.enumerate() {
      let on-tour = tour.any(t => (t.at(0) == u and t.at(1) == v) or (t.at(0) == v and t.at(1) == u))
      g-edge(verts.at(u), verts.at(v),
        stroke: if on-tour { 2pt + graph-colors.at(0) } else { 1pt + luma(200) })
      let mx = (verts.at(u).at(0) + verts.at(v).at(0)) / 2
      let my = (verts.at(u).at(1) + verts.at(v).at(1)) / 2
      // offset diagonal labels to avoid overlap
      let dx = if u == 0 and v == 2 { -0.25 } else if u == 1 and v == 3 { 0.25 } else { 0 }
      let dy = if u == 0 and v == 2 { 0.15 } else if u == 1 and v == 3 { 0.15 } else { 0 }
      draw.content((mx + dx, my + dy), text(7pt, fill: luma(80))[#weights.at(idx)])
    }
    for (k, pos) in verts.enumerate() {
      g-node(pos, name: "v" + str(k),
        fill: graph-colors.at(0),
        label: text(fill: white)[$v_#k$])
    }
  })
},
caption: [Complete graph $K_4$ with weighted edges. The optimal tour $v_0 -> v_1 -> v_2 -> v_3 -> v_0$ (blue edges) has cost 6.],
) <fig:k4-tsp>
]
#problem-def("MaximumClique")[
  Given $G = (V, E)$, find $K subset.eq V$ maximizing $|K|$ such that all pairs in $K$ are adjacent: $forall u, v in K: (u, v) in E$. Equivalent to MIS on the complement graph $overline(G)$.
][
Maximum Clique arises in social network analysis (finding tightly-connected communities), bioinformatics (protein interaction clusters), and coding theory. The problem is equivalent to Maximum Independent Set on the complement graph $overline(G)$. The best known algorithm runs in $O^*(1.1996^n)$ via the complement reduction to MIS @xiao2017. Robson's direct backtracking algorithm achieves $O^*(1.1888^n)$ using exponential space @robson2001.

*Example.* Consider the house graph $G$ with $n = 5$ vertices and $|E| = 6$ edges. The triangle $K = {v_2, v_3, v_4}$ is a maximum clique of size $omega(G) = 3$: all three pairs $(v_2, v_3)$, $(v_2, v_4)$, $(v_3, v_4)$ are edges. No 4-clique exists because vertices $v_0$ and $v_1$ each have degree 2 and are not adjacent to all of ${v_2, v_3, v_4}$.

#figure({
  let hg = house-graph()
  draw-edge-highlight(hg.vertices, hg.edges, ((2,3), (2,4), (3,4)), (2, 3, 4))
},
caption: [The house graph with maximum clique $K = {v_2, v_3, v_4}$ (blue, $omega(G) = 3$). All edges within the clique are shown in bold blue.],
) <fig:house-clique>
]
#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.

*Example.* Consider the path graph $P_5$ with $n = 5$ vertices, edges $(v_i, v_(i+1))$ for $i = 0, ..., 3$, and unit weights $w(v) = 1$. The set $S = {v_1, v_3}$ 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' = {v_0, v_2, v_4}$ with $w(S') = 3$ is a strictly larger maximal IS, illustrating that maximality does not imply maximum weight.

#figure({
  draw-node-highlight(((0, 0), (1, 0), (2, 0), (3, 0), (4, 0)), ((0,1),(1,2),(2,3),(3,4)), (1, 3))
},
caption: [Path $P_5$ with maximal IS $S = {v_1, v_3}$ (blue, $w(S) = 2$). $S$ is maximal — no white vertex can be added — but not maximum: ${v_0, v_2, v_4}$ achieves $w = 3$.],
) <fig:path-maximal-is>
]


== Set Problems

#problem-def("MaximumSetPacking")[
  Given universe $U$, collection $cal(S) = {S_1, ..., S_m}$ with $S_i subset.eq U$, weights $w: cal(S) -> RR$, find $cal(P) subset.eq cal(S)$ maximizing $sum_(S in cal(P)) w(S)$ s.t. $forall S_i, S_j in cal(P): S_i inter S_j = emptyset$.
][
One of Karp's 21 NP-complete problems @karp1972. Generalizes maximum matching (the special case where all sets have size 2, solvable in polynomial time). Applications include resource allocation, VLSI design, and frequency assignment. The optimization version is as hard to approximate as maximum clique. The best known exact algorithm runs in $O^*(2^m)$ by brute-force enumeration over the $m$ sets#footnote[No algorithm improving on brute-force enumeration is known for general weighted set packing.].

*Example.* Let $U = {1, 2, 3, 4, 5}$ and $cal(S) = {S_1, S_2, S_3, S_4}$ with $S_1 = {1, 2}$, $S_2 = {2, 3}$, $S_3 = {3, 4}$, $S_4 = {4, 5}$, and unit weights $w(S_i) = 1$. A maximum packing is $cal(P) = {S_1, S_3}$ with $w(cal(P)) = 2$: $S_1 inter S_3 = emptyset$. Adding $S_2$ would conflict with both ($S_1 inter S_2 = {2}$, $S_2 inter S_3 = {3}$), and $S_4$ conflicts with $S_3$ ($S_3 inter S_4 = {4}$). The alternative packing ${S_2, S_4}$ also achieves weight 2.

#figure(
  canvas(length: 1cm, {
    // Element positions along a line
    let elems = ((0, 0), (1, 0), (2, 0), (3, 0), (4, 0))
    // Set regions: S1={1,2}, S2={2,3}, S3={3,4}, S4={4,5}
    // Selected packing {S1, S3} in blue, others in gray
    sregion(((0, 0), (1, 0)), label: [$S_1$], ..sregion-selected)
    sregion(((1, 0), (2, 0)), label: [$S_2$], ..sregion-dimmed)
    sregion(((2, 0), (3, 0)), label: [$S_3$], ..sregion-selected)
    sregion(((3, 0), (4, 0)), label: [$S_4$], ..sregion-dimmed)
    // Elements
    for (k, pos) in elems.enumerate() {
      selem(pos, label: [#(k + 1)], fill: black)
    }
  }),
  caption: [Maximum set packing: $cal(P) = {S_1, S_3}$ (blue) are disjoint; $S_2, S_4$ (gray) conflict with the packing.],
) <fig:set-packing>
]

#problem-def("MinimumSetCovering")[
  Given universe $U$, collection $cal(S)$ with weights $w: cal(S) -> RR$, find $cal(C) subset.eq cal(S)$ minimizing $sum_(S in cal(C)) w(S)$ s.t. $union.big_(S in cal(C)) S = U$.
][
One of Karp's 21 NP-complete problems @karp1972. Arises in facility location, crew scheduling, and test suite minimization. The greedy algorithm achieves an $O(ln n)$-approximation where $n = |U|$, which is essentially optimal: cannot be approximated within $(1-o(1)) ln n$ unless P = NP. The best known exact algorithm runs in $O^*(2^m)$ by brute-force enumeration over the $m$ sets#footnote[No algorithm improving on brute-force enumeration is known for general weighted set covering.].

*Example.* Let $U = {1, 2, 3, 4, 5}$ and $cal(S) = {S_1, S_2, S_3}$ with $S_1 = {1, 2, 3}$, $S_2 = {2, 4}$, $S_3 = {3, 4, 5}$, and unit weights $w(S_i) = 1$. A minimum cover is $cal(C) = {S_1, S_3}$ with $w(cal(C)) = 2$: $S_1 union S_3 = {1, 2, 3, 4, 5} = U$. No single set covers all of $U$, so at least two sets are required.

#figure(
  canvas(length: 1cm, {
    // 2D layout: S1={1,2,3} left, S3={3,4,5} right, S2={2,4} bridging bottom
    let elems = (
      (-1.2, 0.4),   // 1: only S1
      (-0.5, -0.4),  // 2: S1 ∩ S2
      (0.3, 0.4),    // 3: S1 ∩ S3
      (1.0, -0.4),   // 4: S2 ∩ S3
      (1.7, 0.4),    // 5: only S3
    )
    // Set regions: S1={1,2,3}, S2={2,4}, S3={3,4,5}
    sregion((elems.at(0), elems.at(1), elems.at(2)), pad: 0.4, label: [$S_1$], ..sregion-selected)
    sregion((elems.at(1), elems.at(3)), pad: 0.35, label: [$S_2$], ..sregion-dimmed)
    sregion((elems.at(2), elems.at(3), elems.at(4)), pad: 0.4, label: [$S_3$], ..sregion-selected)
    // Elements
    for (k, pos) in elems.enumerate() {
      selem(pos, label: [#(k + 1)], fill: black)
    }
  }),
  caption: [Minimum set covering: $cal(C) = {S_1, S_3}$ (blue) cover all of $U$; $S_2$ (gray) is redundant.],
) <fig:set-covering>
]

== Optimization Problems

#problem-def("SpinGlass")[
  Given $n$ spin variables $s_i in {-1, +1}$, pairwise couplings $J_(i j) in RR$, and external fields $h_i in RR$, minimize the Hamiltonian (energy function): $H(bold(s)) = -sum_((i,j)) J_(i j) s_i s_j - sum_i h_i s_i$.
][
The Ising spin glass is the canonical model in statistical mechanics for disordered magnetic systems @barahona1982. Ground-state computation is NP-hard on general interaction graphs but polynomial-time solvable on planar graphs without external field ($h_i = 0$) via reduction to minimum-weight perfect matching. Central to quantum annealing, where hardware natively encodes spin Hamiltonians. The best known general algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[On general interaction graphs, no algorithm improving on brute-force enumeration is known.].

*Example.* Consider $n = 5$ spins on a triangular lattice with uniform antiferromagnetic couplings $J_(i j) = -1$ for all edges and no external field ($h_i = 0$). The Hamiltonian simplifies to $H(bold(s)) = sum_((i,j)) s_i s_j$, which counts parallel pairs minus antiparallel pairs. The lattice contains 7 edges and 3 triangular faces; since each triangle cannot have all three pairs antiparallel, frustration is unavoidable. A ground state is $bold(s) = (+, -, +, +, -)$ achieving $H = -3$: five edges are satisfied (antiparallel) and two are frustrated (parallel). No configuration can satisfy more than 5 of 7 edges.

#figure(
  canvas(length: 1cm, {
    let h = calc.sqrt(3) / 2
    let pos = ((0, h), (1, h), (2, h), (0.5, 0), (1.5, 0))
    let edges = ((0,1), (1,2), (3,4), (0,3), (1,3), (1,4), (2,4))
    let spins = (1, -1, 1, 1, -1)
    // Draw edges: black solid = satisfied, dashed gray = frustrated
    for (u, v) in edges {
      let sat = spins.at(u) * spins.at(v) < 0
      g-edge(pos.at(u), pos.at(v),
        stroke: if sat { 1pt + black } else { (paint: rgb("#cc4444"), thickness: 1.2pt, dash: "dashed") })
    }
    // Draw spins: blue = +1, red = −1
    for (k, p) in pos.enumerate() {
      let up = spins.at(k) > 0
      g-node(p, name: "s" + str(k), radius: 0.22,
        fill: if up { graph-colors.at(0) } else { graph-colors.at(1) },
        label: text(fill: white, if up { $+$ } else { $-$ }))
    }
  }),
  caption: [Triangular lattice with $n = 5$ spins and antiferromagnetic couplings ($J = -1$). Ground state $bold(s) = (+, -, +, +, -)$ with $H = -3$. Solid edges: satisfied (antiparallel); dashed red: frustrated (parallel).],
) <fig:spin-glass>
]

#problem-def("QUBO")[
  Given $n$ binary variables $x_i in {0, 1}$, upper-triangular matrix $Q in RR^(n times n)$, minimize $f(bold(x)) = sum_(i=1)^n Q_(i i) x_i + sum_(i < j) Q_(i j) x_i x_j$ (using $x_i^2 = x_i$ for binary variables).
][
Equivalent to the Ising model via the linear substitution $s_i = 2x_i - 1$. The native formulation for quantum annealing hardware (e.g., D-Wave) and a standard target for penalty-method reductions @glover2019. QUBO unifies many combinatorial problems into a single unconstrained binary framework, making it a universal intermediate representation for quantum and classical optimization. The best known general algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[QUBO inherits the Ising model's complexity; no algorithm improving on brute-force is known for the general case.].

*Example.* Consider $n = 3$ with $Q = mat(-1, 2, 0; 0, -1, 2; 0, 0, -1)$. The objective is $f(bold(x)) = -x_1 - x_2 - x_3 + 2x_1 x_2 + 2x_2 x_3$. Evaluating all $2^3$ assignments: $f(0,0,0) = 0$, $f(1,0,0) = -1$, $f(0,1,0) = -1$, $f(0,0,1) = -1$, $f(1,1,0) = 0$, $f(0,1,1) = 0$, $f(1,0,1) = -2$, $f(1,1,1) = 1$. The minimum is $f^* = -2$ at $bold(x)^* = (1, 0, 1)$: selecting $x_1$ and $x_3$ avoids the penalty terms $2x_1 x_2$ and $2x_2 x_3$.
]

#problem-def("ILP")[
  Given $n$ integer variables $bold(x) in ZZ^n$, constraint matrix $A in RR^(m times n)$, bounds $bold(b) in RR^m$, and objective $bold(c) in RR^n$, find $bold(x)$ minimizing $bold(c)^top bold(x)$ subject to $A bold(x) <= bold(b)$ and variable bounds.
][
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.

*Example.* Minimize $bold(c)^top bold(x) = -5x_1 - 6x_2$ subject to $x_1 + x_2 <= 5$, $4x_1 + 7x_2 <= 28$, $x_1, x_2 >= 0$, $bold(x) in ZZ^2$. The LP relaxation optimum is $p_1 = (7 slash 3, 8 slash 3) approx (2.33, 2.67)$ with value $approx -27.67$, which is non-integral. Branch-and-bound yields the ILP optimum $bold(x)^* = (3, 2)$ with $bold(c)^top bold(x)^* = -27$.

#figure(
  canvas(length: 0.8cm, {
    // Axes
    draw.line((-0.3, 0), (5.5, 0), mark: (end: "straight"), stroke: 0.6pt)
    draw.line((0, -0.3), (0, 4.8), mark: (end: "straight"), stroke: 0.6pt)
    draw.content((5.7, -0.15), text(8pt)[$x_1$])
    draw.content((-0.15, 5.0), text(8pt)[$x_2$])
    // Tick marks
    for i in range(1, 6) {
      draw.line((i, -0.08), (i, 0.08), stroke: 0.4pt)
      draw.content((i, -0.35), text(6pt)[#i])
    }
    for i in range(1, 5) {
      draw.line((-0.08, i), (0.08, i), stroke: 0.4pt)
      draw.content((-0.35, i), text(6pt)[#i])
    }
    // Feasible region polygon: (0,0) → (5,0) → (7/3, 8/3) → (0, 4)
    draw.line((0,0), (5,0), (7/3, 8/3), (0, 4), close: true,
      fill: green.lighten(70%), stroke: none)
    // Constraint lines (extending beyond feasible region)
    draw.line((0, 5), (5, 0), stroke: graph-colors.at(0))  // x1 + x2 = 5
    draw.line((0, 4), (5.25, 1), stroke: orange)            // 4x1 + 7x2 = 28
    // Objective function level curve (dashed): -5x1 - 6x2 = -23, i.e. x2 = (23 - 5x1)/6
    draw.line((0, 23/6), (23/5, 0), stroke: (paint: luma(80), dash: "dashed"))
    // Gradient direction arrow
    draw.line((1.5, 2.5), (1.1, 1.9), mark: (end: "straight"), stroke: 1pt + luma(80))
    draw.content((0.7, 1.75), text(6pt, fill: luma(80))[$bold(c)$])
    // Constraint labels
    draw.content((4.3, 1.0), text(6pt, fill: graph-colors.at(0))[$x_1 + x_2 = 5$], anchor: "west")
    draw.content((4.5, 1.7), text(6pt, fill: orange)[$4x_1 + 7x_2 = 28$], anchor: "west")
    draw.content((1.2, 4.3), text(6pt, fill: luma(80))[objective], anchor: "south")
    // Integer lattice points (hollow circles)
    for x1 in range(6) {
      for x2 in range(5) {
        draw.circle((x1, x2), radius: 0.06, fill: none, stroke: 0.4pt + luma(120))
      }
    }
    // LP optimum (fractional, non-integer)
    draw.circle((7/3, 8/3), radius: 0.1, fill: graph-colors.at(1), stroke: none)
    draw.content((7/3 + 0.3, 8/3 + 0.3), text(7pt)[$p_1$])
    // ILP optimum (integer)
    draw.circle((3, 2), radius: 0.1, fill: graph-colors.at(1), stroke: none)
    draw.content((3.3, 2.3), text(7pt)[$bold(x)^*$])
  }),
  caption: [ILP feasible region (green) with constraints $x_1 + x_2 <= 5$ (blue) and $4x_1 + 7x_2 <= 28$ (orange). Hollow circles mark the integer lattice. The LP relaxation optimum $p_1 = (7 slash 3, 8 slash 3)$ is non-integral; the ILP optimum $bold(x)^* = (3, 2)$ gives $bold(c)^top bold(x)^* = -27$.],
) <fig:ilp-example>
]

#problem-def("ClosestVectorProblem")[
  Given a lattice basis $bold(B) in RR^(m times n)$ (columns $bold(b)_1, dots, bold(b)_n in RR^m$ spanning lattice $cal(L)(bold(B)) = {bold(B) bold(x) : bold(x) in ZZ^n}$) and target $bold(t) in RR^m$, find $bold(x) in ZZ^n$ minimizing $norm(bold(B) bold(x) - bold(t))_2$.
][
  The Closest Vector Problem is a fundamental lattice problem, proven NP-hard by van Emde Boas @vanemde1981. CVP appears in lattice-based cryptography, coding theory, and integer programming @lenstra1983. Kannan's enumeration algorithm @kannan1987 solves CVP in $n^(O(n))$ time; Micciancio and Voulgaris @micciancio2010 improved this to deterministic $O^*(4^n)$ using Voronoi cell computations, and Aggarwal, Dadush, and Stephens-Davidowitz @aggarwal2015 achieved randomized $O^*(2^n)$.

  *Example.* Consider the 2D lattice with basis $bold(b)_1 = (2, 0)^top$, $bold(b)_2 = (1, 2)^top$ and target $bold(t) = (2.8, 1.5)^top$. The lattice points near $bold(t)$ include $bold(B)(1, 0)^top = (2, 0)^top$, $bold(B)(0, 1)^top = (1, 2)^top$, and $bold(B)(1, 1)^top = (3, 2)^top$. The closest is $bold(B)(1, 1)^top = (3, 2)^top$ with distance $norm(bold(B)(1,1)^top - bold(t))_2 = norm((0.2, 0.5))_2 = sqrt(0.04 + 0.25) approx 0.539$.

  #figure(
    canvas(length: 0.8cm, {
      import draw: *
      // Lattice points: B*(x1,x2) = x1*(2,0) + x2*(1,2)
      for x1 in range(0, 3) {
        for x2 in range(0, 3) {
          let px = x1 * 2 + x2 * 1
          let py = x2 * 2
          let is-closest = (x1 == 1 and x2 == 1)
          let nm = "p" + str(x1) + str(x2)
          circle(
            (px, py),
            radius: if is-closest { 0.15 } else { 0.08 },
            fill: if is-closest { graph-colors.at(0) } else { luma(180) },
            stroke: if is-closest { 0.8pt + graph-colors.at(0) } else { 0.4pt + luma(120) },
            name: nm,
          )
        }
      }
      // Target vector
      circle((2.8, 1.5), radius: 0.1, fill: graph-colors.at(1), stroke: none, name: "target")
      content((rel: (0, -0.45), to: "target"), text(7pt)[$bold(t)$])
      // Dashed line from target to closest point
      line("target", "p11", stroke: (paint: graph-colors.at(0), thickness: 0.8pt, dash: "dashed"))
      // Basis vectors as arrows from origin
      line("p00", "p10", mark: (end: "straight"), stroke: 0.8pt + luma(100), name: "b1")
      content((rel: (0, -0.35), to: "b1.mid"), text(7pt)[$bold(b)_1$])
      line("p00", "p01", mark: (end: "straight"), stroke: 0.8pt + luma(100), name: "b2")
      content((rel: (-0.3, 0), to: "b2.mid"), text(7pt)[$bold(b)_2$])
      // Label closest point
      content((rel: (0.45, 0.3), to: "p11"), text(7pt)[$bold(B)(1,1)^top$])
    }),
    caption: [2D lattice with basis $bold(b)_1 = (2, 0)^top$, $bold(b)_2 = (1, 2)^top$. Target $bold(t) = (2.8, 1.5)^top$ (red) and closest lattice point $bold(B)(1,1)^top = (3, 2)^top$ (blue). Distance $norm(bold(B)(1,1)^top - bold(t))_2 approx 0.539$.],
  ) <fig:cvp-example>
]

== Satisfiability Problems

#problem-def("Satisfiability")[
  Given a CNF formula $phi = and.big_(j=1)^m C_j$ with $m$ clauses over $n$ Boolean variables, where each clause $C_j = or.big_i ell_(j i)$ is a disjunction of literals, find an assignment $bold(x) in {0, 1}^n$ such that $phi(bold(x)) = 1$ (all clauses satisfied).
][
The Boolean Satisfiability Problem (SAT) is the first problem proven NP-complete @cook1971. SAT serves as the foundation of NP-completeness theory: showing a new problem NP-hard typically proceeds by reduction from SAT or one of its variants. Despite worst-case hardness, conflict-driven clause learning (CDCL) solvers handle industrial instances with millions of variables. The Strong Exponential Time Hypothesis (SETH) @impagliazzo2001 conjectures that no $O^*((2-epsilon)^n)$ algorithm exists for general CNF-SAT, and the best known algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[SETH conjectures this is optimal; no $O^*((2-epsilon)^n)$ algorithm is known.].

*Example.* Consider $phi = (x_1 or x_2) and (not x_1 or x_3) and (not x_2 or not x_3)$ with $n = 3$ variables and $m = 3$ clauses. The assignment $(x_1, x_2, x_3) = (1, 0, 1)$ satisfies all clauses: $C_1 = (1 or 0) = 1$, $C_2 = (0 or 1) = 1$, $C_3 = (1 or 0) = 1$. Hence $phi(1, 0, 1) = 1$.
]

#problem-def("KSatisfiability")[
  SAT with exactly $k$ literals per clause.
][
The restriction of SAT to exactly $k$ literals per clause reveals a sharp complexity transition: 2-SAT is polynomial-time solvable via implication graph SCC decomposition @aspvall1979 in $O(n+m)$, while $k$-SAT for $k >= 3$ is NP-complete. Random $k$-SAT exhibits a satisfiability threshold at clause density $m slash n approx 2^k ln 2$, a key phenomenon in computational phase transitions. The best known algorithm for 3-SAT runs in $O^*(1.307^n)$ via biased-PPSZ @hansen2019. Under SETH, $k$-SAT requires time $O^*(c_k^n)$ with $c_k -> 2$ as $k -> infinity$.

*Example.* Consider the 3-SAT formula $phi = (x_1 or x_2 or x_3) and (not x_1 or not x_2 or x_3) and (x_1 or not x_2 or not x_3)$ with $n = 3$ variables and $m = 3$ clauses, each containing exactly 3 literals. The assignment $(x_1, x_2, x_3) = (1, 0, 1)$ satisfies all clauses: $C_1 = (1 or 0 or 1) = 1$, $C_2 = (0 or 1 or 1) = 1$, $C_3 = (1 or 1 or 0) = 1$.
]

#problem-def("CircuitSAT")[
  Given a Boolean circuit $C$ composed of logic gates (AND, OR, NOT, XOR) with $n$ input variables, find an input assignment $bold(x) in {0,1}^n$ such that $C(bold(x)) = 1$.
][
Circuit Satisfiability is the most natural NP-complete problem: the Cook-Levin theorem @cook1971 proves NP-completeness by showing any nondeterministic polynomial-time computation can be encoded as a Boolean circuit. CircuitSAT is strictly more succinct than CNF-SAT, since a circuit with $g$ gates may require an exponentially larger CNF formula without auxiliary variables. The Tseitin transformation reduces CircuitSAT to CNF-SAT with only $O(g)$ clauses by introducing one auxiliary variable per gate. The best known algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[No algorithm improving on brute-force is known for general circuits.].

*Example.* Consider the circuit $C(x_1, x_2) = (x_1 "AND" x_2) "XOR" (x_1 "OR" x_2)$ with $n = 2$ inputs. Evaluating: $C(0,0) = (0) "XOR" (0) = 0$, $C(0,1) = (0) "XOR" (1) = 1$, $C(1,0) = (0) "XOR" (1) = 1$, $C(1,1) = (1) "XOR" (1) = 0$. The satisfying assignments are $(0, 1)$ and $(1, 0)$ -- precisely the inputs where exactly one variable is true.

#figure(
  canvas(length: 1cm, {
    // Gate positions: AND/OR vertically stacked, XOR to the right
    // With inputs=2, w=0.8: h = max(0.5, 0.7) = 0.7, ports at ±0.175 from center
    gate-and((2, 0.8), name: "and")
    gate-or((2, -0.8), name: "or")
    gate-xor((4.5, 0), name: "xor")
    // AND → XOR, OR → XOR (right-angle routing)
    draw.line("and.out", (3.5, 0.8), (3.5, 0.175), "xor.in0")
    draw.line("or.out", (3.5, -0.8), (3.5, -0.175), "xor.in1")
    // Output wire and label
    draw.line("xor.out", (5.5, 0), mark: (end: ">"))
    draw.content((5.8, 0), text(8pt)[$C$])
    // x1 fork: to and.in0 (y = 0.975) and or.in0 (y = −0.625)
    draw.line((0, 0.975), (0.8, 0.975), "and.in0")
    draw.line((0.8, 0.975), (0.8, -0.625), "or.in0")
    draw.circle((0.8, 0.975), radius: 0.04, fill: black, stroke: none)
    // x2 fork: to or.in1 (y = −0.975) and and.in1 (y = 0.625)
    draw.line((0, -0.975), (0.5, -0.975), "or.in1")
    draw.line((0.5, -0.975), (0.5, 0.625), "and.in1")
    draw.circle((0.5, -0.975), radius: 0.04, fill: black, stroke: none)
    // Input labels
    draw.content((-0.3, 0.975), text(8pt)[$x_1$])
    draw.content((-0.3, -0.975), text(8pt)[$x_2$])
  }),
  caption: [Circuit $C(x_1, x_2) = (x_1 and x_2) xor (x_1 or x_2)$. Junction dots mark where inputs fork to both gates. Satisfying assignments: $(0,1)$ and $(1,0)$.],
) <fig:circuit-sat>
]

#problem-def("Factoring")[
  Given a composite integer $N$ and bit sizes $m, n$, find integers $p in [2, 2^m - 1]$ and $q in [2, 2^n - 1]$ such that $p times q = N$. Here $p$ has $m$ bits and $q$ has $n$ bits.
][
The hardness of integer factorization underpins RSA cryptography and other public-key systems. Unlike most problems in this collection, Factoring is not known to be NP-complete; it lies in NP $inter$ co-NP, suggesting it may be of intermediate complexity. The best classical algorithm is the General Number Field Sieve @lenstra1993 running in sub-exponential time $e^(O(b^(1 slash 3)(log b)^(2 slash 3)))$ where $b$ is the bit length. Shor's algorithm @shor1994 solves Factoring in polynomial time on a quantum computer.

*Example.* Let $N = 15$ with $m = 2$ bits and $n = 3$ bits, so $p in [2, 3]$ and $q in [2, 7]$. The solution is $p = 3$, $q = 5$, since $3 times 5 = 15 = N$. Note $p = 3$ fits in 2 bits and $q = 5$ fits in 3 bits. The alternative factorization $5 times 3$ requires $m = 3$, $n = 2$.
]

== Specialized Problems

#problem-def("BMF")[
  Given an $m times n$ boolean matrix $A$ and rank $k$, find boolean matrices $B in {0,1}^(m times k)$ and $C in {0,1}^(k times n)$ minimizing the Hamming distance $d_H (A, B circle.tiny C)$, where the boolean product $(B circle.tiny C)_(i j) = or.big_ell (B_(i ell) and C_(ell j))$.
][
Boolean Matrix Factorization decomposes binary data into interpretable boolean factors, unlike real-valued SVD which loses the discrete structure. NP-hard even to approximate, BMF arises in data mining, text classification, and role-based access control where factors correspond to latent binary features. Practical algorithms use greedy rank-1 extraction or alternating fixed-point methods. The best known exact algorithm runs in $O^*(2^(m k + k n))$ by brute-force search over $B$ and $C$#footnote[No algorithm improving on brute-force enumeration is known for general BMF.].

*Example.* Let $A = mat(1, 1, 0; 1, 1, 1; 0, 1, 1)$ and $k = 2$. Set $B = mat(1, 0; 1, 1; 0, 1)$ and $C = mat(1, 1, 0; 0, 1, 1)$. Then $B circle.tiny C = mat(1, 1, 0; 1, 1, 1; 0, 1, 1) = A$, achieving Hamming distance $d_H = 0$ (exact factorization). The two boolean factors capture overlapping row/column patterns: factor 1 selects rows ${1, 2}$ and columns ${1, 2}$; factor 2 selects rows ${2, 3}$ and columns ${2, 3}$.

#figure(
  {
    let cell(val, x, y, color) = {
      let f = if val == 1 { color.transparentize(30%) } else { white }
      box(width: 0.45cm, height: 0.45cm, fill: f, stroke: 0.4pt + luma(180),
        align(center + horizon, text(7pt, if val == 1 { [1] } else { [0] })))
    }
    let mat-grid(data, color) = {
      grid(columns: data.at(0).len(), column-gutter: 0pt, row-gutter: 0pt,
        ..data.flatten().enumerate().map(((i, v)) => {
          cell(v, calc.rem(i, data.at(0).len()), int(i / data.at(0).len()), color)
        }))
    }
    let A = ((1,1,0),(1,1,1),(0,1,1))
    let B = ((1,0),(1,1),(0,1))
    let C = ((1,1,0),(0,1,1))
    set text(8pt)
    align(center, stack(dir: ltr, spacing: 0.3cm,
      [$A =$], mat-grid(A, graph-colors.at(0)),
      [$= B circle.tiny C =$],
      mat-grid(B, graph-colors.at(1)),
      [$circle.tiny$],
      mat-grid(C, rgb("#76b7b2")),
    ))
  },
  caption: [Boolean matrix factorization: $A = B circle.tiny C$ with rank $k = 2$. Factor 1 (red) covers the top-left block; factor 2 (teal) covers the bottom-right block.],
) <fig:bmf>
]

#problem-def("PaintShop")[
  Given a sequence of $2n$ positions where each of $n$ cars appears exactly twice, assign a binary color to each car (each car's two occurrences receive opposite colors) to minimize the number of color changes between consecutive positions.
][
NP-hard and APX-hard @epping2004. Arises in automotive manufacturing where color changes between consecutive cars on an assembly line require costly purging of paint nozzles. Each car appears twice in the sequence (two coats), and each car's two occurrences must receive opposite colors (one per side). A natural benchmark for quantum annealing due to its binary structure and industrial relevance. The best known algorithm runs in $O^*(2^n)$ by brute-force enumeration#footnote[No algorithm improving on brute-force is known for general Paint Shop.].

*Example.* Consider $n = 3$ cars with sequence $(A, B, A, C, B, C)$. Each car gets one occurrence colored 0 and the other colored 1. The assignment $A: 0\/1$, $B: 0\/1$, $C: 1\/0$ yields color sequence $(0, 0, 1, 1, 1, 0)$ with 2 color changes (positions $2 -> 3$ and $5 -> 6$). The alternative $A: 1\/0$, $B: 0\/1$, $C: 0\/1$ yields $(1, 0, 0, 0, 1, 1)$ with 2 changes. The minimum is 2 changes.

#figure(
  {
    let cars = ("A", "B", "A", "C", "B", "C")
    let colors = (0, 0, 1, 1, 1, 0)  // optimal assignment
    let blue = graph-colors.at(0)
    let red = graph-colors.at(1)
    align(center, stack(dir: ltr, spacing: 0pt,
      ..cars.zip(colors).enumerate().map(((i, (car, c))) => {
        let fill = if c == 0 { white } else { blue.transparentize(40%) }
        let change = if i > 0 and colors.at(i) != colors.at(i - 1) {
          place(dx: -0.08cm, dy: 0.55cm, text(6pt, fill: red, weight: "bold")[×])
        }
        stack(dir: ttb, spacing: 0.08cm,
          box(width: 0.55cm, height: 0.55cm, fill: fill, stroke: 0.5pt + luma(120),
            align(center + horizon, text(8pt, weight: "bold", car))),
          text(6pt, fill: luma(100), str(c)),
          change,
        )
      })))
  },
  caption: [Paint Shop: sequence $(A, B, A, C, B, C)$ with optimal coloring. White = color 0, blue = color 1. Two color changes (marked ×) at positions $2 -> 3$ and $5 -> 6$.],
) <fig:paintshop>
]

#problem-def("BicliqueCover")[
  Given a bipartite graph $G = (L, R, E)$ and integer $k$, find $k$ bicliques $(L_1, R_1), dots, (L_k, R_k)$ that cover all edges ($E subset.eq union.big_i L_i times R_i$) while minimizing the total size $sum_i (|L_i| + |R_i|)$.
][
Biclique Cover is equivalent to factoring the biadjacency matrix $M$ of the bipartite graph as a Boolean sum of rank-1 binary matrices, connecting it to Boolean matrix rank and nondeterministic communication complexity. Applications include data compression, database optimization (covering queries with materialized views), and bioinformatics (gene expression biclustering). NP-hard even for fixed $k >= 2$. The best known algorithm runs in $O^*(2^(|L| + |R|))$ by brute-force enumeration#footnote[No algorithm improving on brute-force enumeration is known for general Biclique Cover.].

*Example.* Consider $G = (L, R, E)$ with $L = {ell_1, ell_2}$, $R = {r_1, r_2, r_3}$, and edges $E = {(ell_1, r_1), (ell_1, r_2), (ell_2, r_2), (ell_2, r_3)}$. A biclique cover with $k = 2$: $(L_1, R_1) = ({ell_1}, {r_1, r_2})$ covering edges ${(ell_1, r_1), (ell_1, r_2)}$, and $(L_2, R_2) = ({ell_2}, {r_2, r_3})$ covering ${(ell_2, r_2), (ell_2, r_3)}$. Total size $= (1+2) + (1+2) = 6$. Merging into a single biclique is impossible since $(ell_1, r_3) in.not E$.

#figure(
  canvas(length: 1cm, {
    // Bipartite layout: L on left, R on right
    let lpos = ((0, 1), (0, 0))           // l1, l2
    let rpos = ((2.5, 1.5), (2.5, 0.5), (2.5, -0.5))  // r1, r2, r3
    let edges = ((0, 0), (0, 1), (1, 1), (1, 2))  // (li, rj) pairs
    // Biclique 1: l1-{r1,r2} in blue; Biclique 2: l2-{r2,r3} in teal
    let bc1 = ((0,0), (0,1))
    let bc2 = ((1,1), (1,2))
    for (li, rj) in edges {
      let is-bc1 = bc1.contains((li, rj))
      let c = if is-bc1 { graph-colors.at(0) } else { rgb("#76b7b2") }
      g-edge(lpos.at(li), rpos.at(rj), stroke: 1.5pt + c)
    }
    // L nodes
    for (k, p) in lpos.enumerate() {
      g-node(p, name: "l" + str(k), fill: luma(240), label: $ell_#(k+1)$)
    }
    // R nodes
    for (k, p) in rpos.enumerate() {
      g-node(p, name: "r" + str(k), fill: luma(240), label: $r_#(k+1)$)
    }
  }),
  caption: [Biclique cover of a bipartite graph: biclique 1 (blue) $= ({ell_1}, {r_1, r_2})$, biclique 2 (teal) $= ({ell_2}, {r_2, r_3})$. Edge $(ell_1, r_3)$ is absent, preventing a single biclique.],
) <fig:biclique-cover>
]

#problem-def("BinPacking")[
  Given $n$ items with sizes $s_1, dots, s_n in RR^+$ and bin capacity $C > 0$, find an assignment $x: {1, dots, n} -> NN$ minimizing $|{x(i) : i = 1, dots, n}|$ (the number of distinct bins used) subject to $forall j: sum_(i: x(i) = j) s_i lt.eq C$.
][
  Bin Packing is one of the classical NP-hard optimization problems @garey1979, with applications in logistics, cutting stock, and cloud resource allocation. The best known exact algorithm runs in $O^*(2^n)$ time via inclusion-exclusion over set partitions @bjorklund2009.

  *Example.* Consider $n = 6$ items with sizes $(6, 6, 5, 5, 4, 4)$ and capacity $C = 10$. The lower bound is $ceil(30 slash 10) = 3$ bins. An optimal packing uses exactly 3 bins: $B_1 = {6, 4}$, $B_2 = {6, 4}$, $B_3 = {5, 5}$, each with total load $10 = C$.

  #figure({
    canvas(length: 1cm, {
      let s = 0.28
      let w = 1.0
      let gap = 0.6
      let bins = ((6, 4), (6, 4), (5, 5))
      let fills = (
        (graph-colors.at(0), graph-colors.at(1)),
        (graph-colors.at(0), graph-colors.at(1)),
        (graph-colors.at(2), graph-colors.at(2)),
      )
      for i in range(3) {
        let x = i * (w + gap)
        draw.rect((x, 0), (x + w, 10 * s), stroke: 0.8pt + black)
        let y = 0
        for j in range(bins.at(i).len()) {
          let sz = bins.at(i).at(j)
          let c = fills.at(i).at(j)
          draw.rect((x, y), (x + w, y + sz * s), stroke: 0.4pt, fill: c)
          draw.content((x + w / 2, y + sz * s / 2), text(8pt, fill: white)[#sz])
          y += sz * s
        }
        draw.content((x + w / 2, -0.3), text(8pt)[$B_#(i + 1)$])
      }
      draw.line((-0.15, 10 * s), (2 * (w + gap) + w + 0.15, 10 * s),
        stroke: (dash: "dashed", paint: luma(150), thickness: 0.5pt))
      draw.content((-0.5, 10 * s), text(7pt)[$C$])
    })
  },
  caption: [Optimal packing of items with sizes $(6, 6, 5, 5, 4, 4)$ into 3 bins of capacity $C = 10$. Numbers indicate item sizes; all bins are fully utilized.],
  ) <fig:binpacking-example>
]

// Completeness check: warn about problem types in JSON but missing from paper
#{
  let json-models = {
    let names = graph-data.nodes.map(n => n.name)
    let unique = ()
    for n in names { if n not in unique { unique.push(n) } }
    unique
  }
  let defined = display-name.keys()
  let missing = json-models.filter(n => n not in defined)
  if missing.len() > 0 {
    block(width: 100%, inset: (x: 1em, y: 0.5em), fill: rgb("#fff3cd"), stroke: (left: 3pt + rgb("#ffc107")))[
      #text(fill: rgb("#856404"), weight: "bold")[Warning: Missing problem definitions for:]
      #text(fill: rgb("#856404"))[ #missing.join(", ")]
    ]
  }
}

= Reductions <sec:reductions>

Each reduction is presented as a *Rule* (with linked problem names and overhead from the graph data), followed by a *Proof* (construction, correctness, variable mapping, solution extraction), and optionally a *Concrete Example* (a small instance with verified solution). Problem names in the rule title link back to their definitions in @sec:problems.

== Trivial Reductions

#let mvc_mis = load-example("minimumvertexcover_to_maximumindependentset")
#let mvc_mis_r = load-results("minimumvertexcover_to_maximumindependentset")
#let mvc_mis_sol = mvc_mis_r.solutions.at(0)
#reduction-rule("MinimumVertexCover", "MaximumIndependentSet",
  example: true,
  example-caption: [Petersen graph ($n = 10$): VC $arrow.l.r$ IS],
  extra: [
    Source VC: $C = {#mvc_mis_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #mvc_mis_sol.source_config.filter(x => x == 1).len()) #h(1em)
    Target IS: $S = {#mvc_mis_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #mvc_mis_sol.target_config.filter(x => x == 1).len()) \
    $|"VC"| + |"IS"| = #mvc_mis.source.instance.num_vertices = |V|$ #sym.checkmark
  ],
)[
  Vertex cover and independent set are set complements: removing a cover from $V$ leaves vertices with no edges between them (an independent set), and vice versa. Since $|S| + |C| = |V|$ is constant, maximizing one is equivalent to minimizing the other. The reduction preserves the graph and weights unchanged.
][
  _Construction._ Given VC instance $(G, bold(w))$, create IS instance $(G, bold(w))$ with identical graph and weights. Variables correspond one-to-one: vertex $v$ in the source maps to vertex $v$ in the target.

  _Correctness._ ($arrow.r.double$) If $C$ is a vertex cover, then for any $u, v in V backslash C$, the edge $(u, v) in.not E$ (otherwise $C$ would miss it), so $V backslash C$ is independent. ($arrow.l.double$) If $S$ is independent, then for any $(u, v) in E$, at most one endpoint lies in $S$, so $V backslash S$ covers every edge. Since $|S| + |C| = |V|$ is constant, a minimum vertex cover corresponds to a maximum independent set.

  _Solution extraction._ For IS solution $S$, return $C = V backslash S$, i.e.\ flip each variable: $c_v = 1 - s_v$.
]

#reduction-rule("MaximumIndependentSet", "MinimumVertexCover")[
  The exact reverse of VC $arrow.r$ IS: complementing an independent set yields a vertex cover. The graph and weights are preserved unchanged, and $|"IS"| + |"VC"| = |V|$ ensures optimality carries over.
][
  _Construction._ Given IS instance $(G, bold(w))$, create VC instance $(G, bold(w))$ with identical graph and weights.

  _Correctness._ ($arrow.r.double$) If $S$ is independent, no edge has both endpoints in $S$, so every edge has at least one endpoint in $V backslash S$, making $V backslash S$ a cover. ($arrow.l.double$) If $C$ is a vertex cover, every edge is incident to some vertex in $C$, so no edge connects two vertices of $V backslash C$, making $V backslash C$ independent.

  _Solution extraction._ For VC solution $C$, return $S = V backslash C$, i.e.\ flip each variable: $s_v = 1 - c_v$.
]

#reduction-rule("MaximumIndependentSet", "MaximumSetPacking")[
  The key insight is that two vertices are adjacent if and only if they share an edge. By representing each vertex $v$ as the set of its incident edges $S_v$, adjacency becomes set overlap: $S_u inter S_v != emptyset$ iff $(u,v) in E$. Thus an independent set (no two adjacent) maps exactly to a packing (no two overlapping).
][
  _Construction._ Universe $U = E$ (edges, indexed $0, ..., |E|-1$). For each vertex $v$, define $S_v = {e in E : v in e}$ (the set of edge indices incident to $v$), with weight $w(S_v) = w(v)$. Variables correspond one-to-one: vertex $v$ maps to set $S_v$.

  _Correctness._ ($arrow.r.double$) If $I$ is independent, then for any $u, v in I$, edge $(u,v) in.not E$, so $S_u inter S_v = emptyset$ — the sets are mutually disjoint, forming a valid packing. ($arrow.l.double$) If ${S_v : v in P}$ is a packing, then for any $u, v in P$, $S_u inter S_v = emptyset$, meaning $u$ and $v$ share no edge, so $P$ is independent. Weight sums are identical, so optimality is preserved.

  _Solution extraction._ For packing ${S_v : v in P}$, return IS $= P$ (same variable assignment).
]

#reduction-rule("MaximumSetPacking", "MaximumIndependentSet")[
  The _intersection graph_ captures set overlap as adjacency: two sets that share an element become neighbors, so a packing (mutually disjoint sets) corresponds exactly to an independent set (mutually non-adjacent vertices). This is the standard reduction from set packing to independent set.
][
  _Construction._ Build the intersection graph $G' = (V', E')$: create one vertex $v_i$ per set $S_i$ ($i = 1, ..., m$), and add edge $(v_i, v_j)$ iff $S_i inter S_j != emptyset$. Set $w(v_i) = w(S_i)$. Variables correspond one-to-one: set $S_i$ maps to vertex $v_i$.

  _Correctness._ ($arrow.r.double$) If $cal(P)$ is a packing (all sets mutually disjoint), then for any $S_i, S_j in cal(P)$, $S_i inter S_j = emptyset$, so $(v_i, v_j) in.not E'$, meaning ${v_i : S_i in cal(P)}$ is independent. ($arrow.l.double$) If $I subset.eq V'$ is independent, then for any $v_i, v_j in I$, $(v_i, v_j) in.not E'$, so $S_i inter S_j = emptyset$, meaning ${S_i : v_i in I}$ is a valid packing. Weight sums match, so optimality is preserved.

  _Solution extraction._ For IS $I subset.eq V'$, return packing $cal(P) = {S_i : v_i in I}$ (same variable assignment).
]

#reduction-rule("MinimumVertexCover", "MinimumSetCovering")[
  A vertex cover must "hit" every edge; set covering must "hit" every universe element. By making each edge a universe element and each vertex the set of its incident edges, the two covering conditions become identical. This is the canonical embedding of vertex cover as a special case of set covering.
][
  _Construction._ Universe $U = {0, ..., |E|-1}$ (one element per edge). For each vertex $v$, define $S_v = {i : e_i "incident to" v}$ (the indices of edges touching $v$), with weight $w(S_v) = w(v)$. Variables correspond one-to-one: vertex $v$ maps to set $S_v$.

  _Correctness._ ($arrow.r.double$) If $C$ is a vertex cover, every edge $e_i$ has at least one endpoint $v in C$, so $i in S_v$ for some selected set — hence $union.big_(v in C) S_v = U$, a valid covering. ($arrow.l.double$) If ${S_v : v in C}$ covers $U$, then every edge index $i in U$ appears in some $S_v$ with $v in C$, meaning edge $e_i$ is incident to some $v in C$ — hence $C$ is a vertex cover. Weight sums are identical, so optimality is preserved.

  _Solution extraction._ For covering ${S_v : v in C}$, return VC $= C$ (same variable assignment).
]

#reduction-rule("MaximumMatching", "MaximumSetPacking")[
  A matching selects edges that share no endpoints; set packing selects sets that share no elements. By representing each edge as the 2-element set of its endpoints and using vertices as the universe, two edges conflict (share an endpoint) if and only if their sets overlap. This embeds matching as a special case of set packing where every set has size exactly 2.
][
  _Construction._ Universe $U = V$ (vertices, indexed $0, ..., |V|-1$). For each edge $e = (u, v)$, define $S_e = {u, v}$ with weight $w(S_e) = w(e)$. Variables correspond one-to-one: edge $e$ maps to set $S_e$.

  _Correctness._ ($arrow.r.double$) If $M$ is a matching, then for any $e_1, e_2 in M$, the edges share no endpoint, so $S_(e_1) inter S_(e_2) = emptyset$ — the sets are mutually disjoint, forming a valid packing. ($arrow.l.double$) If ${S_e : e in P}$ is a packing, then for any $e_1, e_2 in P$, $S_(e_1) inter S_(e_2) = emptyset$, meaning the edges share no vertex, so $P$ is a valid matching. Weight sums are identical, so optimality is preserved.

  _Solution extraction._ For packing ${S_e : e in P}$, return matching $= P$ (same variable assignment).
]

#reduction-rule("QUBO", "SpinGlass")[
  QUBO uses binary variables $x_i in {0,1}$; the Ising model uses spin variables $s_i in {-1,+1}$. The affine substitution $x_i = (s_i + 1)\/2$ converts between the two encodings. Since every quadratic binary function maps to a quadratic spin function (and vice versa), the two models are polynomially equivalent. This is the reverse of SpinGlass $arrow.r$ QUBO.
][
  _Construction._ Substitute $x_i = (s_i + 1)\/2$ into $f(bold(x)) = sum_(i <= j) Q_(i j) x_i x_j$. For diagonal terms ($i = j$): $Q_(i i) x_i = Q_(i i)(s_i + 1)\/2$, contributing $Q_(i i)\/2$ to $h_i$. For off-diagonal terms ($i < j$): $Q_(i j) x_i x_j = Q_(i j)(s_i + 1)(s_j + 1)\/4$, contributing $Q_(i j)\/4$ to $J_(i j)$, $Q_(i j)\/4$ to both $h_i$ and $h_j$, plus a constant. Collecting terms:
  $ J_(i j) = Q_(i j) / 4, quad h_i = 1/2 (Q_(i i) + sum_(j != i) Q_(i j) / 2) $

  _Correctness._ ($arrow.r.double$) Any binary assignment $bold(x)$ maps to a spin assignment $bold(s)$ with $s_i = 2 x_i - 1$, and the QUBO objective equals the Ising energy up to a global constant. ($arrow.l.double$) Any spin ground state maps back to a binary minimizer via $x_i = (s_i + 1)\/2$. The constant offset does not affect the argmin.

  _Solution extraction._ Convert spins to binary: $x_i = (s_i + 1) \/ 2$, i.e.\ $s_i = +1 arrow.r x_i = 1$, $s_i = -1 arrow.r x_i = 0$.
]

#let sg_qubo = load-example("spinglass_to_qubo")
#let sg_qubo_r = load-results("spinglass_to_qubo")
#let sg_qubo_sol = sg_qubo_r.solutions.at(0)
#reduction-rule("SpinGlass", "QUBO",
  example: true,
  example-caption: [10-spin Ising model on Petersen graph],
  extra: [
    Source: $n = #sg_qubo.source.instance.num_spins$ spins, $h_i = 0$, couplings $J_(i j) in {plus.minus 1}$ \
    Mapping: $s_i = 2x_i - 1$ converts spins ${-1, +1}$ to binary ${0, 1}$ \
    Ground state ($#sg_qubo_r.solutions.len()$-fold degenerate): $bold(x) = (#sg_qubo_sol.target_config.map(str).join(", "))$ #sym.checkmark
  ],
)[
  The Ising model and QUBO are both quadratic functions over finite domains: spins ${-1,+1}$ and binary variables ${0,1}$, respectively. The affine map $s_i = 2x_i - 1$ establishes a bijection between the two domains and preserves the quadratic structure. Substituting into the Ising Hamiltonian yields a QUBO objective that differs from the original energy by a constant, so ground states correspond exactly.
][
  _Construction._ Substitute $s_i = 2x_i - 1$ into $H = -sum_(i<j) J_(i j) s_i s_j - sum_i h_i s_i$. Expanding:
  $ s_i s_j = (2x_i - 1)(2x_j - 1) = 4x_i x_j - 2x_i - 2x_j + 1 $
  Collecting terms and using $x_i^2 = x_i$:
  $ Q_(i j) = -4 J_(i j) quad (i < j), quad Q_(i i) = 2 sum_(j != i) J_(i j) - 2 h_i $
  The constant offset $-sum_(i<j) J_(i j) + sum_i h_i$ does not affect the minimizer.

  _Correctness._ ($arrow.r.double$) Any spin configuration $bold(s)$ maps to a unique binary vector $bold(x)$ via $x_i = (s_i + 1)\/2$, and $H_"SG"(bold(s)) = H_"QUBO"(bold(x)) + "const"$, so a ground state of the Ising model maps to a QUBO minimizer. ($arrow.l.double$) Any QUBO minimizer $bold(x)$ maps back to spins $s_i = 2x_i - 1$ with the same energy relationship, so optimality is preserved in both directions.

  _Solution extraction._ Convert binary to spins: $s_i = 2x_i - 1$, i.e.\ $x_i = 1 arrow.r s_i = +1$, $x_i = 0 arrow.r s_i = -1$.
]

== Penalty-Method QUBO Reductions <sec:penalty-method>

The _penalty method_ @glover2019 @lucas2014 converts a constrained optimization problem into an unconstrained QUBO by adding quadratic penalty terms. Given an objective $"obj"(bold(x))$ to minimize and constraints $g_k (bold(x)) = 0$, construct:
$ f(bold(x)) = "obj"(bold(x)) + P sum_k g_k (bold(x))^2 $
where $P$ is a penalty weight large enough that any constraint violation costs more than the entire objective range. Since $g_k (bold(x))^2 >= 0$ with equality iff $g_k (bold(x)) = 0$, minimizers of $f$ are feasible and optimal for the original problem. Because binary variables satisfy $x_i^2 = x_i$, the resulting $f$ is a quadratic in $bold(x)$, i.e.\ a QUBO.

#let mis_qubo = load-example("maximumindependentset_to_qubo")
#let mis_qubo_r = load-results("maximumindependentset_to_qubo")
#reduction-rule("MaximumIndependentSet", "QUBO",
  example: true,
  example-caption: [IS on the Petersen graph ($n = 10$) to QUBO],
  extra: [
    *Source edges:* $= {#mis_qubo.source.instance.edges.map(e => $(#e.at(0), #e.at(1))$).join(", ")}$ \
    *QUBO matrix* ($Q in RR^(#mis_qubo.target.instance.num_vars times #mis_qubo.target.instance.num_vars)$):
    $ Q = #math.mat(..mis_qubo.target.instance.matrix.map(row => row.map(v => {
      let r = calc.round(v, digits: 0)
      [#r]
    }))) $
    *Optimal IS* (size #mis_qubo_r.solutions.at(0).source_config.filter(x => x == 1).len()):
    #mis_qubo_r.solutions.map(sol => {
      let verts = sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i))
      $\{#verts.join(", ")\}$
    }).join(", ")
  ],
)[
  An independent set selects vertices with no two adjacent. Each vertex $i$ gets a binary variable $x_i in {0,1}$ indicating selection, and the objective $sum_i w_i x_i$ rewards large sets. The adjacency constraint $x_i x_j = 0$ for each edge is naturally quadratic, so the penalty method directly yields a QUBO: diagonal entries reward vertex selection, while off-diagonal entries penalize adjacent pairs with a weight large enough to make any edge violation costlier than selecting all vertices.
][
  _Construction._ The IS objective is: maximize $sum_i w_i x_i$ subject to $x_i x_j = 0$ for $(i,j) in E$. Applying the penalty method (@sec:penalty-method):
  $ f(bold(x)) = -sum_i w_i x_i + P sum_((i,j) in E) x_i x_j $
  with $P = 1 + sum_i w_i$. Reading off the QUBO coefficients: diagonal $Q_(i i) = -w_i$ (linear reward for selection), off-diagonal $Q_(i j) = P$ for edges $i < j$ (quadratic penalty for adjacency).

  _Correctness._ ($arrow.r.double$) If $bold(x)$ encodes a maximum-weight IS $S^*$, then all penalty terms vanish ($x_i x_j = 0$ for all edges), and $f(bold(x)) = -sum_(i in S^*) w_i$. Any non-IS assignment activates at least one penalty $P > sum_i w_i$, yielding $f > 0 >= f(bold(x))$. ($arrow.l.double$) Among feasible assignments (independent sets), the penalty terms vanish and $f(bold(x)) = -sum_(i in S) w_i$, minimized exactly when $S$ is a maximum-weight IS. Thus QUBO minimizers correspond to maximum-weight independent sets.

  _Solution extraction._ Return $bold(x)$ directly — each $x_i = 1$ indicates vertex $i$ is in the IS.
]

#reduction-rule("MinimumVertexCover", "QUBO")[
  A vertex cover must include at least one endpoint of every edge. The covering constraint for edge $(i,j)$ — that $x_i = x_j = 0$ is forbidden — translates to the quadratic penalty $(1-x_i)(1-x_j)$, which equals 1 exactly when neither endpoint is selected. The penalty method combines the weight-minimization objective with these coverage penalties into a single QUBO, where diagonal entries reflect the trade-off between vertex cost and coverage benefit, and off-diagonal entries penalize uncovered edges.
][
  _Construction._ The VC objective is: minimize $sum_i w_i x_i$ subject to $x_i + x_j >= 1$ for $(i,j) in E$. Applying the penalty method (@sec:penalty-method), the constraint $x_i + x_j >= 1$ is violated iff $x_i = x_j = 0$, with penalty $(1 - x_i)(1 - x_j)$:
  $ f(bold(x)) = sum_i w_i x_i + P sum_((i,j) in E) (1 - x_i)(1 - x_j) $
  with $P = 1 + sum_i w_i$. Expanding: $(1 - x_i)(1 - x_j) = 1 - x_i - x_j + x_i x_j$.
  Summing over all edges, each vertex $i$ appears in $"deg"(i)$ penalty terms. The QUBO coefficients are: diagonal $Q_(i i) = w_i - P dot "deg"(i)$ (objective cost minus linear penalty for coverage), off-diagonal $Q_(i j) = P$ for edges (quadratic penalty). The constant $P |E|$ does not affect the minimizer.

  _Correctness._ ($arrow.r.double$) If $bold(x)$ encodes a minimum vertex cover, every edge has at least one endpoint selected, so all penalty terms $(1-x_i)(1-x_j) = 0$ vanish and $f(bold(x)) = sum_(i in C) w_i$. ($arrow.l.double$) If some edge $(i,j)$ is uncovered ($x_i = x_j = 0$), the penalty $P > sum_i w_i$ exceeds the entire objective range, so $bold(x)$ cannot be a minimizer. Among valid covers (all penalties zero), $f(bold(x)) = sum_(i in C) w_i$ up to a constant, minimized exactly when $C$ is a minimum-weight vertex cover.

  _Solution extraction._ Return $bold(x)$ directly — each $x_i = 1$ indicates vertex $i$ is in the cover.
]

#let kc_qubo = load-example("kcoloring_to_qubo")
#let kc_qubo_r = load-results("kcoloring_to_qubo")
#let kc_qubo_sol = kc_qubo_r.solutions.at(0)
#reduction-rule("KColoring", "QUBO",
  example: true,
  example-caption: [House graph ($n = 5$, $|E| = 6$, $chi = 3$) with $k = 3$ colors],
  extra: [
    #{
      let hg = house-graph()
      let fills = kc_qubo_sol.source_config.map(c => graph-colors.at(c))
      align(center, canvas(length: 0.8cm, {
        for (u, v) in hg.edges { g-edge(hg.vertices.at(u), hg.vertices.at(v)) }
        for (k, pos) in hg.vertices.enumerate() {
          g-node(pos, name: str(k), fill: fills.at(k), label: str(k))
        }
      }))
    }

    *Step 1 -- Encode each color choice as a binary variable.* A coloring assigns each vertex one of $k$ colors. To express this in binary, introduce $k$ indicator variables per vertex: $x_(v,c) = 1$ means "vertex $v$ gets color $c$." For the house graph with $k = 3$, this gives $n k = 5 times 3 = 15$ QUBO variables:
    $ underbrace(x_(0,0) x_(0,1) x_(0,2), "vertex 0") #h(4pt) underbrace(x_(1,0) x_(1,1) x_(1,2), "vertex 1") #h(4pt) dots.c #h(4pt) underbrace(x_(4,0) x_(4,1) x_(4,2), "vertex 4") $

    *Step 2 -- Penalize invalid color assignments (one-hot constraint).* A valid coloring requires each vertex to have _exactly one_ color, i.e.\ $sum_c x_(v,c) = 1$. The penalty $(1 - sum_c x_(v,c))^2$ equals zero when exactly one variable is 1, and is positive otherwise. Weighted by $P_1 = 1 + n = 6$, this contributes diagonal entries $Q_(v k+c, v k+c) = -6$ and off-diagonal entries $Q_(v k+c_1, v k+c_2) = 12$ between colors of the same vertex. These form the $5 times 5$ diagonal blocks of $Q$.\

    *Step 3 -- Penalize same-color neighbors (edge conflict).* For each edge $(u,v) in E$ and each color $c$, the product $x_(u,c) x_(v,c) = 1$ iff both endpoints receive color $c$ — exactly the coloring conflict we want to forbid. The penalty $P_2 dot x_(u,c) x_(v,c)$ with $P_2 = P_1 slash 2 = 3$ makes such conflicts costly. The house has 6 edges, each contributing 3 color-conflict penalties $arrow.r$ 18 off-diagonal entries of value $3$ in $Q$.\

    *Step 4 -- Verify a solution.* The first valid 3-coloring is $(c_0, ..., c_4) = (#kc_qubo_sol.source_config.map(str).join(", "))$, shown in the figure above. The one-hot encoding is $bold(x) = (#kc_qubo_sol.target_config.map(str).join(", "))$. Check: each 3-bit group has exactly one 1 (valid one-hot #sym.checkmark), and for every edge the two endpoints have different colors (e.g.\ edge $0 dash 1$: colors $#kc_qubo_sol.source_config.at(0), #kc_qubo_sol.source_config.at(1)$ #sym.checkmark).\

    *Count:* #kc_qubo_r.solutions.len() valid colorings $= 3! times 3$. The triangle $2 dash 3 dash 4$ forces 3 distinct colors ($3! = 6$ permutations); for each, the base vertices $0, 1$ each have 3 compatible choices but share edge $0 dash 1$, leaving $3$ valid pairs.
  ],
)[
  The $k$-coloring problem has two requirements: each vertex gets exactly one color, and adjacent vertices get different colors. Both can be expressed as quadratic penalties over binary variables. Introduce $n k$ binary variables $x_(v,c) in {0,1}$ (indexed by $v dot k + c$), where $x_(v,c) = 1$ means vertex $v$ receives color $c$. The first requirement becomes a _one-hot constraint_ penalizing vertices with zero or multiple colors; the second becomes an _edge conflict penalty_ penalizing same-color neighbors. The combined QUBO matrix $Q in RR^(n k times n k)$ encodes both penalties.
][
  _Construction._ Applying the penalty method (@sec:penalty-method), the two requirements translate into two penalty terms:
  $ f(bold(x)) = underbrace(P_1 sum_(v in V) (1 - sum_(c=1)^k x_(v,c))^2, "one-hot: exactly one color per vertex") + underbrace(P_2 sum_((u,v) in E) sum_(c=1)^k x_(u,c) x_(v,c), "edge conflict: neighbors differ") $

  _One-hot expansion._ The constraint $(1 - sum_c x_(v,c))^2$ penalizes any vertex with $!= 1$ active color. Expanding using $x_(v,c)^2 = x_(v,c)$ (binary variables):
  $ (1 - sum_c x_(v,c))^2 = 1 - sum_c x_(v,c) + 2 sum_(c_1 < c_2) x_(v,c_1) x_(v,c_2) $
  Reading off the QUBO coefficients: diagonal $Q_(v k+c, v k+c) = -P_1$ (favors assigning a color) and intra-vertex off-diagonal $Q_(v k+c_1, v k+c_2) = 2 P_1$ for $c_1 < c_2$ (discourages multiple colors).

  _Edge conflict._ For each edge $(u,v)$ and color $c$, the product $x_(u,c) x_(v,c)$ equals 1 iff both endpoints share color $c$. The penalty $P_2 x_(u,c) x_(v,c)$ adds $P_2$ to $Q_(u k+c, v k+c)$ (with appropriate index ordering).

  In our implementation, $P_1 = P = 1 + n$ and $P_2 = P\/2$. The penalty $P_1$ exceeds the number of vertices, ensuring that any constraint violation outweighs any objective gain.

  _Correctness._ ($arrow.r.double$) If $bold(x)$ violates any one-hot constraint (some vertex has 0 or $>= 2$ colors), the penalty $P_1 > n$ exceeds the objective range, so $bold(x)$ is not a minimizer. ($arrow.l.double$) Among valid one-hot encodings, $f$ reduces to the edge conflict term, minimized when no two adjacent vertices share a color — exactly the $k$-coloring objective.

  _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$.
]

#reduction-rule("MaximumSetPacking", "QUBO")[
  Set packing selects mutually disjoint sets of maximum total weight. Two sets conflict if and only if they share a universe element — the same adjacency structure as an independent set on the _intersection graph_. This reduction builds the intersection graph implicitly and applies the IS penalty method directly: each set becomes a QUBO variable, diagonal entries reward selection, and off-diagonal entries penalize pairs of overlapping sets with a penalty large enough to forbid any overlap.
][
  _Construction._ Given sets $S_1, ..., S_m$ with weights $w_1, ..., w_m$, introduce binary variables $x_i in {0,1}$ for each set. Two sets $S_i, S_j$ _conflict_ iff $S_i inter S_j != emptyset$. The packing objective is: maximize $sum_i w_i x_i$ subject to $x_i x_j = 0$ for every conflicting pair. Applying the penalty method (@sec:penalty-method):
  $ f(bold(x)) = -sum_i w_i x_i + P sum_(S_i inter S_j != emptyset, thin i < j) x_i x_j $
  with $P = 1 + sum_i w_i$. The QUBO coefficients are: diagonal $Q_(i i) = -w_i$ (reward for selecting set $S_i$), off-diagonal $Q_(i j) = P$ for each conflicting pair $i < j$ (penalty for overlap).

  _Correctness._ ($arrow.r.double$) If $bold(x)$ encodes a maximum-weight packing, all selected sets are mutually disjoint, so all penalty terms vanish and $f(bold(x)) = -sum_(i in cal(P)) w_i$. Any assignment selecting overlapping sets incurs penalty $P > sum_i w_i$, making it suboptimal. ($arrow.l.double$) Among feasible assignments (no overlapping sets selected), the penalty terms vanish and $f(bold(x)) = -sum_(i in cal(P)) w_i$, minimized exactly when $cal(P)$ is a maximum-weight packing.

  _Solution extraction._ Return $bold(x)$ directly — each $x_i = 1$ indicates set $S_i$ is in the packing.
]

#reduction-rule("KSatisfiability", "QUBO")[
  Each clause in a $k$-SAT formula is falsified by exactly one assignment to its literals. For $k = 2$, this falsifying pattern is a product of two (possibly complemented) binary variables — already quadratic, so each clause maps directly to QUBO terms. For $k = 3$, the falsifying pattern $y_1 y_2 y_3$ is cubic; Rosenberg quadratization replaces the product $y_1 y_2$ with an auxiliary variable $a$, enforced by a penalty that makes $a != y_1 y_2$ suboptimal. The total QUBO counts unsatisfied clauses, so minimizers maximize satisfiability.
][
  *Case $k = 2$.*

  _Construction._ Each 2-literal clause has exactly one falsifying assignment (both literals false). The penalty for that assignment is a quadratic function of $x_i, x_j$:

  #table(
    columns: (auto, auto, auto, auto),
    inset: 4pt,
    align: left,
    table.header([*Clause*], [*Falsified when*], [*Penalty*], [*QUBO contributions*]),
    [$x_i or x_j$], [$x_i=0, x_j=0$], [$(1-x_i)(1-x_j)$], [$Q_(i i) -= 1, Q_(j j) -= 1, Q_(i j) += 1$],
    [$overline(x_i) or x_j$], [$x_i=1, x_j=0$], [$x_i(1-x_j)$], [$Q_(i i) += 1, Q_(i j) -= 1$],
    [$x_i or overline(x_j)$], [$x_i=0, x_j=1$], [$(1-x_i)x_j$], [$Q_(j j) += 1, Q_(i j) -= 1$],
    [$overline(x_i) or overline(x_j)$], [$x_i=1, x_j=1$], [$x_i x_j$], [$Q_(i j) += 1$],
  )

  Summing over all clauses, $f(bold(x)) = sum_j "penalty"_j (bold(x))$ counts falsified clauses.

  _Correctness._ ($arrow.r.double$) Each penalty term is non-negative and equals 1 exactly when its clause is falsified. If $bold(x)$ satisfies all clauses, $f(bold(x)) = 0$. ($arrow.l.double$) Any minimizer of $f$ achieves the fewest falsified clauses, hence maximizes satisfiability.

  *Case $k = 3$ (Rosenberg quadratization).*

  _Construction._ For each clause $(ell_1 or ell_2 or ell_3)$, define complement variables $y_i = overline(ell_i)$ (so $y_i = x_i$ if the literal is negated, $y_i = 1 - x_i$ if positive). The clause is violated when $y_1 y_2 y_3 = 1$. This cubic penalty is reduced to quadratic form by introducing an auxiliary variable $a$ and the substitution $a = y_1 y_2$, enforced via a Rosenberg penalty with weight $M$:
  $ H = a dot y_3 + M (y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a) $
  where $M = 2$ suffices. Each clause adds one auxiliary variable (indices $n, n+1, ..., n+m-1$), so the total QUBO has $n + m$ variables.

  _Correctness._ ($arrow.r.double$) If $a = y_1 y_2$, the Rosenberg penalty term vanishes and $H = y_1 y_2 y_3$ counts the clause violation faithfully. ($arrow.l.double$) If $a != y_1 y_2$, the penalty $M(dots.c) >= 1$ strictly exceeds the clause-counting contribution (at most 1), so any minimizer must have $a = y_1 y_2$ for every clause. Among such assignments, $H$ counts unsatisfied clauses, and minimizers maximize satisfiability.

  _Solution extraction._ Discard auxiliary variables: return $bold(x)[0..n]$.
]

#reduction-rule("ILP", "QUBO")[
  A binary ILP optimizes a linear objective over binary variables subject to linear constraints. The penalty method converts each equality constraint $bold(a)_k^top bold(x) = b_k$ into the quadratic penalty $(bold(a)_k^top bold(x) - b_k)^2$, which is zero if and only if the constraint is satisfied. Inequality constraints are first converted to equalities using binary slack variables with powers-of-two coefficients. The resulting unconstrained quadratic over binary variables is a QUBO whose matrix $Q$ combines the negated objective (as diagonal terms) with the expanded constraint penalties (as a Gram matrix $A^top A$).
][
  _Construction._ First, normalize all constraints to equalities. Inequalities $bold(a)_k^top bold(x) <= b_k$ become $bold(a)_k^top bold(x) + sum_(s=0)^(S_k - 1) 2^s y_(k,s) = b_k$ where $S_k = ceil(log_2 (b_k + 1))$ binary slack bits. For $>=$ constraints, the slack has a negative sign. The extended system is $A' bold(x)' = bold(b)$ with $bold(x)' = (bold(x), bold(y)) in {0,1}^(n')$. For minimization, negate $bold(c)$ to convert to maximization.

  Applying the penalty method (@sec:penalty-method), combine the negated objective with quadratic constraint penalties:
  $ f(bold(x)') = -bold(c')^top bold(x)' + P sum_(k=1)^m (bold(a)'_k^(top) bold(x)' - b_k)^2 $
  where $bold(c)' = (bold(c), bold(0))$ and $P = 1 + ||bold(c)||_1 + ||bold(b)||_1$. Expanding the quadratic penalty:
  $ sum_k (bold(a)'_k^(top) bold(x)' - b_k)^2 = bold(x)'^(top) A'^(top) A' bold(x)' - 2 bold(b)^top A' bold(x)' + ||bold(b)||_2^2 $
  Combining with $-bold(c')^top bold(x)'$ and dropping the constant $||bold(b)||_2^2$:
  $ Q = -"diag"(bold(c)' + 2P bold(b)^top A') + P A'^(top) A' $
  The diagonal contains linear terms (objective plus constraint); the upper triangle of $A'^(top) A'$ gives quadratic cross-terms.

  _Correctness._ ($arrow.r.double$) If $bold(x)'^*$ is an optimal ILP solution, then $A' bold(x)'^* = bold(b)$ and all penalty terms vanish, so $f(bold(x)'^*) = -bold(c')^top bold(x)'^*$. ($arrow.l.double$) If any constraint is violated, $(bold(a)'_k^(top) bold(x)' - b_k)^2 >= 1$ and the penalty $P > ||bold(c)||_1$ exceeds the entire objective range, so $bold(x)'$ cannot be a QUBO minimizer. Among feasible assignments (all penalties zero), $f$ reduces to $-bold(c')^top bold(x)'$, minimized at the ILP optimum.

  _Solution extraction._ Discard slack variables: return $bold(x)' [0..n]$.
]

#let qubo_ilp = load-example("qubo_to_ilp")
#let qubo_ilp_r = load-results("qubo_to_ilp")
#let qubo_ilp_sol = qubo_ilp_r.solutions.at(0)
#reduction-rule("QUBO", "ILP",
  example: true,
  example-caption: [4-variable QUBO with 3 quadratic terms],
  extra: [
    Source: $n = #qubo_ilp.source.instance.num_vars$ binary variables, 3 off-diagonal terms \
    Target: #qubo_ilp.target.instance.num_vars ILP variables ($#qubo_ilp.source.instance.num_vars$ original $+ #(qubo_ilp.target.instance.num_vars - qubo_ilp.source.instance.num_vars)$ auxiliary), 9 McCormick constraints \
    Optimal: $bold(x) = (#qubo_ilp_sol.source_config.map(str).join(", "))$ ($#qubo_ilp_r.solutions.len()$-fold degenerate) #sym.checkmark
  ],
)[
  QUBO minimizes a quadratic form $bold(x)^top Q bold(x)$ over binary variables. Every quadratic term $Q_(i j) x_i x_j$ can be _linearized_ by introducing an auxiliary variable $y_(i j)$ constrained to equal the product $x_i x_j$ via three McCormick inequalities. Diagonal terms $Q_(i i) x_i^2 = Q_(i i) x_i$ are already linear for binary $x_i$. The result is a binary ILP with a linear objective and $3 m$ constraints (where $m$ is the number of non-zero off-diagonal entries), whose minimizer corresponds exactly to the QUBO minimizer.
][
  _Construction._ For $Q in RR^(n times n)$ (upper triangular) with $m$ non-zero off-diagonal entries:

  _Diagonal terms._ For binary $x_i$: $Q_(i i) x_i^2 = Q_(i i) x_i$, which is directly linear.

  _Off-diagonal terms._ For each non-zero $Q_(i j)$ ($i < j$), introduce binary $y_(i j) = x_i dot x_j$ with McCormick constraints:
  $ y_(i j) <= x_i, quad y_(i j) <= x_j, quad y_(i j) >= x_i + x_j - 1 $

  _ILP formulation._ Minimize $sum_i Q_(i i) x_i + sum_(i < j) Q_(i j) y_(i j)$ subject to the McCormick constraints and $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.

  _Solution extraction._ Return the first $n$ variables (discard auxiliary $y_(i j)$).
]

#let cs_ilp = load-example("circuitsat_to_ilp")
#let cs_ilp_r = load-results("circuitsat_to_ilp")
#reduction-rule("CircuitSAT", "ILP",
  example: true,
  example-caption: [1-bit full adder to ILP],
  extra: [
    Circuit: #cs_ilp.source.instance.num_gates gates (2 XOR, 2 AND, 1 OR), #cs_ilp.source.instance.num_variables variables \
    Target: #cs_ilp.target.instance.num_vars ILP variables (circuit vars $+$ auxiliary), trivial objective \
    #cs_ilp_r.solutions.len() feasible solutions ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
  ],
)[
  Each boolean gate (AND, OR, NOT, XOR) has a truth table that can be captured exactly by a small set of linear inequalities over binary variables. By Tseitin-style flattening, each internal expression node gets an auxiliary ILP variable constrained to match its gate's output, so the conjunction of all gate constraints is feasible if and only if the circuit is satisfiable. The ILP has a trivial objective (minimize 0), making it a pure feasibility problem.
][
  _Construction._ Recursively assign an ILP variable to each expression node. Named circuit variables keep their identity; internal nodes get auxiliary variables.

  _Gate encodings_ (output $c$, inputs $a_1, ..., a_k$, all binary):
  - NOT: $c + a = 1$
  - AND: $c <= a_i$ ($forall i$), $c >= sum a_i - (k - 1)$
  - OR: $c >= a_i$ ($forall i$), $c <= sum a_i$
  - XOR (binary, chained pairwise): $c <= a + b$, $c >= a - b$, $c >= b - a$, $c <= 2 - a - b$

  _Objective._ Minimize $0$ (feasibility problem): any feasible solution satisfies the circuit.

  _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.

  _Solution extraction._ Return values of the named circuit variables.
]

== Non-Trivial Reductions

#let sat_mis = load-example("satisfiability_to_maximumindependentset")
#let sat_mis_r = load-results("satisfiability_to_maximumindependentset")
#let sat_mis_sol = sat_mis_r.solutions.at(0)
#reduction-rule("Satisfiability", "MaximumIndependentSet",
  example: true,
  example-caption: [3-SAT with 5 variables and 7 clauses],
  extra: [
    SAT assignment: $(x_1, ..., x_5) = (#sat_mis_sol.source_config.map(str).join(", "))$ \
    IS graph: #sat_mis.target.instance.num_vertices vertices ($= 3 times #sat_mis.source.instance.num_clauses$ literals), #sat_mis.target.instance.num_edges edges \
    IS of size #sat_mis.source.instance.num_clauses $= m$: one vertex per clause $arrow.r$ satisfying assignment #sym.checkmark
  ],
)[
  @karp1972 A satisfying assignment must make at least one literal true in every clause, and different clauses cannot assign contradictory values to the same variable. These two requirements map naturally to an independent set problem: _intra-clause cliques_ force exactly one literal per clause to be selected, while _conflict edges_ between complementary literals across clauses enforce consistency. The target IS size equals the number of clauses $m$, so an IS of size $m$ exists iff the formula is satisfiable.
][
  _Construction._ For $phi = and.big_(j=1)^m C_j$ with $C_j = (ell_(j,1) or ... or ell_(j,k_j))$:

  _Vertices:_ For each literal $ell_(j,i)$ in clause $C_j$, create $v_(j,i)$. Total: $|V| = sum_j k_j$.

  _Edges:_ (1) Intra-clause cliques: $E_"clause" = {(v_(j,i), v_(j,i')) : i != i'}$. (2) Conflict edges: $E_"conflict" = {(v_(j,i), v_(j',i')) : j != j', ell_(j,i) = overline(ell_(j',i'))}$.

  _Correctness._ ($arrow.r.double$) A satisfying assignment selects one true literal per clause; these vertices form an IS of size $m$ (no clause edges by selection, no conflict edges by consistency). ($arrow.l.double$) An IS of size $m$ must contain exactly one vertex per clause (by clause cliques); the corresponding literals are consistent (by conflict edges) and satisfy $phi$.

  _Solution extraction._ For $v_(j,i) in S$ with literal $x_k$: set $x_k = 1$; for $overline(x_k)$: set $x_k = 0$.
]

#let sat_kc = load-example("satisfiability_to_kcoloring")
#let sat_kc_r = load-results("satisfiability_to_kcoloring")
#let sat_kc_sol = sat_kc_r.solutions.at(0)
#reduction-rule("Satisfiability", "KColoring",
  example: true,
  example-caption: [5-variable SAT with 3 unit clauses to 3-coloring],
  extra: [
    SAT assignment: $(x_1, ..., x_5) = (#sat_kc_sol.source_config.map(str).join(", "))$ \
    Construction: 3 base + $2 times #sat_kc.source.instance.num_vars$ variable gadgets + OR-gadgets $arrow.r$ #sat_kc.target.instance.num_vertices vertices, #sat_kc.target.instance.num_edges edges \
    #sat_kc_r.solutions.len() valid 3-colorings (color symmetry of satisfying assignments) #sym.checkmark
  ],
)[
  @garey1979 A 3-coloring partitions vertices into three classes. The key insight is that three colors suffice to encode Boolean logic: one color represents TRUE, one FALSE, and a third (AUX) serves as a neutral ground. Variable gadgets force each variable's positive and negative literals to receive opposite truth colors, while clause gadgets use an OR-chain that can only receive the TRUE color when at least one input literal is TRUE-colored. Connecting the output of each clause gadget to the FALSE vertex forces it to be TRUE-colored, encoding the requirement that every clause is satisfied.
][
  _Construction._ (1) _Base triangle:_ vertices TRUE, FALSE, AUX, all mutually connected. This fixes three distinct colors and establishes the color semantics. (2) _Variable gadget_ for $x_i$: vertices $"pos"_i$, $"neg"_i$ connected to each other and to AUX. Since $"pos"_i$ and $"neg"_i$ are both adjacent to AUX, neither can receive the AUX color; since they are adjacent to each other, one must be TRUE-colored and the other FALSE-colored. (3) _Clause gadget_ for $(ell_1 or dots or ell_k)$: apply OR-gadgets iteratively --- $o_1 = "OR"(ell_1, ell_2)$, $o_2 = "OR"(o_1, ell_3)$, etc. --- producing final output $o$, then connect $o$ to both FALSE and AUX.

  _OR-gadget$(a, b) arrow.bar o$:_ Introduces five auxiliary vertices with edges arranged so that $o$ can receive the TRUE color iff at least one of $a$, $b$ has the TRUE color. When both inputs have the FALSE color, the gadget's internal constraints force $o$ into the AUX color.

  _Correctness._ ($arrow.r.double$) A satisfying assignment colors $"pos"_i$ as TRUE when $x_i = 1$ and FALSE otherwise. Each clause has at least one TRUE literal, so the OR-chain output receives the TRUE color, which is compatible with edges to FALSE and AUX. ($arrow.l.double$) In any valid 3-coloring, the variable gadgets assign consistent truth values and the clause gadget connections to FALSE force each clause output to be TRUE-colored, meaning at least one literal per clause is TRUE.

  _Solution extraction._ Set $x_i = 1$ iff $"color"("pos"_i) = "color"("TRUE")$.
]

#let sat_ds = load-example("satisfiability_to_minimumdominatingset")
#let sat_ds_r = load-results("satisfiability_to_minimumdominatingset")
#let sat_ds_sol = sat_ds_r.solutions.at(0)
#reduction-rule("Satisfiability", "MinimumDominatingSet",
  example: true,
  example-caption: [5-variable 7-clause 3-SAT to dominating set],
  extra: [
    SAT assignment: $(x_1, ..., x_5) = (#sat_ds_sol.source_config.map(str).join(", "))$ \
    Vertex structure: $#sat_ds.target.instance.num_vertices = 3 times #sat_ds.source.instance.num_vars + #sat_ds.source.instance.num_clauses$ (variable triangles + clause vertices) \
    Dominating set of size $n = #sat_ds.source.instance.num_vars$: one vertex per variable triangle #sym.checkmark
  ],
)[
  @garey1979 Each variable is represented by a triangle whose three vertices correspond to the positive literal, negative literal, and a dummy. Any dominating set must include at least one vertex from each triangle to dominate the dummy. The clause vertices are connected only to the literal vertices that appear in the clause, so a dominating set of minimum size $n$ (one vertex per triangle) dominates all clause vertices iff the chosen literals satisfy every clause.
][
  _Construction._ (1) _Variable triangle_ for $x_i$: vertices $"pos"_i = 3i$, $"neg"_i = 3i+1$, $"dum"_i = 3i+2$ forming a triangle. The dummy vertex $"dum"_i$ is adjacent only to $"pos"_i$ and $"neg"_i$, so it can only be dominated by a vertex from its own triangle. (2) _Clause vertex_ $c_j = 3n+j$ connected to $"pos"_i$ if $x_i in C_j$, to $"neg"_i$ if $overline(x_i) in C_j$.

  _Correctness._ ($arrow.r.double$) Given a satisfying assignment, select $"pos"_i$ if $x_i = 1$, else $"neg"_i$. This dominates all triangle vertices (each triangle has one selected vertex adjacent to both others). Each clause $C_j$ has at least one true literal, so $c_j$ is adjacent to at least one selected vertex. Total size: $n$. ($arrow.l.double$) Any dominating set needs $>= 1$ vertex per triangle (to dominate $"dum"_i$). A set of size $n$ has exactly one per triangle. If $"dum"_i$ is selected, it does not dominate any clause vertex; but it does dominate $"pos"_i$ and $"neg"_i$, which still need to cover clauses. Since $"dum"_i$ has no clause neighbors, we can swap it for $"pos"_i$ or $"neg"_i$ without losing domination of the triangle. After swapping, each clause vertex $c_j$ must be dominated by some $"pos"_i$ or $"neg"_i$, defining a consistent satisfying assignment.

  _Solution extraction._ Set $x_i = 1$ if $"pos"_i$ selected; $x_i = 0$ if $"neg"_i$ selected.
]

#reduction-rule("KSatisfiability", "Satisfiability")[
  Every $k$-SAT instance is already a SAT instance --- clauses happen to have exactly $k$ literals, but SAT places no restriction on clause width. The embedding is the identity.
][
  _Construction._ Variables and clauses are unchanged.

  _Correctness._ ($arrow.r.double$) Any $k$-SAT satisfying assignment satisfies the same clauses under SAT. ($arrow.l.double$) Any SAT satisfying assignment satisfies the same clauses (which all have width $k$). _Solution extraction._ Identity.
]

#let sat_ksat = load-example("satisfiability_to_ksatisfiability")
#let sat_ksat_r = load-results("satisfiability_to_ksatisfiability")
#let sat_ksat_sol = sat_ksat_r.solutions.at(0)
#reduction-rule("Satisfiability", "KSatisfiability",
  example: true,
  example-caption: [Mixed-size clauses (sizes 1 to 5) to 3-SAT],
  extra: [
    Source: #sat_ksat.source.instance.num_vars variables, #sat_ksat.source.instance.num_clauses clauses (sizes 1, 2, 3, 3, 4, 5) \
    Target 3-SAT: $#sat_ksat.target.instance.num_vars = #sat_ksat.source.instance.num_vars + 7$ variables, #sat_ksat.target.instance.num_clauses clauses (small padded, large split) \
    First solution: $(x_1, ..., x_5) = (#sat_ksat_sol.source_config.map(str).join(", "))$, auxiliary vars are don't-cares #sym.checkmark
  ],
)[
  @cook1971 @garey1979 Clauses shorter than $k$ can be padded with a complementary pair $y, overline(y)$ that is always satisfiable; clauses longer than $k$ can be split into a chain of width-$k$ clauses linked by auxiliary variables that propagate truth values. Both transformations preserve satisfiability while enforcing uniform clause width.
][
  _Construction._

  _Small clauses ($|C| < k$):_ Pad $(ell_1 or dots or ell_r)$ with fresh auxiliary $y$: $(ell_1 or dots or ell_r or y or overline(y) or dots)$ to length $k$. The pair $y, overline(y)$ is a tautology, so the padded clause is satisfiable iff the original is.

  _Large clauses ($|C| > k$):_ Split $(ell_1 or dots or ell_r)$ with auxiliaries $y_1, dots, y_(r-k)$:
  $ (ell_1 or dots or ell_(k-1) or y_1) and (overline(y_1) or ell_k or dots or y_2) and dots and (overline(y_(r-k)) or ell_(r-k+2) or dots or ell_r) $

  _Correctness._ ($arrow.r.double$) If the original clause is satisfied by some literal $ell_j$, set the auxiliary chain so that $y_i = 1$ for all $i$ before $ell_j$'s sub-clause and $y_i = 0$ after. Each sub-clause then contains either a true original literal or a true auxiliary. ($arrow.l.double$) If all sub-clauses are satisfied but every original literal is false, the first clause forces $y_1 = 1$, which forces $y_2 = 1$ (since $overline(y_1)$ is false), and so on until the last clause has $overline(y_(r-k)) = 0$ and all remaining literals false --- a contradiction.

  _Solution extraction._ Discard auxiliary variables; return original variable assignments.
]

#reduction-rule("Satisfiability", "CircuitSAT",
  example: true,
  example-caption: [3-variable SAT formula to boolean circuit],
)[
  CNF is inherently an AND-of-ORs structure, which maps directly to a boolean circuit: each clause becomes an OR gate over its literals, and a final AND gate combines all clause outputs. The circuit is constrained to output _true_, so a satisfying circuit assignment exists iff the original formula is satisfiable.
][
  _Construction._ For $phi = C_1 and dots and C_k$ with $C_i = (ell_(i 1) or dots or ell_(i m_i))$: (1) Create circuit inputs $x_1, dots, x_n$ corresponding to SAT variables. (2) For each clause $C_i$, add an OR gate $g_i$ with inputs from the clause's literals (negated inputs use NOT gates). (3) Add a final AND gate with inputs $g_1, dots, g_k$, constrained to output _true_.

  _Correctness._ ($arrow.r.double$) A satisfying assignment makes at least one literal true in each clause, so each OR gate outputs true and the AND gate outputs true. ($arrow.l.double$) A satisfying circuit assignment has all OR gates true (forced by the AND output constraint), meaning at least one literal per clause is true --- exactly a SAT solution.

  _Solution extraction._ Return the values of the circuit input variables $x_1, dots, x_n$.
]

#let cs_sg = load-example("circuitsat_to_spinglass")
#let cs_sg_r = load-results("circuitsat_to_spinglass")
#reduction-rule("CircuitSAT", "SpinGlass",
  example: true,
  example-caption: [1-bit full adder to Ising model],
  extra: [
    Circuit: #cs_sg.source.instance.num_gates gates (2 XOR, 2 AND, 1 OR), #cs_sg.source.instance.num_variables variables \
    Target: #cs_sg.target.instance.num_spins spins (each gate allocates I/O + auxiliary spins) \
    #cs_sg_r.solutions.len() ground states ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
  ],
)[
  @whitfield2012 @lucas2014 Each logic gate can be represented as an Ising gadget --- a small set of spins with couplings $J_(i j)$ and fields $h_i$ chosen so that the gadget's ground states correspond exactly to the gate's truth table rows. Composing gadgets for all gates in the circuit yields a spin glass whose ground states encode precisely the satisfying assignments of the circuit. The energy gap between valid and invalid I/O patterns ensures that any global ground state respects every gate's logic.
][
  _Construction._

  _Spin mapping:_ Boolean variables $sigma in {0,1}$ map to Ising spins $s = 2sigma - 1 in {-1, +1}$. Each circuit variable is assigned a unique spin index; gate gadgets reference these indices for their inputs and outputs.

  _Gate gadgets_ (inputs 0,1; output 2; auxiliary 3 for XOR) are listed in @tab:gadgets. For each gate, instantiate the gadget's couplings and fields. The total Hamiltonian is the sum over all gadgets: $H = -sum_(i < j) J_(i j) s_i s_j - sum_i h_i s_i$.

  _Correctness._ ($arrow.r.double$) A satisfying circuit assignment maps to a spin configuration where every gadget is in a ground state (valid I/O), so the total energy is minimized. ($arrow.l.double$) Any global ground state must minimize each gadget's contribution. Since each gadget's ground states match its gate's truth table, the spin configuration encodes a valid circuit evaluation. The output spin is constrained to $+1$ (true), so the circuit is satisfied.

  _Solution extraction._ Map spins back to Boolean: $sigma_i = (s_i + 1) / 2$. Return the circuit input variables.
]

#figure(
  table(
    columns: (auto, auto, auto),
    inset: 4pt,
    align: left,
    table.header([*Gate*], [*Couplings $J$*], [*Fields $h$*]),
    [AND], [$J_(01)=1, J_(02)=J_(12)=-2$], [$h_0=h_1=-1, h_2=2$],
    [OR], [$J_(01)=1, J_(02)=J_(12)=-2$], [$h_0=h_1=1, h_2=-2$],
    [NOT], [$J_(01)=1$], [$h_0=h_1=0$],
    [XOR], [$J_(01)=1, J_(02)=J_(12)=-1, J_(03)=J_(13)=-2, J_(23)=2$], [$h_0=h_1=-1, h_2=1, h_3=2$],
  ),
  caption: [Ising gadgets for logic gates. Ground states match truth tables.]
) <tab:gadgets>

#let fact_cs = load-example("factoring_to_circuitsat")
#let fact_cs_r = load-results("factoring_to_circuitsat")
#let fact-decode(config, start, count) = {
  let pow2 = (1, 2, 4, 8, 16, 32)
  range(count).fold(0, (acc, i) => acc + config.at(start + i) * pow2.at(i))
}
#let fact-nbf = fact_cs.source.instance.num_bits_first
#let fact-nbs = fact_cs.source.instance.num_bits_second
#reduction-rule("Factoring", "CircuitSAT",
  example: true,
  example-caption: [Factor $N = #fact_cs.source.instance.number$],
  extra: [
    Circuit: $#fact-nbf times #fact-nbs$ array multiplier with #fact_cs.target.instance.num_gates gates, #fact_cs.target.instance.num_variables variables \
    #fact_cs_r.solutions.len() solutions: #fact_cs_r.solutions.map(sol => {
      let p = fact-decode(sol.source_config, 0, fact-nbf)
      let q = fact-decode(sol.source_config, fact-nbf, fact-nbs)
      $#p times #q = #fact_cs.source.instance.number$
    }).join(" and ") #sym.checkmark
  ],
)[
  Integer multiplication can be implemented as a boolean circuit: an $m times n$ array multiplier computes $p times q$ using only AND, XOR, and OR gates arranged in a grid of full adders. Constraining the output bits to match $N$ turns the circuit into a satisfiability problem --- the circuit is satisfiable iff $N = p times q$ for some $p, q$ within the given bit widths. _(Folklore; no canonical reference.)_
][
  _Construction._ Build $m times n$ array multiplier for $p times q$:

  _Full adder $(i,j)$:_ Each cell computes one partial product bit $p_i and q_j$ and adds it to the running sum from previous cells. The sum and carry are: $s_(i,j) + 2c_(i,j) = (p_i and q_j) + s_"prev" + c_"prev"$, implemented via:
  $ a := p_i and q_j, quad t_1 := a xor s_"prev", quad s_(i,j) := t_1 xor c_"prev" $
  $ t_2 := t_1 and c_"prev", quad t_3 := a and s_"prev", quad c_(i,j) := t_2 or t_3 $

  _Output constraint:_ Fix output wires to the binary representation of $N$: $M_k := "bit"_k(N)$ for $k = 1, dots, m+n$.

  _Correctness._ ($arrow.r.double$) If $N = p times q$ with $p < 2^m$ and $q < 2^n$, setting the input bits to the binary representations of $p$ and $q$ produces output bits matching $N$, satisfying all constraints. ($arrow.l.double$) Any satisfying assignment to the circuit computes a valid multiplication (the gates enforce arithmetic correctness), and the output constraint ensures the product equals $N$.

  _Solution extraction._ Read off factor bits: $p = sum_i p_i 2^(i-1)$, $q = sum_j q_j 2^(j-1)$.
]

#let mc_sg = load-example("maxcut_to_spinglass")
#let mc_sg_r = load-results("maxcut_to_spinglass")
#let mc_sg_sol = mc_sg_r.solutions.at(0)
#let mc_sg_cut = mc_sg.source.instance.edges.filter(e => mc_sg_sol.source_config.at(e.at(0)) != mc_sg_sol.source_config.at(e.at(1))).len()
#reduction-rule("MaxCut", "SpinGlass",
  example: true,
  example-caption: [Petersen graph ($n = 10$, unit weights) to Ising],
  extra: [
    Direct 1:1 mapping: vertices $arrow.r$ spins, $J_(i j) = w_(i j) = 1$, $h_i = 0$ \
    Partition: $S = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ vs $overline(S) = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => str(i)).join(", ")}$ \
    Cut value $= #mc_sg_cut$ ($#mc_sg_r.solutions.len()$-fold degenerate) #sym.checkmark
  ],
)[
  @barahona1982 A maximum cut partitions vertices into two groups to maximize the total weight of edges crossing the partition. In the Ising model, two spins with opposite signs contribute $-J_(i j) s_i s_j = J_(i j)$ to the energy, while same-sign spins contribute $-J_(i j)$. Setting $J_(i j) = w_(i j)$ and $h_i = 0$ makes each cut edge lower the energy by $2 J_(i j)$ relative to an uncut edge, so the Ising ground state corresponds to the maximum cut.
][
  _Construction._ Map each vertex to a spin with $J_(i j) = w_(i j)$ for each edge and $h_i = 0$ (no external field). Spins are $s_i = 2 sigma_i - 1$ where $sigma_i in {0, 1}$ is the partition label.

  _Correctness._ ($arrow.r.double$) A maximum cut assigns $sigma_i in {0,1}$. For cut edges, $s_i s_j = -1$, contributing $-J_(i j)(-1) = +J_(i j)$. For uncut edges, $s_i s_j = +1$, contributing $-J_(i j)$. Maximizing cut weight is equivalent to minimizing $-sum J_(i j) s_i s_j$, the Ising energy. ($arrow.l.double$) An Ising ground state minimizes $-sum J_(i j) s_i s_j$, which is maximized when opposite-sign pairs (cut edges) have the largest possible weights --- exactly the maximum cut.

  _Solution extraction._ Partition $= {i : s_i = +1}$.
]

#let sg_mc = load-example("spinglass_to_maxcut")
#let sg_mc_r = load-results("spinglass_to_maxcut")
#let sg_mc_sol = sg_mc_r.solutions.at(0)
#reduction-rule("SpinGlass", "MaxCut",
  example: true,
  example-caption: [10-spin Ising with alternating $J_(i j) in {plus.minus 1}$],
  extra: [
    All $h_i = 0$: no ancilla needed, direct 1:1 vertex mapping \
    Edge weights $w_(i j) = J_(i j) in {plus.minus 1}$ (alternating couplings) \
    Ground state ($#sg_mc_r.solutions.len()$-fold degenerate): partition $S = {#sg_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ #sym.checkmark
  ],
)[
  @barahona1982 @lucas2014 The Ising Hamiltonian $H = -sum J_(i j) s_i s_j - sum h_i s_i$ has two types of terms. The pairwise couplings $J_(i j)$ map directly to MaxCut edge weights, since minimizing $-J_(i j) s_i s_j$ favors opposite spins (cut edges) when $J_(i j) > 0$. The local fields $h_i$ have no direct MaxCut analogue, but can be absorbed by introducing a single ancilla vertex connected to every spin with weight $h_i$: fixing the ancilla's partition side effectively creates a linear bias on each spin.
][
  _Construction._ If all $h_i = 0$: set $w_(i j) = J_(i j)$ directly (1:1 mapping, no ancilla). If some $h_i != 0$: add ancilla vertex $a$ with edges $w_(i,a) = h_i$ for each spin $i$. The Ising energy $-sum J_(i j) s_i s_j - sum h_i s_i$ equals $-sum J_(i j) s_i s_j - sum h_i s_i s_a$ when $s_a = +1$, which is a pure pairwise Hamiltonian on $n + 1$ spins.

  _Correctness._ ($arrow.r.double$) An Ising ground state assigns spins to minimize $H$. The equivalent MaxCut graph has the same objective (up to a constant), so the spin configuration defines a maximum cut. ($arrow.l.double$) A maximum cut on the constructed graph maximizes $sum_("cut") w_(i j)$, which corresponds to minimizing $-sum J_(i j) s_i s_j - sum h_i s_i s_a$. With $s_a$ fixed, this is the Ising energy, so the cut defines a ground state.

  _Solution extraction._ Without ancilla: partition labels are the spin values directly. With ancilla: if $sigma_a = 1$ (ancilla on the $+1$ side), the spin values are read directly; if $sigma_a = 0$, flip all spins before reading (since the ancilla should represent $s_a = +1$).
]

#reduction-rule("KColoring", "ILP")[
  A $k$-coloring assigns each vertex exactly one of $k$ colors such that adjacent vertices differ. Both requirements are naturally linear: the "exactly one color" condition is an equality constraint on $k$ binary indicators per vertex, and the "neighbors differ" condition bounds each color's indicator sum to at most one per edge. The resulting ILP has $|V| k$ variables and $|V| + |E| k$ constraints with a trivial objective.
][
  _Construction._ For graph $G = (V, E)$ with $k$ colors:

  _Variables:_ Binary $x_(v,c) in {0, 1}$ for each vertex $v in V$ and color $c in {1, ..., k}$. Interpretation: $x_(v,c) = 1$ iff vertex $v$ has color $c$.

  _Constraints:_ (1) Each vertex has exactly one color: $sum_(c=1)^k x_(v,c) = 1$ for all $v in V$. (2) Adjacent vertices have different colors: $x_(u,c) + x_(v,c) <= 1$ for all $(u, v) in E$ and $c in {1, ..., k}$.

  _Objective:_ Feasibility problem (minimize 0).

  _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.

  _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$; assign color $c$ to $v$.
]

#reduction-rule("Factoring", "ILP")[
  Integer multiplication $p times q = N$ is a system of bilinear equations over binary factor bits with carry propagation. Each bit-product $p_i q_j$ is a bilinear term that McCormick linearization replaces with an auxiliary variable and three inequalities. The carry-chain equations are already linear, so the full system becomes a binary ILP with $O(m n)$ variables and constraints.
][
  _Construction._ For target $N$ with $m$-bit factor $p$ and $n$-bit factor $q$:

  _Variables:_ Binary $p_i, q_j in {0,1}$ for factor bits; binary $z_(i j) in {0,1}$ for products $p_i dot q_j$; integer $c_k >= 0$ for carries at each bit position.

  _Product linearization (McCormick):_ For each $z_(i j) = p_i dot q_j$:
  $ z_(i j) <= p_i, quad z_(i j) <= q_j, quad z_(i j) >= p_i + q_j - 1 $

  _Bit-position equations:_ For each bit position $k$:
  $ sum_(i+j=k) z_(i j) + c_(k-1) = N_k + 2 c_k $
  where $N_k$ is the $k$-th bit of $N$ and $c_(-1) = 0$.

  _No overflow:_ $c_(m+n-1) = 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.

  _Solution extraction._ Read $p = sum_i p_i 2^i$ and $q = sum_j q_j 2^j$ from the binary variables.
]

== ILP Formulations

The following reductions to Integer Linear Programming are straightforward formulations where problem constraints map directly to linear inequalities.

#reduction-rule("MaximumIndependentSet", "ILP")[
  Each vertex is either selected or not, and each edge forbids selecting both endpoints -- a constraint that is directly linear in binary indicator variables.
][
  _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v <= 1$ for each $(u, v) in E$. Objective: maximize $sum_v w_v x_v$.

  _Correctness._ ($arrow.r.double$) An independent set has no two adjacent vertices selected, so all edge constraints hold. ($arrow.l.double$) Any feasible binary solution selects no two adjacent vertices, forming an independent set; the objective maximizes total weight.

  _Solution extraction._ $S = {v : x_v = 1}$.
]

#reduction-rule("MinimumVertexCover", "ILP")[
  Every edge must be covered by at least one endpoint -- a lower-bound constraint that is directly linear in binary vertex indicators.
][
  _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v >= 1$ for each $(u, v) in E$. Objective: minimize $sum_v w_v x_v$.

  _Correctness._ ($arrow.r.double$) A vertex cover includes at least one endpoint of every edge, satisfying all constraints. ($arrow.l.double$) Any feasible solution covers every edge; the objective minimizes total weight.

  _Solution extraction._ $C = {v : x_v = 1}$.
]

#reduction-rule("MaximumMatching", "ILP")[
  Each edge is either selected or not, and each vertex may be incident to at most one selected edge -- a degree-bound constraint that is directly linear in binary edge indicators.
][
  _Construction._ Variables: $x_e in {0, 1}$ for each $e in E$. Constraints: $sum_(e in.rev v) x_e <= 1$ for each $v in V$. Objective: maximize $sum_e w_e x_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.

  _Solution extraction._ $M = {e : x_e = 1}$.
]

#reduction-rule("MaximumSetPacking", "ILP")[
  Two sets conflict if they share a universe element, and at most one of each conflicting pair may be selected -- the same exclusion structure as independent set on the intersection graph, expressible as pairwise linear constraints.
][
  _Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $x_i + x_j <= 1$ for each overlapping pair $S_i, S_j in cal(S)$ with $S_i inter S_j != emptyset$. Objective: maximize $sum_i w_i x_i$.

  _Correctness._ ($arrow.r.double$) A packing has mutually disjoint sets, so no overlapping pair is co-selected. ($arrow.l.double$) Any feasible solution selects only mutually disjoint sets; the objective maximizes total weight.

  _Solution extraction._ $cal(P) = {S_i : x_i = 1}$.
]

#reduction-rule("MinimumSetCovering", "ILP")[
  Every universe element must be covered by at least one selected set -- a lower-bound constraint on the sum of indicators for sets containing that element, which is directly linear.
][
  _Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $sum_(S_i in.rev u) x_i >= 1$ for each $u in U$. Objective: minimize $sum_i w_i x_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.

  _Solution extraction._ $cal(C) = {S_i : x_i = 1}$.
]

#reduction-rule("MinimumDominatingSet", "ILP")[
  Every vertex must be dominated -- either selected itself or adjacent to a selected vertex -- which is a lower-bound constraint on the sum of indicators over its closed neighborhood.
][
  _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_v + sum_(u in N(v)) x_u >= 1$ for each $v in V$ (each vertex dominated). Objective: minimize $sum_v w_v x_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.

  _Solution extraction._ $D = {v : x_v = 1}$.
]

#reduction-rule("MaximumClique", "ILP")[
  A clique requires every pair of selected vertices to be adjacent; equivalently, no two selected vertices may share a _non_-edge. This is the independent set formulation on the complement graph $overline(G)$.
][
  _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v <= 1$ for each $(u, v) in.not E$ (non-edges). Objective: maximize $sum_v x_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.

  _Solution extraction._ $K = {v : x_v = 1}$.
]

#reduction-rule("TravelingSalesman", "ILP",
  example: true,
  example-caption: [Weighted $K_4$: the optimal tour $0 arrow 1 arrow 3 arrow 2 arrow 0$ with cost 80 is found by position-based ILP.],
)[
  A Hamiltonian tour is a permutation of vertices. Position-based encoding assigns each vertex a tour position via binary indicators, with permutation constraints ensuring a valid bijection. The tour cost involves products of position indicators for consecutive positions, which McCormick linearization converts to auxiliary variables with linear constraints.
][
  _Construction._ For graph $G = (V, E)$ with $n = |V|$ and $m = |E|$:

  _Variables:_ Binary $x_(v,k) in {0, 1}$ for each vertex $v in V$ and position $k in {0, ..., n-1}$. Interpretation: $x_(v,k) = 1$ iff vertex $v$ is at position $k$ in the tour.

  _Auxiliary variables:_ For each edge $(u,v) in E$ and position $k$, introduce $y_(u,v,k)$ and $y_(v,u,k)$ to linearize the products $x_(u,k) dot x_(v,(k+1) mod n)$ and $x_(v,k) dot x_(u,(k+1) mod n)$ respectively.

  _Constraints:_ (1) Each vertex has exactly one position: $sum_(k=0)^(n-1) x_(v,k) = 1$ for all $v in V$. (2) Each position has exactly one vertex: $sum_(v in V) x_(v,k) = 1$ for all $k$. (3) Non-edge consecutive prohibition: if ${v,w} in.not E$, then $x_(v,k) + x_(w,(k+1) mod n) <= 1$ for all $k$. (4) McCormick: $y <= x_(v,k)$, $y <= x_(w,(k+1) mod n)$, $y >= x_(v,k) + x_(w,(k+1) mod n) - 1$.

  _Objective:_ Minimize $sum_((u,v) in E) w(u,v) dot sum_k (y_(u,v,k) + y_(v,u,k))$.

  _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.

  _Solution extraction._ For each position $k$, find vertex $v$ with $x_(v,k) = 1$ to recover the tour permutation; then select edges between consecutive positions.
]

== Unit Disk Mapping

#reduction-rule("MaximumIndependentSet", "KingsSubgraph")[
  @nguyen2023 The key idea is to represent each vertex of a general graph as a chain of grid nodes (a "copy line") on a King's subgraph, where adjacency is limited to unit-distance neighbors. Edges between vertices in the original graph are encoded by crossing gadgets: when two copy lines cross, the gadget ensures that at most one can be fully selected, mimicking the independence constraint. The overhead from the copy-line structure is a known constant $Delta$, so $"MIS"(G_"grid") = "MIS"(G) + Delta$, and the reduction preserves optimality with at most quadratic blowup.
][
  _Construction (Copy-Line Method)._ Given $G = (V, E)$ with $n = |V|$:

  1. _Vertex ordering:_ Compute a path decomposition of $G$ to obtain vertex order $(v_1, dots, v_n)$. The pathwidth determines the grid height.

  2. _Copy lines:_ For each vertex $v_i$, create an L-shaped "copy line" on the grid:
  $ "CopyLine"(v_i) = {(r, c_i) : r in [r_"start", r_"stop"]} union {(r_i, c) : c in [c_i, c_"stop"]} $
  where positions are determined by the vertex order and edge structure.

  3. _Crossing gadgets:_ When two copy lines cross (corresponding to an edge $(v_i, v_j) in E$), insert a crossing gadget that enforces: at most one of the two lines can be "active" (all vertices selected).

  4. _MIS correspondence:_ Each copy line has MIS contribution $approx |"line"|/2$. The gadgets add overhead $Delta$ such that:
  $ "MIS"(G_"grid") = "MIS"(G) + Delta $

  _Correctness._ ($arrow.r.double$) An IS $S$ in $G$ maps to a grid IS by activating copy lines for vertices in $S$ (selecting alternating grid nodes) and deactivating lines for vertices not in $S$. At each crossing gadget between adjacent vertices $v_i, v_j in S$, at most one line is active, but since $v_i$ and $v_j$ are not both in $S$ (they are independent), no conflict arises. ($arrow.l.double$) A grid MIS determines which copy lines are active (majority of nodes selected). Active lines correspond to an IS in $G$: if two adjacent vertices $v_i, v_j$ were both active, their crossing gadget would prevent both from contributing fully, contradicting optimality.

  _Solution extraction._ For each copy line, check if the majority of its vertices are in the grid MIS. Map back: $v_i in S$ iff copy line $i$ is active.
]

*Example: Petersen Graph.*#footnote[Generated using `cargo run --example export_petersen_mapping` from the accompanying code repository.] The Petersen graph ($n=10$, MIS$=4$) maps to a $30 times 42$ King's subgraph with 219 nodes and overhead $Delta = 89$. Solving MIS on the grid yields $"MIS"(G_"grid") = 4 + 89 = 93$. The weighted and unweighted KSG mappings share identical grid topology (same node positions and edges); only the vertex weights differ. With triangular lattice encoding @nguyen2023, the same graph maps to a $42 times 60$ grid with 395 nodes and overhead $Delta = 375$, giving $"MIS"(G_"tri") = 4 + 375 = 379$.

// Load JSON data
#let petersen = json("static/petersen_source.json")
#let square_weighted = json("static/petersen_square_weighted.json")
#let square_unweighted = json("static/petersen_square_unweighted.json")
#let triangular_mapping = json("static/petersen_triangular.json")

#figure(
  grid(
    columns: 3,
    gutter: 1.5em,
    align(center + horizon)[
      #{
        let pg = petersen-graph()
        canvas(length: 1cm, {
          for (u, v) in pg.edges { g-edge(pg.vertices.at(u), pg.vertices.at(v)) }
          for (k, pos) in pg.vertices.enumerate() {
            g-node(pos, fill: blue, stroke: none)
          }
        })
      }
      (a) Petersen graph
    ],
    align(center + horizon)[
      #draw-grid-graph(square_weighted)
      (b) King's subgraph (weighted)
    ],
    align(center + horizon)[
      #draw-triangular-graph(triangular_mapping)
      (c) Triangular lattice (weighted)
    ],
  ),
  caption: [Unit disk mappings of the Petersen graph. Blue: weight 1, red: weight 2, green: weight 3.],
) <fig:petersen-mapping>

#reduction-rule("MaximumIndependentSet", "TriangularSubgraph")[
  @nguyen2023 The same copy-line principle as the King's subgraph reduction applies, but on a triangular lattice. The triangular geometry offers a denser packing of neighbors (each node has 6 neighbors vs. 8 in the King's grid), which requires redesigned crossing and simplifier gadgets but preserves the same asymptotic overhead. The resulting graph is a unit disk graph under the triangular metric, suitable for hardware architectures based on triangular lattice connectivity.
][
  _Construction._ Same copy-line method as the KSG mapping: vertex ordering via path decomposition, L-shaped copy lines, and crossing gadgets at edge intersections. The gadgets are adapted for the triangular lattice geometry, where adjacency is defined by unit distance under the triangular metric (6 neighbors per interior node instead of 8).

  _Correctness._ ($arrow.r.double$) An IS in $G$ maps to an IS on the triangular grid by the same copy-line activation mechanism. ($arrow.l.double$) A grid MIS maps back to an IS by the copy-line activity rule, with the adapted crossing gadgets enforcing the same independence constraints.

  _Solution extraction._ Same as the KSG mapping: determine copy-line activity by majority vote, then map back to the original graph.

  _Overhead._ Both vertex and edge counts grow as $O(n^2)$ where $n = |V|$, matching the KSG mapping.
]

*Weighted Extension.* For MWIS, copy lines use weighted vertices (weights 1, 2, or 3). Source weights $< 1$ are added to designated "pin" vertices.

*QUBO Mapping.* A QUBO problem $min bold(x)^top Q bold(x)$ maps to weighted MIS on a grid by:
1. Creating copy lines for each variable
2. Using XOR gadgets for couplings: $x_"out" = not(x_1 xor x_2)$
3. Adding weights for linear and quadratic terms

See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/export_petersen_mapping.rs")[`export_petersen_mapping.rs`].

// Completeness check: warn about reduction rules in JSON but missing from paper
#context {
  let covered = covered-rules.get()
  let json-edges = {
    let edges = graph-data.edges.map(e => (graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name))
    let unique = ()
    for e in edges {
      if unique.find(u => u.at(0) == e.at(0) and u.at(1) == e.at(1)) == none {
        unique.push(e)
      }
    }
    unique
  }
  let missing = json-edges.filter(e => {
    covered.find(c => c.at(0) == e.at(0) and c.at(1) == e.at(1)) == none
  })
  if missing.len() > 0 {
    block(width: 100%, inset: (x: 1em, y: 0.5em), fill: rgb("#fff3cd"), stroke: (left: 3pt + rgb("#ffc107")))[
      #text(fill: rgb("#856404"), weight: "bold")[Warning: Missing reduction rules:] \
      #for m in missing [
        #text(fill: rgb("#856404"))[- #m.at(0) #sym.arrow.r #m.at(1)] \
      ]
    ]
  }
}

== Resource Estimation from Examples

The following table shows concrete variable overhead for example instances, generated from the reduction examples (`make examples`).

#let example-files = (
  "maximumindependentset_to_minimumvertexcover", "minimumvertexcover_to_maximumindependentset",
  "maximumindependentset_to_maximumsetpacking", "maximummatching_to_maximumsetpacking",
  "minimumvertexcover_to_minimumsetcovering",
  "maxcut_to_spinglass", "spinglass_to_maxcut",
  "spinglass_to_qubo", "qubo_to_spinglass",
  "maximumindependentset_to_qubo", "minimumvertexcover_to_qubo", "kcoloring_to_qubo",
  "maximumsetpacking_to_qubo", "ksatisfiability_to_qubo", "ilp_to_qubo",
  "satisfiability_to_maximumindependentset", "satisfiability_to_kcoloring", "satisfiability_to_minimumdominatingset", "satisfiability_to_ksatisfiability",
  "circuitsat_to_spinglass", "factoring_to_circuitsat",
  "maximumindependentset_to_ilp", "minimumvertexcover_to_ilp", "maximummatching_to_ilp",
  "kcoloring_to_ilp", "factoring_to_ilp",
  "maximumsetpacking_to_ilp", "minimumsetcovering_to_ilp",
  "minimumdominatingset_to_ilp", "maximumclique_to_ilp",
  "travelingsalesman_to_ilp",
)

#let examples = example-files.map(n => {
  let d = load-example(n)
  (name: n, data: d)
})

#pagebreak()
#bibliography("references.bib", style: "ieee")