1"""Stage 6: build the manuscript figures as PDF files in results/figures/.23matplotlib is not available in the sandbox, so every figure is emitted as a4TikZ/pgfplots document (results/figures/src/*.tex) and compiled with the5locally cached tectonic bundle. All plotted numbers are read from results/.6Graph drawings are produced from the P(n,k) definition; chronologies are7re-validated here by an independent closure replay before they are drawn8(an illegal force aborts the build).9"""10import csv11import json12import math13import os14import subprocess15import sys1617ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))18os.chdir(ROOT)19OUT = "results/figures"20SRC = f"{OUT}/src"21os.makedirs(SRC, exist_ok=True)22import shutil23shutil.copy("manuscript/autoscholar.cls", f"{SRC}/autoscholar.cls") # same class and fonts as the manuscript2425PRE = r"""\documentclass{autoscholar}26\usepackage{tikz}27\usepackage{pgfplots}28\pgfplotsset{compat=1.18}29\usetikzlibrary{arrows.meta,calc,backgrounds,positioning}30\definecolor{asblue}{HTML}{2B5C8A}31\definecolor{asgold}{HTML}{B8860B}32% the figure is measured in a box and shipped out on a page of exactly its size;33% the class's end-of-document disclosure is not wanted on a figure file34\RemoveFromHook{enddocument}[autoscholar]35\newsavebox\figbox36\begin{document}37\begin{lrbox}{\figbox}%38"""39POST = r"""%40\end{lrbox}41\hoffset=-1in \voffset=-1in42\pdfpagewidth=\dimexpr\wd\figbox+6pt\relax43\pdfpageheight=\dimexpr\ht\figbox+\dp\figbox+6pt\relax44\shipout\vbox{\kern3pt\hbox{\kern3pt\usebox\figbox\kern3pt}\kern3pt}45\end{document}46"""474849# ------------------------------------------------------------------ graph helpers50def nbrs(n, k, v):51 layer, i = v52 if layer == "u":53 return [("u", (i - 1) % n), ("u", (i + 1) % n), ("v", i)]54 return [("v", (i - k) % n), ("v", (i + k) % n), ("u", i)]555657def replay(n, k, S, chron):58 """independent legality check of a chronology; returns final black set"""59 black = set(S)60 for src, tgt in chron:61 if src not in black or tgt in black:62 raise ValueError(f"illegal force {src}->{tgt}: source white or target black")63 white = [w for w in nbrs(n, k, src) if w not in black]64 if white != [tgt]:65 raise ValueError(f"illegal force {src}->{tgt}: white neighbours {white}")66 black.add(tgt)67 return black686970def parse(label):71 return (label[0], int(label[1:]))727374def pos(n, layer, i, R=3.0, r=1.75):75 ang = math.pi / 2 - 2 * math.pi * i / n76 rad = R if layer == "u" else r77 return rad * math.cos(ang), rad * math.sin(ang)787980def petersen_tikz(n, k, fill=None, labels=None, forces=None, R=3.0, r=1.75, node_r="2.6pt", label_size="tiny", show_index=True, legend=None):81 """fill: dict vertex -> colour ; labels: dict vertex -> text inside node;82 forces: list of (src, tgt, step) drawn as arrows along the edge"""83 fill = fill or {}84 labels = labels or {}85 L = []86 L.append("\\begin{tikzpicture}[every node/.style={inner sep=0pt}]")87 L.append(f"\\tikzset{{v/.style={{circle,draw=asink,line width=0.5pt,minimum size={node_r},inner sep=0pt}}}}")88 # edges89 for i in range(n):90 x1, y1 = pos(n, "u", i, R, r)91 x2, y2 = pos(n, "u", (i + 1) % n, R, r)92 L.append(f"\\draw[asstone,line width=0.6pt] ({x1:.3f},{y1:.3f}) -- ({x2:.3f},{y2:.3f});")93 x3, y3 = pos(n, "v", i, R, r)94 L.append(f"\\draw[asline,line width=0.6pt] ({x1:.3f},{y1:.3f}) -- ({x3:.3f},{y3:.3f});")95 x4, y4 = pos(n, "v", (i + k) % n, R, r)96 L.append(f"\\draw[asstone,line width=0.6pt] ({x3:.3f},{y3:.3f}) -- ({x4:.3f},{y4:.3f});")97 # forces98 for src, tgt, step in (forces or []):99 xs, ys = pos(n, src[0], src[1], R, r)100 xt, yt = pos(n, tgt[0], tgt[1], R, r)101 L.append(f"\\draw[asaccent,line width=0.9pt,-{{Stealth[length=4pt]}},shorten >=3.2pt,shorten <=3.2pt] ({xs:.3f},{ys:.3f}) -- ({xt:.3f},{yt:.3f});")102 # vertices103 for layer in ("u", "v"):104 for i in range(n):105 v = (layer, i)106 x, y = pos(n, layer, i, R, r)107 col = fill.get(v, "white")108 txt = labels.get(v, "")109 tcol = "white" if col in ("asink", "asaccent", "asblue") else "asink"110 L.append(f"\\node[v,fill={col}] at ({x:.3f},{y:.3f}) {{\\{label_size}\\color{{{tcol}}}{txt}}};")111 if show_index:112 ang = math.pi / 2 - 2 * math.pi * i / n113 off = 0.36 if layer == "u" else -0.37114 lx, ly = (R + off) * math.cos(ang), (R + off) * math.sin(ang)115 if layer == "v":116 lx, ly = (r + off) * math.cos(ang), (r + off) * math.sin(ang)117 # index labels at \scriptsize (enlarged after referee round 1, finding F7)118 L.append(f"\\node[inner sep=1pt] at ({lx:.3f},{ly:.3f}) {{\\scriptsize\\color{{asstone}}${layer}_{{{i}}}$}};")119 if legend:120 L.append(legend)121 L.append("\\end{tikzpicture}")122 return "\n".join(L)123124125def compile_tex(name, body):126 path = f"{SRC}/{name}.tex"127 open(path, "w").write(PRE + body + POST)128 cmd = ["tectonic", "-X", "compile", "--only-cached", "-o", OUT, path]129 res = subprocess.run(cmd, capture_output=True, text=True)130 if res.returncode != 0:131 sys.stderr.write(res.stdout[-3000:] + res.stderr[-3000:])132 raise SystemExit(f"figure {name} failed")133 print("built", f"{OUT}/{name}.pdf")134135136# ------------------------------------------------------------------ data137exact = {int(r["n"]): r for r in csv.DictReader(open("results/exact_values.csv"))}138kvn = {int(r["n"]): r for r in csv.DictReader(open("results/known_vs_new.csv"))}139window = list(csv.DictReader(open("results/tables/boundary_window_p18.csv")))140btab = list(csv.DictReader(open("results/tables/boundary_table.csv")))141bf = list(csv.DictReader(open("results/tables/brute_force.csv")))142wit = [json.loads(l) for l in open("results/upper_bound_witnesses.jsonl") if l.strip()]143cex = [json.loads(l) for l in open("results/counterexamples.jsonl") if l.strip()]144summary = json.load(open("results/robustness/summary.json"))145146# ------------------------------------------------------------------ Fig 1: anatomy P(13,5) and P(15,5)147for n in (13, 15):148 body = petersen_tikz(n, 5, R=2.6, r=1.5, node_r="3.4pt")149 compile_tex(f"fig1_anatomy_P{n}_5", body)150151# ------------------------------------------------------------------ Fig 2a: P7 chronology on P(14,5)152n = 14153S = [("u", i) for i in range(12)]154chron = [(("u", i), ("v", i)) for i in range(1, 11)] + [(("v", 5), ("v", 0)), (("v", 6), ("v", 11))]155for j in range(12, n):156 chron += [(("u", j - 1), ("u", j)), (("v", j - 5), ("v", j))]157final = replay(n, 5, S, chron)158assert len(final) == 2 * n, "P7 chronology does not force P(14,5)"159fill = {v: "asink" for v in S}160labels = {}161forces = []162for step, (s, t) in enumerate(chron, 1):163 labels[t] = str(step)164 forces.append((s, t, step))165legend = ("\\node[anchor=north,align=left,text width=7.6cm] at (0,-3.55) {\\footnotesize black $=$ initial set $S=\\{u_0,\\dots,u_{11}\\}$;\\ "166 "numbers $=$ step at which the vertex is forced};")167compile_tex("fig2a_chronology_P14_5_P7", petersen_tikz(n, 5, fill=fill, labels=labels, forces=forces, R=2.9, r=1.7, node_r="9pt", label_size="scriptsize", legend=legend))168169# ------------------------------------------------------------------ Fig 2b: optimal witness on P(15,5)170w15 = min((w for w in wit if w["n"] == 15), key=lambda w: w["size"])171S = [parse(x) for x in w15["S"]]172chron = [(parse(a), parse(b)) for a, b in w15["chronology"]]173final = replay(15, 5, S, chron)174assert len(final) == 30 and len(S) == 8175fill = {v: "asink" for v in S}176labels = {}177forces = []178for step, (s, t) in enumerate(chron, 1):179 labels[t] = str(step)180 forces.append((s, t, step))181legend = ("\\node[anchor=north,align=left,text width=7.6cm] at (0,-3.55) {\\footnotesize black $=$ minimum zero-forcing set of size $8$ "182 "($" + ",".join(f"{a}_{{{i}}}" for a, i in S) + "$)};")183compile_tex("fig2b_chronology_P15_5_optimal", petersen_tikz(15, 5, fill=fill, labels=labels, forces=forces, R=2.9, r=1.7, node_r="9pt", label_size="scriptsize", legend=legend))184185# ------------------------------------------------------------------ Fig 3: exact values 11..48186known = [(n, int(exact[n]["Z"])) for n in sorted(exact) if kvn[n]["classification"] == "known"]187new = [(n, int(exact[n]["Z"])) for n in sorted(exact) if kvn[n]["classification"] == "new"]188hold = [(n, int(exact[n]["Z"])) for n in sorted(exact) if exact[n]["holdout"] == "True"]189ub = [(n, int(kvn[n]["published_upper_bound"])) for n in sorted(exact)]190body = r"""\begin{tikzpicture}191\begin{axis}[width=14cm,height=7cm,xlabel={$n$},ylabel={$Z(P(n,5))$},xmin=10,xmax=49,ymin=2,ymax=13.5,192 ytick={2,4,6,8,10,12},xtick={11,15,20,25,30,35,40,45,48},grid=major,grid style={asline!60},193 legend style={at={(0.98,0.05)},anchor=south east,font=\footnotesize,draw=asline,fill=white,row sep=-1pt},194 axis line style={asstone},tick label style={font=\footnotesize},label style={font=\small},195 every axis plot/.append style={line width=0.7pt}]196\addplot[asstone,dashed,line width=0.6pt] coordinates {(10,12) (49,12)};197\addlegendentry{published upper bound $12$ (all $n\ge 11$)}198\addplot[asstone,densely dotted,line width=0.6pt] coordinates {(15,6) (49,6)};199\addlegendentry{published lower bound $6$ ($n\ge 15$)}200\addplot[asline,only marks,mark=triangle*,mark size=2.6pt,mark options={fill=asline,draw=asstone}] coordinates {""" + " ".join(f"({n},{z})" for n, z in ub if n <= 22) + r"""};201\addlegendentry{best published upper bound, $n\le 22$}202\addplot[asblue,only marks,mark=square*,mark size=2.6pt] coordinates {""" + " ".join(f"({n},{z})" for n, z in known) + r"""};203\addlegendentry{exact value known before (see text)}204\addplot[asaccent,only marks,mark=*,mark size=2.4pt] coordinates {""" + " ".join(f"({n},{z})" for n, z in new) + r"""};205\addlegendentry{exact value certified here (new to our knowledge)}206\addplot[asgold,only marks,mark=o,mark size=4.2pt,line width=0.9pt] coordinates {""" + " ".join(f"({n},{z})" for n, z in hold) + r"""};207\addlegendentry{pre-registered holdout $n$}208\draw[asaccent,line width=0.5pt] (axis cs:22.5,2) -- (axis cs:22.5,13.5);209\node[anchor=north west,font=\footnotesize,text=asaccent] at (axis cs:22.7,13.4) {$n_0=23$: $Z=12$ for all $n\ge 23$ (Theorem~\ref{thm:main})};210\end{axis}211\end{tikzpicture}"""212compile_tex("fig3_exact_values", body.replace("(Theorem~\\ref{thm:main})", "(Theorem 1.1)"))213214# ------------------------------------------------------------------ Fig 4: obstruction at n = 25, p = 18215ob = next(c for c in cex if c.get("type") == "boundary_obstruction" and c["n"] == 25 and c["p"] == 18)216X = [parse(x) for x in ob["X"]]217B = [parse(x) for x in ob["boundary"]]218# independent recount of the boundary219Bchk = set()220for v in X:221 for w in nbrs(25, 5, v):222 if w not in set(X):223 Bchk.add(w)224assert Bchk == set(B) and len(B) == 10 and len(X) == 18, "obstruction recount failed"225fill = {v: "asaccent" for v in X}226fill.update({v: "asstone" for v in B})227legend = ("\\node[anchor=north,align=left,text width=7.6cm] at (0,-3.6) {\\footnotesize rust $=X$ ($|X|=18$: the two inner pentagons $\\{v_i: i\\equiv 0,1 \\pmod 5\\}$ and the eight outer vertices $u_i$, $i\\equiv 0,1 \\pmod 5$, $i\\ne 0,21$);\\ "228 "grey $=\\partial X$ ($|\\partial X|=10$); every other vertex has no neighbour in $X$};")229compile_tex("fig4_obstruction_P25_5", petersen_tikz(25, 5, fill=fill, R=3.0, r=1.75, node_r="5pt", show_index=False, legend=legend))230231# ------------------------------------------------------------------ Fig 5a: boundary window scaling232w = [(int(r["n"]), float(r["solve_seconds"]), float(r["check_seconds"]), int(r["proof_lines"])) for r in window if int(r["n"]) >= 26]233body = r"""\begin{tikzpicture}234\begin{axis}[width=13.5cm,height=6.5cm,xlabel={$n$ (certified window $26\le n\le 154$, $p=18$)},ylabel={seconds},235 xmin=24,xmax=156,ymin=0,ymax=290,grid=major,grid style={asline!60},axis line style={asstone},236 tick label style={font=\footnotesize},label style={font=\small},237 legend style={at={(0.02,0.97)},anchor=north west,font=\footnotesize,draw=asline,fill=white},238 axis y line*=left]239\addplot[asaccent,only marks,mark=*,mark size=1.3pt] coordinates {""" + " ".join(f"({n},{s})" for n, s, c, p in w) + r"""};240\addlegendentry{CaDiCaL 1.9.5 solve time (UNSAT, DRAT logging)}241\addplot[asblue,only marks,mark=square*,mark size=1.3pt] coordinates {""" + " ".join(f"({n},{c})" for n, s, c, p in w) + r"""};242\addlegendentry{drat-trim verification time}243\end{axis}244\begin{axis}[width=13.5cm,height=6.5cm,xmin=24,xmax=156,ymin=0,ymax=5.5,axis y line*=right,axis x line=none,245 ylabel={DRAT proof lines ($10^6$)},tick label style={font=\footnotesize},label style={font=\small},246 legend style={at={(0.02,0.80)},anchor=north west,font=\footnotesize,draw=asline,fill=white},axis line style={asstone}]247\addplot[asstone,only marks,mark=triangle*,mark size=1.4pt] coordinates {""" + " ".join(f"({n},{p/1e6:.3f})" for n, s, c, p in w) + r"""};248\addlegendentry{proof length}249\end{axis}250\end{tikzpicture}"""251compile_tex("fig5a_window_scaling", body)252253# ------------------------------------------------------------------ Fig 5b: exhaustive enumeration cost254Z = {n: int(exact[n]["Z"]) for n in exact}255bfrows = [(int(r["n"]), int(r["s"]), float(r["wall_seconds"]), int(r["subsets"])) for r in bf]256pts = [(n, t, sub) for n, s, t, sub in bfrows if n >= 17 and s == Z[n] - 1]257body = r"""\begin{tikzpicture}258\begin{semilogyaxis}[width=13.5cm,height=6.5cm,xlabel={$n$},ylabel={wall-clock seconds (16 threads)},xmin=16,xmax=28,ymin=0.1,ymax=3000,259 grid=major,grid style={asline!60},axis line style={asstone},tick label style={font=\footnotesize},label style={font=\small},260 legend style={at={(0.02,0.97)},anchor=north west,font=\footnotesize,draw=asline,fill=white},xtick={17,...,27}]261\addplot[asaccent,mark=*,mark size=1.8pt,line width=0.7pt] coordinates {""" + " ".join(f"({n},{t})" for n, t, sub in pts) + r"""};262\addlegendentry{$D_n$-orbit enumeration of all $(Z-1)$-subsets (C oracle)}263\end{semilogyaxis}264\begin{semilogyaxis}[width=13.5cm,height=6.5cm,xmin=16,xmax=28,ymin=1e6,ymax=1e12,axis y line*=right,axis x line=none,265 ylabel={subsets of size $Z-1$},tick label style={font=\footnotesize},label style={font=\small},axis line style={asstone},266 legend style={at={(0.02,0.82)},anchor=north west,font=\footnotesize,draw=asline,fill=white}]267\addplot[asstone,mark=triangle*,mark size=1.8pt,line width=0.6pt,dashed] coordinates {""" + " ".join(f"({n},{sub})" for n, t, sub in pts) + r"""};268\addlegendentry{$\binom{2n}{Z-1}$}269\end{semilogyaxis}270\end{tikzpicture}"""271compile_tex("fig5b_enumeration_scaling", body)272273# ------------------------------------------------------------------ Fig 6: heat map of beta_p(n)274cols = [c for c in btab[0].keys() if c != "p"]275cw, ch = 0.62, 0.5276L = ["\\begin{tikzpicture}"]277for ri, r in enumerate(btab):278 p = int(r["p"])279 y = -ri * ch280 L.append(f"\\node[anchor=east,font=\\footnotesize] at (-0.15,{y:.2f}) {{{p}}};")281 for ci, c in enumerate(cols):282 x = ci * cw283 v = r[c]284 if v.startswith(">="):285 colr, txt, tcol = "asaccent", "$\\ge$12", "white"286 else:287 val = int(v)288 shade = int(8 + (val - 2) * 6) # 2 -> 8%, 11 -> 62%289 colr, txt, tcol = f"asblue!{shade}", str(val), ("white" if shade > 45 else "asink")290 L.append(f"\\fill[{colr}] ({x:.2f},{y - ch/2:.2f}) rectangle ({x + cw:.2f},{y + ch/2:.2f});")291 L.append(f"\\node[font=\\footnotesize,text={tcol}] at ({x + cw/2:.2f},{y:.2f}) {{{txt}}};")292for ci, c in enumerate(cols):293 L.append(f"\\node[anchor=south,font=\\footnotesize] at ({ci*cw + cw/2:.2f},{ch/2 + 0.05:.2f}) {{{c}}};")294L.append(f"\\node[anchor=south,font=\\small] at ({len(cols)*cw/2:.2f},{ch/2 + 0.42:.2f}) {{$n$}};")295L.append(f"\\node[anchor=east,font=\\small,rotate=90] at (-0.75,{-(len(btab)-1)*ch/2:.2f}) {{$p$}};")296# highlight n = 25 column and the chosen (p=18, n>=26) region297i25 = cols.index("25")298L.append(f"\\draw[asgold,line width=1.2pt] ({i25*cw:.2f},{ch/2:.2f}) rectangle ({(i25+1)*cw:.2f},{-(len(btab)-1)*ch - ch/2:.2f});")299ip = [int(r["p"]) for r in btab].index(18)300i26 = cols.index("26")301L.append(f"\\draw[asink,line width=1.0pt,dashed] ({i26*cw:.2f},{-ip*ch + ch/2:.2f}) rectangle ({len(cols)*cw:.2f},{-ip*ch - ch/2:.2f});")302L.append(f"\\node[anchor=north,font=\\footnotesize,align=left,text width={len(cols)*cw-0.2:.1f}cm] at ({len(cols)*cw/2:.2f},{-(len(btab)-1)*ch - ch/2 - 0.15:.2f}) "303 "{cell $=\\beta_p(n)$, the minimum boundary of a $p$-set in $P(n,5)$; rust $=$ certified $\\ge 12$ (DRAT); "304 "gold frame $= n=25$, where every $p\\le 24$ fails; dashed $=$ the row $p=18$, $n\\ge 26$ used in the proof};")305L.append("\\end{tikzpicture}")306compile_tex("fig6_boundary_heatmap", "\n".join(L))307308print("all figures built")309