""" glue.py -- do the least witness's clauses survive gluing? QUESTION. The least witness W at (6, 2, 4) (h, c = (z, h), r = (h, c)) forces one prime 3-unit clause in delays at latency 6, [L_h >= 3] or [L_c >= 3] or [L_r >= 2]. Glued twice, in parallel (one h, two (c, r) pairs) and in series (r1 as copy 2's head), does each copy keep its clause, and does the composite force anything the copies do not, read through the shared unit? DESIGN (frozen before code). F the composite's FD set at T (median.sets), F1, F2 its projections on each copy's units, S the shared unit, J = F1 joined to F2 on S. F lies in J; the join excess |J \\ F| counts what the copies do not imply. A copy is kept when its box (C2's, carried) is a prime clause of F (raises.clauses). Series copy 2's box: r1 at its hull low in F, c2 at its floor 2, r2 below its floor 1. Beside the kill, BUDGET-ONLY: is F the join of the uncapped alive set's projections, cut by the latency, so that r1's leftover carries copy 1 into copy 2 only through L_r1? PREDICTIONS. Parallel kept 2, excess 0 (by construction). Series: excess > 0 at its least latency, new clauses caps across the copies (the path budget); copy 1 lost there (weakly), copy 2 kept (weakly); BUDGET-ONLY holds (weakly). KILL (frozen). "KILL parallel: copy clauses kept K of 2, new N" and the same for series, N the join excess, at each gluing's least latency; fires if K < 2 or N > 0 in either. CONTROLS. G1 the bare witness at 6 reads exactly C2's clause, its join with itself excess 0. G2 parallel reads K = 2, N = 0 at every latency (a known yes: both copies are ancestor-closed). G3 a set of two points whose copies agree on the shared unit but vary apart reads its join excess, the two cross points, by hand. FINDINGS (copied from the run below). G1 the witness's one clause ((2, 2), (2, 2), (1, 1)), excess 0; G2 parallel off nowhere (latency 6 only); G3 the two cross points read. (First run: G3 deleted a point whose projections kept other witnesses, which reads excess 1 by construction; replaced at the audit.) Parallel, floors 2 each, least = naive = 6: |F| 5, |J| 5, excess 0, 6 prime 3-unit clauses, both copies kept (four more: resolvents through h, kinds R.D.C or C.R.D). Series, floors (2, 2, 2, 2, 1), least = naive = 9: |F| 4, |J| 4, excess 0, one prime 3-unit clause (copy 1's), copy 2's box lost: r2's hull is [1, 1], it never drops. BUDGET-ONLY 0 and 0. KILL parallel: copy clauses kept 2 of 2, new 0 KILL series: copy clauses kept 1 of 2, new 0 FIRES, on series copy 2's box only. Added after the kill was read, delays less floors at the least latency: parallel (0,0,0,0,0), (0,0,0,1,-1), (0,1,-1,0,0), (0,1,-1,1,-1), (1,0,-1,0,-1); series (0,0,0,0,0), (0,0,1,-1,0), (0,1,-1,0,0), (1,0,-1,0,0). So the predictions split: parallel as derived; series' excess 0 (predicted > 0, wrong: at its least latency r1 alone fixes copy 2's delays), copy 1 kept (predicted lost, wrong), BUDGET-ONLY held. Copy 2's drop moves to c2, guarded by r1 raised: a two-unit clause, the witness's mechanism one unit up. In both gluings each point's raises and drops cancel along every longest path (h, c, r of each copy; series' one path through all five), and the least latency is the naive one: the floors are alive there, so these clauses describe the set without making its emptiness a question. BELOW NAIVE (frozen after the gluing kill was read). Is that so of the census? raises.py's prime 3-unit clauses over the 990 non-median-closed FD sets of Y5 and X6, split by T < naive (dags.Dag asserts the floors alive at naive). KILL "D.R.R. clauses below naive: N (sets below naive M, their clauses K)", fires if N == 0, UNREADABLE if M == 0. Control B1: the split's totals are raises.py's. Predicted: below-naive sets a minority (moderately); D.R.R. among them (weakly). From the run: B1 990 sets, 3,063 clauses. At naive 933 sets, 2,997 clauses (C.C.C. 1,562, D.R.R. 915, C.D.R. 339, C.C.D. 157, C.C.R. 12, D.D.R. 9, C.D.D. 2, C.R.R. 1). Below naive 57 sets (X6 54, Y5 3), 66 clauses: D.R.R. 56 (X6 53, Y5 3), C.C.C. 6, C.D.R. 3, C.R.R. 1. KILL D.R.R. clauses below naive: 56 (non-median-closed sets below naive 57, their prime 3-unit clauses 66). MISSES; both predictions held. Where the latency is below naive the forced clauses are nearly all a drop guarded by two raises, and the caps nearly all sit at naive (1,562 of 1,568). The first D.R.R. below naive: X6, (6, 2, 4), heads h0, h1, u2 = (z, h0), u3 = (h0, u2), u4 = (h1, u3), u5 = (z, u4), T = 8 against naive 9, its clause on (h0, u2, u3) with sides (2, 2), (2, 2), (1, 1): the least witness's own clause, the witness read on by two units in a graph that gains. GUARDED GAINS (frozen after the census was read). A D.R.R. clause holds wherever r does not drop, so a set with a RAISE-FREE point (every unit at or below its floor) is decided by drops alone. Over every FD set below naive (Y4, Y5, X6), does some set hold none? KILL "below-naive FD sets with no raise-free point: N (M)", fires if N == 0. Control R1: the witness at 6 less its floors point reads none, with it one. Predicted N == 0 (moderately). From the run: R1 passes. KILL below-naive FD sets with no raise-free point: 101 (below-naive FD sets 3837). MISSES; the prediction was wrong. Added after the kill was read: X6 94, Y5 7, Y4 none; every one has a single minimal set of raised units (one unit in 100, two in 1), so the raise is forced and no gain offers a choice. By naive - T: X6 91 at 1, 3 at 2; Y5 7 at 1. The first: X6, (6, 2, 4), heads h0, h1, h2, u3 = (z, h0), u4 = (h0, h1), u5 = (h2, u3), T = 5 against naive 6, every point raising h2 to 3 or 4 and dropping u5 to 1: h2 arrives early, so its raise spends slack and buys the drop. A gain that needs a raise exists from 5 units; a gain guarded by an OR of raises, the choice a reduction would build a variable from, does not appear to 6 units at the three cells (to 5 at the 34). RUN RECORD. main: 3/3 checks, 0.0 s; under a memory cap, peak commit 19.2 MB. With BELOW NAIVE: 4/4 checks, 22.8 s, peak commit 20.1 MB. With GUARDED GAINS: 5/5 checks, 37.4 s, peak commit 20.6 MB. After the audit (G3 replaced, clauses and the gap split printed): 5/5 checks, 37.3 s, peak commit 20.6 MB. In code/: 5/5 checks, 37.5 s, 20.9 MB, every count above reproduced. """ import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") import dags # noqa: E402 import graphs # noqa: E402 import median # noqa: E402 import raises # noqa: E402 import sublattice as sl # noqa: E402 from minclose import cell_named # noqa: E402 CHECKS = [] CELL = "(6, 2, 4)" WITNESS = ((None, None), (None, 0), (0, 1)) # name, units, copies (unit indices, in witness order h, c, r), shared GLUES = ( ("parallel", ((None, None), (None, 0), (0, 1), (None, 0), (0, 3)), ((0, 1, 2), (0, 3, 4)), (0,)), ("series", ((None, None), (None, 0), (0, 1), (None, 2), (2, 3)), ((0, 1, 2), (2, 3, 4)), (2,)), ) 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 proj(P, U): return {tuple(p[u] for u in U) for p in P} def join(P, copies, shared): """The points of the full space whose projection on each copy lies in P's projection there (copies cover every unit).""" A, B = copies PA, PB = proj(P, A), proj(P, B) n = len(next(iter(P))) out = set() for a in PA: for b in PB: p = [None] * n ok = True for U, v in ((A, a), (B, b)): for u, x in zip(U, v): if p[u] is not None and p[u] != x: ok = False p[u] = x if ok: out.add(tuple(p)) return out def box(P, U, tops): """The clause box on units U, sides (hull low, top).""" return (tuple(U), tuple((min(p[u] for p in P), t) for u, t in zip(U, tops))) def wanted(name, P, copies): """The copies' boxes as frozen.""" out = [box(P, copies[0], (2, 2, 1))] if name == "parallel": out.append(box(P, copies[1], (2, 2, 1))) else: r1 = copies[1][0] lo = min(p[r1] for p in P) out.append(box(P, copies[1], (lo, 2, 0))) return out def new_clauses(P, J): """Prime 3-unit clauses of P whose box meets J's projection.""" out = [] for U, sides in raises.clauses(P): hit = any(all(s <= q[u] <= t for u, (s, t) in zip(U, sides)) for q in J) if hit: out.append((U, sides)) return out def controls(): print("G1..G3 the instrument") d = dags.Dag(cell_named(CELL), WITNESS) rows = sl.alive_all(d, d.naive()) P = median.sets(d, d.naive(), rows, 6)["FD"] cl = raises.clauses(P) want = [box(P, (0, 1, 2), (2, 2, 1))] ex = len(join(P, ((0, 1, 2), (0, 1, 2)), None) - P) check("G1 the bare witness at 6: exactly C2's clause, self-join " "excess 0", cl == want and ex == 0, f"{cl}, excess {ex}") name, units, copies, shared = GLUES[0] d = dags.Dag(cell_named(CELL), units) nv = d.naive() rows = sl.alive_all(d, nv) least = min(r[0] for r in rows) bad = [] for T in range(least, nv + 1): P = median.sets(d, nv, rows, T)["FD"] cl = set(raises.clauses(P)) K = sum(w in cl for w in wanted(name, P, copies)) N = len(join(P, copies, shared) - P) if (K, N) != (2, 0): bad.append((T, K, N)) check("G2 parallel: kept 2, excess 0 at every latency", not bad, f"latencies {least}..{nv}, off {bad}") # by hand: copy 1 {(0,0,0), (1,0,0)} and copy 2 {(0,0,0), (0,1,1)} # agree on unit 2 everywhere, so the join is their 2 x 2 product P = {(0, 0, 0, 0, 0), (1, 0, 0, 1, 1)} ex = sorted(join(P, ((0, 1, 2), (2, 3, 4)), None) - P) check("G3 a set whose copies vary apart: excess (0, 0, 0, 1, 1), " "(1, 0, 0, 0, 0) by hand", ex == [(0, 0, 0, 1, 1), (1, 0, 0, 0, 0)], f"{ex}") def budget_only(d, copies, T): """Points of (A1 joined A2, cut at latency T) not in F, and the reverse, A the uncapped alive set (delays, arrivals).""" rows = sl.alive_all(d, 10 ** 6) A = {r[1]: r[0] for r in rows} full = set(A) J = join(full, copies, None) F = {p for p, lat in A.items() if lat <= T} # latency of a joined point: a series graph's path sum Jc = {p for p in J if sum(p) <= T} return len(Jc - F), len(F - Jc) def below_naive(): """raises.py's census split by T < naive (frozen after the gluing kill was read).""" from collections import Counter n = Counter() first = {} for tag, cls, cells_ in median.populations(): if tag == "Y4": continue for cell in cells_: for units in cls: d = dags.Dag(cell, units) nv = d.naive() rows = sl.alive_all(d, nv) least = min(r[0] for r in rows) for T in range(least, nv + 1): P = median.sets(d, nv, rows, T)["FD"] if len(P) < 3 or median.fast(P)[0]: continue arm = "below" if T < nv else "naive" n[(arm, "sets")] += 1 # added after the kill was read: by population n[("pop", arm, tag)] += 1 for cl in raises.clauses(P): tg = raises.kinds(P, d.Ls, cl) pat = "".join(sorted(t.ljust(2, ".") for t in tg)) n[(arm, "clauses")] += 1 n[(arm, pat)] += 1 n[("pop", arm, tag, pat)] += 1 if arm == "below": first.setdefault(pat, (tag, graphs.name(cell), units, T, nv, cl)) for arm in ("naive", "below"): pats = {k[1]: v for k, v in sorted(n.items()) if k[0] == arm and k[1] not in ("sets", "clauses")} pop = {k[2:]: v for k, v in sorted(n.items()) if k[0] == "pop" and k[1] == arm} print(f" {arm}: sets {n[(arm, 'sets')]}, prime 3-unit clauses " f"{n[(arm, 'clauses')]}, patterns {pats}") print(f" by population {pop}") for k in sorted(first): print(f" first below naive {k}: {first[k]}") tot_s = n[("naive", "sets")] + n[("below", "sets")] tot_c = n[("naive", "clauses")] + n[("below", "clauses")] check("B1 the split's totals are raises.py's 990 sets, 3,063 clauses", (tot_s, tot_c) == (990, 3063), f"{tot_s}, {tot_c}") M, K = n[("below", "sets")], n[("below", "clauses")] print(f"KILL D.R.R. clauses below naive: {n[('below', 'D.R.R.')]} " f"(non-median-closed sets below naive {M}, their prime 3-unit " f"clauses {K}){' UNREADABLE' if M == 0 else ''}") def raise_free(P, floors): """Does P hold a point with every unit at or below its floor?""" return any(all(x <= f for x, f in zip(p, floors)) for p in P) def guarded_gains(): """Every FD set below naive: does it hold a raise-free point (frozen after the census was read)?""" w = sorted(((2, 3, 1), (3, 2, 1))) check("R1 the witness less its floors point reads no raise-free " "point; with it, one", not raise_free(w, (2, 2, 2)) and raise_free(w + [(2, 2, 2)], (2, 2, 2))) from collections import Counter M = N = 0 first = None by, sizes, choice, gap = Counter(), Counter(), [], Counter() for tag, cls, cells_ in median.populations(): for cell in cells_: for units in cls: d = dags.Dag(cell, units) nv = d.naive() rows = sl.alive_all(d, nv) least = min(r[0] for r in rows) for T in range(least, nv): P = median.sets(d, nv, rows, T)["FD"] M += 1 if not raise_free(P, d.Ls): N += 1 # added after the kill was read: by population, # and the minimal sets of raised units (more # than one: a choice among raises) rs = {frozenset(u for u, (x, f) in enumerate(zip(p, d.Ls)) if x > f) for p in P} mins = [r for r in rs if not any(q < r for q in rs)] arm = "choice" if len(mins) > 1 else "forced" by[(tag, arm)] += 1 gap[(tag, nv - T)] += 1 sizes[max(len(r) for r in mins)] += 1 if len(mins) > 1 and not choice: choice.append((tag, graphs.name(cell), units, T, nv, sorted(sorted(r) for r in mins))) first = first or (tag, graphs.name(cell), units, T, nv, d.Ls, len(P), sorted(P)) if first: print(f" first with no raise-free point: {first}") print(f" by population: {dict(sorted(by.items()))}; largest minimal " f"raise set: {dict(sorted(sizes.items()))}; by naive - T: " f"{dict(sorted(gap.items()))}") if choice: print(f" first with a choice: {choice[0]}") print(f"KILL below-naive FD sets with no raise-free point: {N} " f"(below-naive FD sets {M}){' UNREADABLE' if M < 10 else ''}") def main(): t0 = time.time() controls() if not all(CHECKS): print("\nCONTROL FAILED: nothing below is read.") return 1 kill = {} for name, units, copies, shared in GLUES: d = dags.Dag(cell_named(CELL), units) nv = d.naive() rows = sl.alive_all(d, nv) least = min(r[0] for r in rows) print(f"\n{name} floors {d.Ls}, latencies {least}..{nv}, " f"copies {copies}, shared {shared}") for T in range(least, nv + 1): P = median.sets(d, nv, rows, T)["FD"] if len(P) < 2: print(f" T {T}: |F| {len(P)}") continue cl = raises.clauses(P) have = set(cl) ws = wanted(name, P, copies) kept = [w in have for w in ws] J = join(P, copies, shared) N = len(J - P) nc = new_clauses(P, J) print(f" T {T}: |F| {len(P)}, |J| {len(J)}, excess {N}, " f"prime 3-unit clauses {len(cl)}, kept {kept}") for w, k in zip(ws, kept): if not k: near = [c for c in cl if c[0] == w[0]] print(f" lost {w}; on its units: " f"{[(c, raises.kinds(P, d.Ls, c)) for c in near]}") for c in nc: print(f" new {c} {raises.kinds(P, d.Ls, c)}") # added at the audit: every prime 3-unit clause, by kind for c in cl: print(f" clause {c} {raises.kinds(P, d.Ls, c)}") if name == "series": over, under = budget_only(d, copies, T) print(f" BUDGET-ONLY: joined and cut, not in F {over}; " f"in F, not joined {under}") if T == least: kill[name] = (sum(kept), N) if T == least and N: print(f" the excess at the least latency: " f"{sorted(J - P)[:12]}") if T == least: # added after the kill was read: the set itself, and # each point's delays less the floors for p in sorted(P): print(f" F {p} less floors " f"{tuple(x - f for x, f in zip(p, d.Ls))}") print() for name in ("parallel", "series"): K, N = kill[name] print(f"KILL {name}: copy clauses kept {K} of 2, new {N}") fired = any(K < 2 or N > 0 for K, N in kill.values()) print("FIRES" if fired else "MISSES") print("\nBELOW NAIVE raises.py's census split by latency") below_naive() print("\nGUARDED GAINS every FD set below naive") guarded_gains() print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s") return 0 if __name__ == "__main__": sys.exit(main())