""" chain.py -- does extending a gate's graph chain gates, or free them? QUESTION. compose.py read 169 hard triples off the point E's reach and 22 on it, each a unit and two of its own ancestors. Extended by one and by two units, does a hard triple come apart, and does a gate's output become another gate's input? BY HAND (frozen before code). RF at T is Up and Down on the drop vector: Up, each head-to-sink path's delays at most T, up-closed in drops, its scope a chain; Down, each unit alive, down-closed in drops (a unit's leftover reads only its cone, rises with L and each inset, and a unit at floor is alive whatever its insets), its scope a unit and its cone. Three pairwise incomparable units share no path clause: an apart hard triple needs a common descendant over all three forced to drop by a path that misses them, a corner two new units build. But a kill on apartness (no apart hard triple, no composition) leans on apartness being needed, and it is not: a circuit's gate o = NAND(a, b) has o over a and b, and circuit satisfiability is a CSP of such nested triples. Composing needs a gate whose output is of its inputs' kind. A GATE is a hard triple one of whose units is a function of the other two, those two reading all four patterns; with 000 and 111 out, f(0, 0) = 1 and f(1, 1) = 0, and f = NOT of one input is binary, so a hard gate is NAND or NOR, each complete. Its output need not be the top: a path triple u1 < u2 < u3 reading {001, 010, 100, 101} is u2 = NOR(u1, u3). A CHAIN at one (graph, T): gates (a, b) -> o and (c, d) -> o2, o in {c, d}, o2 not in {a, b, o}; inputs I = {a, b} and {c, d} less o (fan-out allowed). STRICT where the relation on I reads all 2^|I| patterns (each gate's own relation already makes its output a function at every point), LOOSE otherwise. DESIGN. The base graphs are re-listed by compose.py's census (X6 at the 441 cells, X7 at the four), every (cell, units) with a hard triple at some T. Each is extended by one unit (an unordered pair from fresh and its units, fresh twice skipped) and by two (the second's pair from fresh, the units and the first; the first a fresh head only when the second reads it), deduplicated by dags.canonical per cell, a list the cell's ranges reject skipped. RF (compose.rf_rows) is read at every T from the graph's naive - 1 down while non-empty. PREDICTIONS. Loose chains exist (moderately); strict chains exist (weakly: fan-out lets the second gate reuse the first's inputs); no apart hard triple (moderately). KILL (frozen). "KILL strict chains: N (extended graphs M, gates G)", over the extensions; fires if N == 0 (gates do not chain at this scale); UNREADABLE if G == 0 or M < 100. Beside: loose chains, hard triples by kind (nested: one unit's cone holds the other two; partly: not nested, some pair comparable; antichain), gates by output position and kind, the same over the base graphs. CONTROLS. K0 synthetic: x0, x1, x2 free, x3 = NAND(x0, x1), x4 = NOR(x3, x2) reads one strict chain; the plant, the points with x0 = x1 = x2 = 0 removed, reads no strict chain. K1 the path triple reads one gate, NOR, output the middle. K2 the re-listing's hard triples sum to 169 off and 22 on. K3 the gate graph's 6-unit prefix, extended by one unit, holds the gate graph's class, which reads a NAND gate at T = 7. K4 ukind reads a head as a head (added on review, its planted break the old label). K5 a print: compose.py's c1 and c2. FINDINGS (copied from the runs below). K0 gates [(0, 1, 3, NAND), (2, 3, 4, NOR)], chains (loose 1, strict 1), the plant (1, 0); K1 [(0, 2, 1, NOR)]; K2 169 off, 22 on, over 182 base graphs ((4, 2, 2) 30, (11, 3, 8) 61, (6, 2, 4) 61, (8, 2, 6) 30); K3 21 one-unit extensions, the gate graph among them, its gate (1, 2, 6) NAND. Extensions 63,410 (9 units 60,116, 8 units 3,291, 7 units 3), RF sets 122,781. Hard triples nested 58,695, partly 3 (all at (4, 2, 2): a unit over one of the other two, the third comparable to neither; none a gate), antichain 0. Gates 45,687: NOR, output not top, 36,056; NOR, top, 8,629; NAND, top, 1,002 (no NAND whose output is not the top). Loose chains 0, strict 0. Base graphs: 363 sets, 191 hard triples, all nested; 157 gates, 0 chains. KILL strict chains: 0 (extended graphs 63410, gates 45687). FIRES, against the weak prediction; loose chains none either, against the moderate one; no antichain hard triple, as moderately predicted. Read as a hard triple no unit's cone holds the other two of, apartness reads the 3 partly nested; read as an antichain (BY HAND's "no apart hard triple"), it reads 0. Scope: the family is the 182 graphs (6 or 7 units, four cells) that carry a hard triple in compose.py's census (X6 at the 441 cells, X7 at the four), plus at most two units; 7-unit graphs at the other cells, bases of 8 or more units, a second gate needing three or more new units, a base with no hard triple, and functional triples tractable alone yet hard together are unread. Added after the kill was read (prints by read_graph and ukind): of the sets with a hard triple, 12,018 hold no gate, 41,584 one, 1,865 two, 122 three or more (so 1,987 sets could hold a chain); pairs of gates in one set share an input 2,244 times (fan-out exists) and an output 1,580 times, an output of one as an input of the other 0 times. Gate inputs sit at (z, h) units (10,637), inner units of floor 1 or 2 (8,791; 57,205) and sinks (14,741); outputs at inner units of floor 1 or 2 (4,808; 35,914) and sinks of floor 1 (4,965): the two roles share unit kinds, yet no unit holds both in one set. K5: compose.py's c1 at T = 8 has hard (1, 6, 8) and (2, 6, 8), no gate; c2 at T = 7 two NAND gates side by side, (1, 2, 6) and (7, 8, 12), no chain. So in this family gates fan out but never feed each other. RUN RECORD. Controls 4/4, 0.0 s. The base census, four shards, 41.8 to 43.0 s, peak commit 31.4 MB; the plan 38.5 s, peak 124.7 MB. Rehearsed at 50 graphs a shard, 0.1 s. Four shards, 11.3 to 11.4 s, peak commit 99.3 to 99.9 MB in the last run (run four times as prints were added and after the head label's fix; every count reproduced). Rerun from code/: controls 4/4, 0.1 s, 18.4 MB. """ import itertools import json import os import sys import time from collections import Counter os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") import dags # noqa: E402 import graphs # noqa: E402 from compose import (C1, C2, at, cone, cond, hard_triples, # noqa: E402 heads_feed_zh, rf_rows) from minclose import cell_named # noqa: E402 from pairwise import jobs, seven # noqa: E402 from schaefer import NAND1, classes_of # noqa: E402 CHECKS = [] def check(name, ok, detail=""): CHECKS.append(bool(ok)) tail = f" ({detail})" if detail else "" print(f" {'PASS' if ok else 'FAIL'} {name}{tail}") def drops(P, floors): return {tuple(int(x < f) for x, f in zip(p, floors)) for p in P} def hard_of(D): """The hard triples of a drop set, compose.hard_triples' test.""" out = [] for U in itertools.combinations(range(len(next(iter(D)))), 3): R = {tuple(x[u] for u in U) for x in D} if (0, 0, 0) not in R and (1, 1, 1) not in R and not classes_of(R): out.append(U) return out def gates(D, H): """[(a, b, o, kind)] over hard triples H: o a function of (a, b), (a, b) reading all four patterns; kind NAND or NOR.""" out = [] for U in H: for i in range(3): o = U[i] a, b = [u for u in U if u != o] f = {} ok = True for x in D: k = (x[a], x[b]) if f.setdefault(k, x[o]) != x[o]: ok = False break if ok and len(f) == 4: kind = "NAND" if f[(0, 1)] == 1 else "NOR" out.append((a, b, o, kind)) return out def chains(D, G): """(loose, strict) counts of ordered gate pairs g1 -> g2.""" loose = strict = 0 for a, b, o, _ in G: for c, d, o2, _ in G: if o not in (c, d) or o2 in (a, b, o): continue loose += 1 I = sorted({a, b} | ({c, d} - {o})) if len({tuple(x[u] for u in I) for x in D}) == 2 ** len(I): strict += 1 return loose, strict def kind(d, U): cones = {u: cone(d, u) for u in U} if any(set(U) - {u} <= cones[u] for u in U): return "nested" if any(v in cones[u] for u in U for v in U if u != v): return "partly" return "antichain" def ukind(d, u): """A unit's place: head, (z, h) (fresh and a head), sink, or inner, with its floor.""" a, b = d.units[u] heads = {j for j, x in enumerate(d.units) if tuple(x) == (None, None)} ins = {a, b} - {None} zh = None in (a, b) and len(ins) == 1 and ins <= heads place = ("head" if u in heads else "(z, h)" if zh else "sink" if not d.readers[u] else "inner") return f"{place}, floor {d.Ls[u]}" def read_graph(d, out, first, tag): nv = d.naive() rows = rf_rows(d, nv - 1) for T in range(nv - 1, -1, -1): P = at(rows, T) if not P: break out[f"{tag} sets"] += 1 H = hard_triples(P, d.Ls) if not H: continue D = drops(P, d.Ls) for U in H: out[f"{tag} hard {kind(d, U)}"] += 1 G = gates(D, H) for a, b, o, k in G: for role, u in (("in", a), ("in", b), ("out", o)): out[f"{tag} gate {role} units: {ukind(d, u)}"] += 1 top = {a, b} <= cone(d, o) out[f"{tag} gates {k}, output {'top' if top else 'not top'}"] += 1 lo, st = chains(D, G) out[f"{tag} sets with gates {min(len(G), 3)}"] += 1 for g, h in itertools.combinations(G, 2): for role in ("in in", "in out", "out out"): gi = set(g[:2]) if role != "out out" else {g[2]} hi = set(h[:2]) if role == "in in" else {h[2]} if role == "in out": x = bool(gi & hi) or g[2] in h[:2] else: x = bool(gi & hi) out[f"{tag} gate pairs sharing {role}"] += x out[f"{tag} gates"] += len(G) out[f"{tag} loose"] += lo out[f"{tag} strict"] += st if (st or any(kind(d, U) != "nested" for U in H)) and \ sum(f[0] == tag for f in first) < 6: first.append([tag, graphs.name(d.cell), d.units, T, nv, d.Ls, [list(g) for g in G][:6], lo, st, [[list(U), kind(d, U)] for U in H][:6]]) def controls(): print("K0, K1, K3 the instrument") D = set() for x0, x1, x2 in itertools.product((0, 1), repeat=3): x3 = 1 - (x0 & x1) D.add((x0, x1, x2, x3, 1 - (x3 | x2))) plant = {x for x in D if x[:3] != (0, 0, 0)} G, Gp = gates(D, hard_of(D)), gates(plant, hard_of(plant)) check("K0 NAND then NOR reads a strict chain; less the 000 inputs, none", chains(D, G)[1] >= 1 and chains(plant, Gp)[1] == 0, f"gates {G}; chains {chains(D, G)}; plant {chains(plant, Gp)}") P = {(0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 0, 1)} G1 = gates(P, [(0, 1, 2)]) check("K1 the path triple is u2 = NOR(u1, u3)", G1 == [(0, 2, 1, "NOR")], f"{G1}") cell = cell_named("(4, 2, 2)") want = dags.canonical(NAND1) ext = extensions(list(NAND1[:6]), cell, two=False) d = dags.Dag(cell, want) Hd = hard_triples(at(rf_rows(d, 7), 7), d.Ls) Gd = gates(drops(at(rf_rows(d, 7), 7), d.Ls), Hd) check("K3 the prefix's one-unit extensions hold the gate graph, which " "reads a NAND gate at T = 7", want in ext and any(g[3] == "NAND" for g in Gd), f"{len(ext)} extensions; {Gd}") kinds = [ukind(d, u).rsplit(", floor", 1)[0] for u in range(3)] check("K4 ukind: unit 0 a head, units 1 and 2 (z, h)", kinds == ["head", "(z, h)", "(z, h)"], f"{kinds}") for nm, units in (("c1", C1), ("c2", C2)): dc = dags.Dag(cell, units) rows = rf_rows(dc, dc.naive() - 1) for T in range(dc.naive() - 1, -1, -1): P = at(rows, T) if not P: break H = hard_triples(P, dc.Ls) G = gates(drops(P, dc.Ls), H) print(f" K5 {nm} T = {T}: RF {len(P)}, hard {H}, gates {G}, " f"chains {chains(drops(P, dc.Ls), G)}") def extensions(units, cell, two=True): """The classes of units extended by one unit, and by two.""" n = len(units) out = set() def ok(us): try: dags.Dag(cell, us) return True except AssertionError: return False def pairs(m): xs = [None] + list(range(m)) return [(x, y) for x, y in itertools.combinations_with_replacement( xs, 2) if x is None or y is None or x != y] for p in pairs(n): if p != (None, None) and ok(units + [p]): out.add(dags.canonical(units + [p])) if not two: continue for q in pairs(n + 1): if p == (None, None) and n not in q: continue if ok(units + [p, q]): out.add(dags.canonical(units + [p, q])) return out def base_shard(shard, ncells): out, rec, conds = Counter(), {}, {} t0 = time.time() for tag, cell, cls in jobs(shard, ncells, seven()): if tag not in ("X6", "X7"): continue nm = graphs.name(cell) if nm not in conds: conds[nm] = cond(cell) for units in cls: try: d = dags.Dag(cell, units) except AssertionError: continue nv = d.naive() rows = rf_rows(d, nv - 1) prot = conds[nm] and heads_feed_zh(d) for T in range(nv - 1, -1, -1): P = at(rows, T) if not P: break H = hard_triples(P, d.Ls) if not H: continue arm = "on" if prot and T == nv - 1 else "off" out[arm] += len(H) key = json.dumps([nm, [list(u) for u in units]]) rec.setdefault(key, Counter())[arm] += len(H) return out, {k: dict(v) for k, v in rec.items()}, time.time() - t0 def plan(base_paths, path): out, rec = Counter(), {} for p in base_paths: with open(p, encoding="utf-8") as fh: r = json.load(fh) out.update(r["out"]) rec.update(r["rec"]) print(f" {os.path.basename(p)}: {r['secs']:.1f} s") print(f" base graphs {len(rec)}: by cell " f"{dict(Counter(json.loads(k)[0] for k in rec))}") for k, v in sorted(rec.items()): print(f" {k} {v}") check("K2 the re-listing's hard triples: 169 off, 22 on", out["off"] == 169 and out["on"] == 22, f"{dict(out)}") t0 = time.time() base = {} ext = {} for k in rec: nm, units = json.loads(k) units = [tuple(u) for u in units] base.setdefault(nm, set()).add(dags.canonical(units)) ext.setdefault(nm, set()).update( extensions(units, cell_named(nm))) jobs_ = [] for nm in sorted(ext): for c in sorted(ext[nm] - base[nm], key=str): jobs_.append([nm, [list(u) for u in c]]) bjobs = [[nm, [list(u) for u in c]] for nm in sorted(base) for c in sorted(base[nm], key=str)] print(f" extensions {len(jobs_)} (by size " f"{dict(Counter(len(j[1]) for j in jobs_))}), " f"{time.time() - t0:.1f} s") with open(path, "w", encoding="utf-8", newline="\n") as fh: json.dump({"ext": jobs_, "base": bjobs}, fh) def ext_shard(plan_path, shard, limit): with open(plan_path, encoding="utf-8") as fh: pl = json.load(fh) out, first = Counter(), [] t0 = time.time() for tag in ("base", "ext"): js = pl[tag][shard::4] if limit: js = js[:limit] for nm, units in js: d = dags.Dag(cell_named(nm), [tuple(u) for u in units]) out[f"{tag} graphs"] += 1 read_graph(d, out, first, tag) return out, first, time.time() - t0 def report(paths): out, first = Counter(), [] for p in paths: with open(p, encoding="utf-8") as fh: r = json.load(fh) out.update(r["out"]) first += r["first"] print(f" {os.path.basename(p)}: {r['secs']:.1f} s") for k in sorted(out): print(f" {k}: {out[k]}") for f in first: print(f" {f}") N, M, G = out["ext strict"], out["ext graphs"], out["ext gates"] tail = " UNREADABLE" if G == 0 or M < 100 else "" print(f"KILL strict chains: {N} (extended graphs {M}, gates {G}){tail}") def dump(path, rec): with open(path, "w", encoding="utf-8", newline="\n") as fh: json.dump(rec, fh) def main(argv): t0 = time.time() if argv and argv[0] == "--bases": out, rec, secs = base_shard(int(argv[1]), int(argv[2])) dump(argv[3], {"out": dict(out), "rec": rec, "secs": secs}) print(f"bases shard {argv[1]}: {secs:.1f} s, {len(rec)} graphs") return 0 if argv and argv[0] == "--plan": plan(argv[2:], argv[1]) return 0 if all(CHECKS) else 1 if argv and argv[0] == "--ext": out, first, secs = ext_shard(argv[1], int(argv[2]), int(argv[3])) dump(argv[4], {"out": dict(out), "first": first, "secs": secs}) print(f"ext shard {argv[2]}: {secs:.1f} s") return 0 if argv and argv[0] == "--merge": report(argv[1:]) return 0 controls() if not all(CHECKS): print("\nCONTROL FAILED: nothing below is read.") return 1 print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s") return 0 if __name__ == "__main__": sys.exit(main(sys.argv[1:]))