Write Rule In Paper

Source Material

For mathematical content (theorems, proofs, examples), consult these sources in priority order:

1. GitHub issue for the rule (gh issue view <number>): contains the verified reduction algorithm, correctness proof, size overhead, and worked examples written during issue creation
2. Derivation documents (if available): e.g., ~/Downloads/reduction_derivations_*.typ — these contain batch-verified proofs with explicit theorem/proof blocks
3. The implementation (src/rules/<source>_<target>.rs): the code is the ground truth for the construction

Do NOT invent proofs — always cross-check against the issue and derivation sources. The issue body typically has: Reduction Algorithm, Correctness (forward/backward), Size Overhead, Example, and References sections that map directly to the paper entry structure.

Step 1: Load Example Data

#let src_tgt = load-example("Source", "Target")
#let src_tgt_sol = src_tgt.solutions.at(0)

Where:

• load-example(source, target, ...) looks up the canonical rule entry from src/example_db/fixtures/examples.json
• The returned record contains source, target, and solutions
• Access fields: src_tgt.source.instance, src_tgt.target.instance, src_tgt_sol.source_config, src_tgt_sol.target_config

Step 2: Write the Theorem Body (Rule Statement)

The theorem body is a concise block with three parts:

2a. Complexity with Reference

State the reduction's time complexity with a citation. Examples:

% With verified reference:
This $O(n + m)$ reduction @Author2023 constructs ...

% Without verified reference — add footnote:
This $O(n^2)$ reduction#footnote[Complexity not independently verified from literature.] constructs ...

Verification: Identify the best known reference for this reduction's complexity. If you cannot find a peer-reviewed or textbook source, you MUST add the footnote.

2b. Construction Summary

One sentence describing what the reduction builds:

... constructs an intersection graph $G' = (V', E')$ where ...

2c. Overhead Hint

State target dimensions in terms of source. This complements the auto-derived overhead (which appears automatically from JSON edge data):

... ($n k$ variables indexed by $v dot k + c$).

Complete theorem body example

][
  Given $G = (V, E)$ with $k$ colors, construct upper-triangular
  $Q in RR^(n k times n k)$ using one-hot encoding $x_(v,c) in {0,1}$
  ($n k$ variables indexed by $v dot k + c$).
]

Step 3: Write the Proof Body

The proof must be self-contained (all notation defined before use) and reproducible (enough detail to reimplement the reduction from the proof alone).

Structure

Use these subsections in order. Use italic labels exactly as shown:

][
  _Construction._ ...

  _Correctness._ ...

  _Variable mapping._ ...    // only if the reduction has a non-trivial variable mapping

  _Solution extraction._ ...
]

3a. Construction

Full mathematical construction of the target instance. Define all symbols and notation here.

For standard reductions (< 300 LOC): Write the complete construction with enough math to reimplement.

For heavy reductions (300+ LOC): Briefly describe the approach and cite a reference:

_Construction._ The reduction follows the standard Cook–Levin construction @Cook1971,
encoding each gate as a set of clauses. See @Source for full details.

3b. Correctness

Bidirectional (iff) argument showing solution correspondence. Use ($arrow.r.double$) and ($arrow.l.double$) for each direction:

_Correctness._ ($arrow.r.double$) If $S$ is independent, then ...
($arrow.l.double$) If $C$ is a vertex cover, then ...

3c. Variable Mapping (if applicable)

Explicitly state how source variables map to target variables. Include this section when the mapping is non-trivial (encoding, expansion, reindexing). Omit for identity mappings or trivial complement operations.

_Variable mapping._ Vertices $= {S_1, ..., S_m}$, edges $= {(S_i, S_j) : S_i inter S_j != emptyset}$, $w(v_i) = w(S_i)$.

3d. Solution Extraction

How to convert a target solution back to a source solution:

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

Step 4: Write the Worked Example (Extra Block)

Detailed by default. Only use a brief example for trivially obvious reductions (complement, identity).

4a. Typst Skeleton

#reduction-rule("Source", "Target",
  example: true,
  example-caption: [Description ($n = ...$, $|E| = ...$)],
  extra: [
    #pred-commands(
      "pred create --example <ALIAS> -o <name>.json",
      "pred reduce <name>.json --to " + target-spec(src_tgt) + " -o bundle.json",
      "pred solve bundle.json",
      "pred evaluate <name>.json --config " + src_tgt_sol.source_config.map(str).join(","),
    )

    // Optional: graph visualization
    #{
      // canvas code for graph rendering
    }

    *Step 1 -- [action].* [description with concrete numbers]

    *Step 2 -- [action].* [construction details]

    // ... more steps as needed

    *Step N -- Verify a solution.* [end-to-end verification]

    *Multiplicity:* The fixture stores one canonical witness. If total multiplicity matters, explain it from the construction.
  ],
)

4a2. Reproducibility Commands

Add a pred-commands() block at the top of the extra: content, before any data display or visualization. The source-side pred create --example ... spec must be derived from the loaded example data, not handwritten:

#let problem-spec(data) = {
  if data.variant.len() == 0 { data.problem }
  else { data.problem + "/" + data.variant.values().join("/") }
}

#pred-commands(
  "pred create --example " + problem-spec(src_tgt.source) + " -o <source>.json",
  "pred reduce <source>.json --to " + target-spec(src_tgt) + " -o bundle.json",
  "pred solve bundle.json",
  "pred evaluate <source>.json --config " + src_tgt_sol.source_config.map(str).join(","),
)

If docs/paper/reductions.typ already defines a shared problem-spec() helper, reuse it instead of duplicating it. Do not guess whether the default variant matches the canonical example; canonical rule fixtures can point at non-default source variants, and handwritten bare aliases can silently break the reproducibility block.

The target-spec() helper handles empty variant dicts automatically. The --config is composed from src_tgt_sol.source_config.

4b. Step-by-Step Content

Each step should:

1. Name the action in bold: *Step K -- [verb phrase].*
2. Show concrete numbers from the example instance (use Typst expressions to extract from JSON, not hardcoded values)
3. Explain where overhead comes from — e.g., "5 vertices x 3 colors = 15 QUBO variables"

4c. Required Steps

4d. Graph Visualization (if applicable)

#{
  let fills = src_tgt_sol.source_config.map(c => graph-colors.at(c))
  align(center, canvas(length: 0.8cm, {
    for (u, v) in graph.edges { g-edge(graph.vertices.at(u), graph.vertices.at(v)) }
    for (k, pos) in graph.vertices.enumerate() {
      g-node(pos, name: str(k), fill: fills.at(k), label: str(k))
    }
  }))
}

4e. Accessing Solution Data

// Source configuration (e.g., color assignments)
#src_tgt_sol.source_config.map(str).join(", ")

// Target configuration (e.g., binary encoding)
#src_tgt_sol.target_config.map(str).join(", ")

// The canonical witness pair
#src_tgt.solutions.at(0)

// Source instance fields
#src_tgt.source.instance.num_vertices

Step 5: Register Display Name (if new problem)

If this is a new problem not yet in the paper, add to the display-name dictionary near the top of reductions.typ:

"ProblemName": [Display Name],

Step 6: Build and Verify

# Build the paper
make paper

Verification Checklist

• Notation self-contained: every symbol is defined before first use within the proof
• Complexity cited: reference exists, or footnote added for unverified claims
• Overhead consistent: prose dimensions match auto-derived overhead from JSON edge data
• Example uses JSON data: concrete values come from load-example/load-results, not hardcoded
• Solution verified: at least one solution checked end-to-end in the example
• Witness semantics: text treats solutions.at(0) as the canonical witness; any multiplicity claim is derived mathematically, not from fixture length
• Pred commands present: pred-commands() block at top of example with create/reduce/solve/evaluate pipeline
• Paper compiles: make paper succeeds without errors
• Completeness check: no new warnings about missing edges in the paper

For simpler reductions, see MinimumVertexCover ↔ MaximumIndependentSet as a minimal example.