Rebuild the graph page: Explorer panel, growth filter and Turing toggle

docs/paper/references.bib

@@ -2332,3 +2332,14 @@ @article{axler2019
   year = {2019},
   url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf}
 }
+
+@article{een2006,
+  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
+  title = {Translating Pseudo-Boolean Constraints into {SAT}},
+  journal = {Journal on Satisfiability, Boolean Modeling and Computation},
+  year = {2006},
+  volume = {2},
+  number = {1--4},
+  pages = {1--26},
+  doi = {10.3233/SAT190014},
+}

docs/website/graph-scene.schema.json

@@ -23,12 +23,27 @@
       "type": "array",
       "items": {
         "type": "object", "additionalProperties": false,
-        "required": ["source", "target", "witness", "turing"],
+        "required": ["source", "target", "witness", "aggregate", "turing", "fields"],
         "properties": {
           "source": {"type": "integer", "minimum": 0, "maximum": 9007199254740991},
           "target": {"type": "integer", "minimum": 0, "maximum": 9007199254740991},
           "witness": {"type": "boolean"},
-          "turing": {"type": "boolean"}
+          "aggregate": {"type": "boolean"},
+          "turing": {"type": "boolean"},
+          "fields": {
+            "type": "object",
+            "additionalProperties": {
+              "type": "object", "additionalProperties": false,
+              "required": ["certificate", "accuracy"],
+              "properties": {
+                "certificate": {"type": ["string", "null"], "minLength": 1},
+                "accuracy": {
+                  "type": "object", "required": ["kind"],
+                  "properties": {"kind": {"enum": ["exact", "upper_bound", "unavailable"]}}
+                }
+              }
+            }
+          }
         }
       }
     },

docs/website/graph.html

@@ -8,8 +8,13 @@
   <title>Reduction Paths — Problem Reductions</title>
   <link rel="icon" href="./assets/favicon.svg" type="image/svg+xml">
   <link rel="preload" href="./assets/graph-scene.json.gz" as="fetch" type="application/gzip" crossorigin>
-  <link rel="preload" href="./assets/path-graph.json.gz" as="fetch" type="application/gzip" crossorigin>
-  <link rel="preload" href="./assets/path-selection_bg.wasm.gz" as="fetch" type="application/gzip" crossorigin>
+  <script>
+    if (location.hash === '#directions') for (const name of ['path-graph.json.gz', 'path-selection_bg.wasm.gz']) {
+      const link = document.createElement('link');
+      Object.assign(link, {rel: 'preload', href: './assets/' + name, as: 'fetch', type: 'application/gzip', crossOrigin: ''});
+      document.head.append(link);
+    }
+  </script>
   <link rel="preload" href="./assets/fonts/dm-sans-variable.woff2" as="font" type="font/woff2" crossorigin>
   <link rel="stylesheet" href="./src/styles/site.css">
   <link rel="stylesheet" href="./src/styles/details.css">
@@ -33,24 +38,45 @@
 </header>
 <main id="canvas" aria-label="Reduction graph"><div id="cy"></div></main>
 
-<section class="panel" aria-label="Reduction paths">
-  <header class="panel-head"><h1 class="brand"><a href="./index.html">Reduction paths</a></h1></header>
-  <div class="ends" id="ends">
-    <div class="end from">
-      <span class="pin" aria-hidden="true"></span>
-      <div><input id="source" placeholder="Start problem" autocomplete="off" spellcheck="false" aria-label="Start problem" role="combobox" aria-autocomplete="list" aria-expanded="false" aria-controls="suggest"><div class="options" id="source-options" hidden></div></div>
+<section class="panel" aria-label="Reduction graph">
+  <p id="graph-error" class="note" role="alert" hidden></p>
+  <div id="view-explore" class="view">
+    <h1 class="sr-only">Reduction graph</h1>
+    <div class="search-row">
+      <label class="searchbox"><svg width="16" height="16" viewBox="0 0 16 16" fill="none" stroke="currentColor" stroke-width="1.5" stroke-linecap="round" aria-hidden="true"><circle cx="7" cy="7" r="4.5"/><path d="m10.5 10.5 3 3"/></svg><input id="find" type="search" placeholder="Search problems" autocomplete="off" spellcheck="false" aria-label="Search problems and rules"></label>
+      <button id="go-directions" class="dir-btn" type="button"><svg width="16" height="16" viewBox="0 0 18 18" fill="none" stroke="currentColor" stroke-width="1.7" stroke-linecap="round" stroke-linejoin="round" aria-hidden="true"><path d="M9 1.8 16.2 9 9 16.2 1.8 9Z"/><path d="M6 10V8.4a1 1 0 0 1 1-1h4.6M10.2 5.9l1.6 1.5-1.6 1.5"/></svg>Directions</button>
     </div>
-    <div class="end to">
-      <span class="pin" aria-hidden="true"></span>
-      <div><input id="target" placeholder="End problem" autocomplete="off" spellcheck="false" aria-label="End problem" role="combobox" aria-autocomplete="list" aria-expanded="false" aria-controls="suggest"><div class="options" id="target-options" hidden></div></div>
+    <div class="tabs" id="tabs" role="tablist" aria-label="Browse"></div>
+    <div class="explore-body" id="explore-body"></div>
+  </div>
+  <div id="view-directions" class="view" hidden>
+    <header class="panel-head dir-head"><button id="back-explore" class="back-btn" type="button" aria-label="Back to explore"><svg width="16" height="16" viewBox="0 0 16 16" fill="none" stroke="currentColor" stroke-width="1.6" stroke-linecap="round" stroke-linejoin="round" aria-hidden="true"><path d="M10 3 5 8l5 5"/></svg></button><h1 class="brand">Directions</h1></header>
+    <div class="ends" id="ends">
+      <div class="end from">
+        <span class="pin" aria-hidden="true"></span>
+        <div><input id="source" placeholder="Start problem" autocomplete="off" spellcheck="false" aria-label="Start problem" role="combobox" aria-autocomplete="list" aria-expanded="false" aria-controls="suggest"><div class="options" id="source-options" hidden></div></div>
+      </div>
+      <div class="end to">
+        <span class="pin" aria-hidden="true"></span>
+        <div><input id="target" placeholder="End problem" autocomplete="off" spellcheck="false" aria-label="End problem" role="combobox" aria-autocomplete="list" aria-expanded="false" aria-controls="suggest"><div class="options" id="target-options" hidden></div></div>
+      </div>
+      <button class="swap" id="swap" aria-label="Swap start and end"><svg width="16" height="16" viewBox="0 0 16 16" fill="none" stroke="currentColor" stroke-width="1.4" stroke-linecap="round" stroke-linejoin="round"><path d="M5 2.5v11M2.5 5 5 2.5 7.5 5M11 13.5v-11M8.5 11l2.5 2.5 2.5-2.5"/></svg></button>
+      <div class="suggest" id="suggest" role="listbox" aria-label="Problems" hidden></div>
     </div>
-    <button class="swap" id="swap" aria-label="Swap start and end"><svg width="16" height="16" viewBox="0 0 16 16" fill="none" stroke="currentColor" stroke-width="1.4" stroke-linecap="round" stroke-linejoin="round"><path d="M5 2.5v11M2.5 5 5 2.5 7.5 5M11 13.5v-11M8.5 11l2.5 2.5 2.5-2.5"/></svg></button>
-    <div class="suggest" id="suggest" role="listbox" aria-label="Problems" hidden></div>
+    <div id="search-status" class="sr-only" role="status"></div>
+    <div class="results" id="results" aria-live="polite"></div>
   </div>
-  <div id="search-status" class="sr-only" role="status"></div>
-  <div class="results" id="results" aria-live="polite"></div>
+  <p class="route-note">Routes alone do not establish complexity or solver availability. Colours summarize variants.</p>
+</section>
+
+<section class="mapbar" id="mapbar" aria-label="Map controls">
+  <div class="seg" id="views" role="group" aria-label="Map view"></div>
+  <div class="legend-group"><span class="legend-label" id="growth-label">Growth</span><div class="growth-legend" id="growth-legend" role="radiogroup" aria-labelledby="growth-label"></div></div>
+  <button type="button" class="legend-chip turing-toggle" id="turing-toggle" role="switch" aria-checked="false">Turing</button>
 </section>
 
+<div class="status-legend" id="status-legend" role="note" aria-label="Node colours"></div>
+
 <div class="pop" id="pop" role="dialog" aria-labelledby="pop-title" hidden></div>
 <nav class="dock" aria-label="Graph navigation">
   <button id="zoom-in" aria-label="Zoom in"><svg width="14" height="14" viewBox="0 0 14 14" stroke="currentColor" stroke-width="1.5" stroke-linecap="round"><path d="M7 2v10M2 7h10"/></svg></button>

docs/website/src/lib/force-layout.mts

@@ -0,0 +1,97 @@
+/* Deterministic force model for the problem graph, shared by the build (published map) and the page (live
+   dragging and re-layout). It follows d3-force: link springs biased by degree, pairwise charge, collision, and a
+   weak pull to the origin. Rules into a solver hub pull weakly and the hubs repel strongly, so the hundred-odd ILP
+   encodings fan out instead of collapsing the map into a star. */
+
+export interface Point { x: number; y: number }
+export interface LayoutInput {
+  ids: readonly string[];
+  links: readonly (readonly [string, string])[];
+  hubs: ReadonlySet<string>;
+  radius: (id: string) => number;
+  // Where to begin; missing ids start on d3's phyllotaxis spiral, so the result never depends on randomness.
+  start?: ReadonlyMap<string, Point>;
+  // Total ticks for a full cool-down from alpha 1.
+  ticks?: number;
+}
+export interface Simulation {
+  alpha: number;
+  // Live interaction holds alpha near this target instead of letting it cool to zero.
+  alphaTarget: number;
+  tick(): void;
+  // A pinned node stays where it is put and the rest of the graph responds to it.
+  pin(id: string, p: Point | null): void;
+  positions(): Map<string, Point>;
+}
+const ALPHA_MIN = 0.001;
+
+export function createSimulation({ ids, links, hubs, radius, start, ticks = 300 }: LayoutInput): Simulation {
+  const index = new Map(ids.map((id, i) => [id, i]));
+  const nodes = ids.map((id, i) => {
+    const p = start?.get(id), r = 10 * Math.sqrt(0.5 + i), a = i * Math.PI * (3 - Math.sqrt(5));
+    return { id, x: p?.x ?? r * Math.cos(a), y: p?.y ?? r * Math.sin(a), vx: 0, vy: 0, r: radius(id), hub: hubs.has(id),
+      degree: 0, fixed: null as Point | null };
+  });
+  const edges = links.flatMap(([a, b]) => {
+    const s = index.get(a), t = index.get(b);
+    return s === undefined || t === undefined || s === t ? [] : [{ s: nodes[s]!, t: nodes[t]!, hub: hubs.has(a) || hubs.has(b) }];
+  });
+  for (const { s, t } of edges) { s.degree++; t.degree++; }
+  const decay = 1 - Math.pow(ALPHA_MIN, 1 / ticks), velocityDecay = 0.4;
+
+  const sim: Simulation = {
+    alpha: 1, alphaTarget: 0,
+    tick() {
+      const alpha = sim.alpha += (sim.alphaTarget - sim.alpha) * decay;
+      for (const { s, t, hub } of edges) {
+        let dx = t.x + t.vx - s.x - s.vx || 1e-6, dy = t.y + t.vy - s.y - s.vy || 1e-6;
+        const len = Math.hypot(dx, dy), k = (len - (hub ? 120 : 32)) / len * alpha * (hub ? 0.04 : 0.5);
+        dx *= k; dy *= k;
+        const bias = s.degree / (s.degree + t.degree);
+        t.vx -= dx * bias; t.vy -= dy * bias; s.vx += dx * (1 - bias); s.vy += dy * (1 - bias);
+      }
+      for (let i = 0; i < nodes.length; i++) {
+        const a = nodes[i]!;
+        for (let j = i + 1; j < nodes.length; j++) {
+          const b = nodes[j]!, dx = b.x - a.x || 1e-6, dy = b.y - a.y || 1e-6, d2 = dx * dx + dy * dy;
+          // Each node pushes the other with its own charge.
+          const pa = (b.hub ? -600 : -34) * alpha / d2, pb = (a.hub ? -600 : -34) * alpha / d2;
+          a.vx += dx * pa; a.vy += dy * pa; b.vx -= dx * pb; b.vy -= dy * pb;
+          const min = a.r + b.r + 2;
+          if (d2 < min * min) {
+            const d = Math.sqrt(d2), push = (min - d) / d * 0.5;
+            a.vx -= dx * push; a.vy -= dy * push; b.vx += dx * push; b.vy += dy * push;
+          }
+        }
+      }
+      for (const n of nodes) {
+        if (n.fixed) { n.x = n.fixed.x; n.y = n.fixed.y; n.vx = n.vy = 0; continue; }
+        n.vx -= n.x * (n.degree ? 0.03 : 0.08) * alpha;
+        n.vy -= n.y * (n.degree ? 0.05 : 0.09) * alpha;
+        n.x += n.vx *= 1 - velocityDecay; n.y += n.vy *= 1 - velocityDecay;
+      }
+    },
+    pin(id, p) { const n = nodes[index.get(id) ?? -1]; if (n) n.fixed = p; },
+    positions: () => new Map(nodes.map(n => [n.id, { x: n.x, y: n.y }])),
+  };
+  return sim;
+}
+
+/* Runs the model to rest: the build's published map, or a view laid out without waiting for frames. */
+export function forceLayout(input: LayoutInput): Map<string, Point> {
+  const sim = createSimulation(input);
+  while (sim.alpha > ALPHA_MIN) sim.tick();
+  return sim.positions();
+}
+export const settled = (sim: Simulation) => sim.alpha <= ALPHA_MIN && sim.alphaTarget === 0;
+
+// Let input and painting run between short batches; canceled views must not apply stale positions.
+export async function settleSimulation(sim: Simulation, signal: AbortSignal): Promise<boolean> {
+  while (!settled(sim)) {
+    await new Promise<void>(resolve => setTimeout(resolve, 0));
+    if (signal.aborted) return false;
+    const until = performance.now() + 4;
+    do { sim.tick(); } while (!settled(sim) && performance.now() < until);
+  }
+  return !signal.aborted;
+}

docs/website/src/lib/graph-structure.mts

@@ -0,0 +1,122 @@
+import { growth, compareDegrees } from './graph-growth.mts';
+
+export interface GrowthField { certificate: string | null; accuracy: { kind: 'exact' | 'upper_bound' | 'unavailable' } }
+export interface RuleEdge {
+  source: number; target: number; witness: boolean; aggregate: boolean; turing: boolean;
+  fields: Record<string, GrowthField>;
+}
+export type Scope = 'witness' | 'aggregate' | 'turing';
+export type ClassId = 'constant' | 'linear' | 'quadratic' | 'cubic' | 'higher' | 'unknown';
+export interface Link { source: number; target: number }
+
+/* Polynomial total degree when every source parameter scales together: a visualization convention, not a runtime claim. */
+export const CLASSES: readonly { id: ClassId; label: string; name: string }[] = [
+  { id: 'constant', label: '1', name: 'Constant' },
+  { id: 'linear', label: 'n', name: 'Linear' },
+  { id: 'quadratic', label: 'n²', name: 'Quadratic' },
+  { id: 'cubic', label: 'n³', name: 'Cubic' },
+  { id: 'higher', label: 'n⁴⁺', name: 'Higher degree' },
+  { id: 'unknown', label: '?', name: 'Undetermined' },
+];
+const order = new Map(CLASSES.map((c, i) => [c.id, i]));
+
+export function growthClass(degree: bigint | null): ClassId {
+  if (degree === null) return 'unknown';
+  return degree >= 4n ? 'higher' : (['constant', 'linear', 'quadratic', 'cubic'] as const)[Number(degree)]!;
+}
+
+export interface EdgeGrowth {
+  degree: bigint | null; cls: ClassId; accuracy: 'exact' | 'upper_bound';
+  fields: { name: string; degree: bigint | null; lead: string; kind: GrowthField['accuracy']['kind'] }[];
+}
+const memo = new WeakMap<RuleEdge, EdgeGrowth>();
+/* Overview policy: the highest field degree. One unavailable field leaves the whole edge undetermined. */
+export function edgeGrowth(edge: RuleEdge): EdgeGrowth {
+  const cached = memo.get(edge);
+  if (cached) return cached;
+  const fields = Object.entries(edge.fields).map(([name, f]) => ({ name, kind: f.accuracy.kind, ...growth(f) }));
+  let degree: bigint | null = 0n;
+  for (const f of fields) {
+    if (f.degree === null) { degree = null; break; }
+    if (compareDegrees(f.degree, degree) > 0) degree = f.degree;
+  }
+  const out = { degree, cls: growthClass(degree), fields,
+    accuracy: fields.every(f => f.kind === 'exact') ? 'exact' as const : 'upper_bound' as const };
+  memo.set(edge, out);
+  return out;
+}
+
+/* Indices of the rules in any listed scope whose class is at most `limit`. `skip` lists rules excluded by other filters. */
+export function activeRules(rules: readonly RuleEdge[], { scope, limit, skip }: { scope: Scope | readonly Scope[]; limit: ClassId; skip?: Set<number> }) {
+  const max = order.get(limit)!, scopes = [scope].flat();
+  return rules.flatMap((rule, i) => scopes.some(s => rule[s]) && !skip?.has(i) && order.get(edgeGrowth(rule).cls)! <= max ? [i] : []);
+}
+
+/* Strongly connected components (iterative Tarjan); `comp[v]` indexes `groups`. */
+export function components(n: number, links: readonly Link[]) {
+  const out: number[][] = Array.from({ length: n }, () => []);
+  for (const l of links) out[l.source]!.push(l.target);
+  const index = new Array<number>(n).fill(-1), low = new Array<number>(n).fill(0), on = new Array<boolean>(n).fill(false);
+  const comp = new Array<number>(n).fill(-1), groups: number[][] = [], stack: number[] = [];
+  let counter = 0;
+  for (let root = 0; root < n; root++) {
+    if (index[root] !== -1) continue;
+    const work: [number, number][] = [[root, 0]];
+    while (work.length) {
+      const frame = work[work.length - 1]!, v = frame[0];
+      if (frame[1] === 0) { index[v] = low[v] = counter++; stack.push(v); on[v] = true; }
+      if (frame[1] < out[v]!.length) {
+        const w = out[v]![frame[1]++]!;
+        if (index[w] === -1) work.push([w, 0]);
+        else if (on[w]) low[v] = Math.min(low[v]!, index[w]!);
+        continue;
+      }
+      work.pop();
+      if (work.length) { const p = work[work.length - 1]![0]; low[p] = Math.min(low[p]!, low[v]!); }
+      if (low[v] === index[v]) {
+        const group: number[] = [];
+        for (let w = -1; w !== v;) { w = stack.pop()!; on[w] = false; comp[w] = groups.length; group.push(w); }
+        groups.push(group);
+      }
+    }
+  }
+  return { comp, groups };
+}
+
+/* Concrete variants reachable from `start` along (down) or towards (up) the active links, excluding `start` itself. */
+export function reach(n: number, links: readonly Link[], start: number, direction: 'down' | 'up') {
+  const next: number[][] = Array.from({ length: n }, () => []);
+  for (const l of links) (direction === 'down' ? next[l.source]! : next[l.target]!).push(direction === 'down' ? l.target : l.source);
+  const seen = new Set<number>([start]), queue = [start];
+  for (let v = queue.pop(); v !== undefined; v = queue.pop()) for (const w of next[v]!) if (!seen.has(w)) { seen.add(w); queue.push(w); }
+  seen.delete(start);
+  return seen;
+}
+
+export interface FamilyRule { source: string; target: string; rules: number[]; cls: ClassId; worst: ClassId }
+/* Family-level navigation edges. Each keeps the exact variant rules behind it; `cls` is its cheapest rule, `worst` its dearest. */
+export function familyRules(nodes: readonly { name: string }[], rules: readonly RuleEdge[], active: readonly number[]) {
+  const out = new Map<string, FamilyRule>();
+  for (const i of active) {
+    const rule = rules[i]!, s = nodes[rule.source]!.name, t = nodes[rule.target]!.name;
+    if (s === t) continue;
+    const cls = edgeGrowth(rule).cls, key = s + '→' + t, entry = out.get(key);
+    if (!entry) out.set(key, { source: s, target: t, rules: [i], cls, worst: cls });
+    else {
+      entry.rules.push(i);
+      if (order.get(cls)! < order.get(entry.cls)!) entry.cls = cls;
+      if (order.get(cls)! > order.get(entry.worst)!) entry.worst = cls;
+    }
+  }
+  return out;
+}
+
+/* Fewest reductions from any root; keep concrete variant IDs to avoid joining unrelated variants. */
+export function depthsFrom<T extends string | number>(names: readonly T[], links: readonly { source: T; target: T }[], roots: readonly T[]) {
+  const next = new Map<T, T[]>();
+  for (const l of links) (next.get(l.source) ?? next.set(l.source, []).get(l.source)!).push(l.target);
+  const depth = new Map<T, number>(roots.filter(r => names.includes(r)).map(r => [r, 0]));
+  const queue = [...depth.keys()];
+  for (let i = 0; i < queue.length; i++) for (const w of next.get(queue[i]!) ?? []) if (!depth.has(w)) { depth.set(w, depth.get(queue[i]!)! + 1); queue.push(w); }
+  return new Map(names.map(n => [n, depth.get(n) ?? null] as const));
+}