From a6601c213d9b143ab7452e88da6b474a4fa4a493 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 18 Sep 2026 13:26:56 +0000 Subject: [PATCH 1/2] Keep two measurement notes in the repo instead of nowhere MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both record work already done; neither changes any evidence or value. vdw/SIGMA-EQUIVARIANCE.md — the reversal map i -> n+1-i permutes colourings, which is all the lex-leader argument of PAPER.md 4.4 needs, but it is NOT an automorphism of the encoded CNF: the pysat totalizer builds its auxiliary tree over positions in a fixed left-to-right order, so 24 of 270 clauses at n=14/j=3 and 86 of 2221 at n=45/j=8 are not preserved. Every offender is a cardinality clause; the exactly-one and AP blocks are sigma-closed. Building the totalizer over the reversed input list gives exactly sigma applied to the forward one. The note leads with the fact that no published term is affected, and gives the evidence: 16 rungs x 3 symmetry configurations = 48 solves with 0 disagreements and every witness re-verified, plus 2052/2052 cube-level agreement on sat(F & cube) vs sat(F & sigma(cube)). It also records a claim that did NOT survive testing. An earlier draft asserted that sigma-renamed DRAT proofs are invalid yet drat-trim accepts them anyway. That was measured on a base formula which is itself UNSAT, where every VERIFIED is a true verdict and a wrong acceptance cannot be detected. Redone on a satisfiable base: 0 SAT targets verified, and a deliberately non-symmetric control was rejected 17 of 17. There is no checker bug, the note says so, and it is in the repo so the retraction is on the record rather than the accusation being left as a rumour. vdw/CENTRAL-CUBING.md — what the central-position cubing added earlier is actually worth. The premise partly reproduced: the prefix incidence figures are exact, the central ones are 252 and 213 rather than the 248 and 212 first claimed. Central beats the repo's prefix cubing by 1.50x-3.66x on conflicts, but section 7 states the honest baseline plainly -- cube-and-conquer at these sizes costs more conflicts than simply solving monolithically, so this narrows a self-inflicted regression rather than making cubing a faster way to compute values. Its value is on the certification path, where per-cube proofs are mandatory. Also adds one sentence to PAPER.md 4.4 pointing at the sigma note, since that is where a reader meets the reversal constraint. verify_all.py: 108 passed, 0 failed. scrub_paths.py --check: clean. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n --- PAPER.md | 8 + vdw/CENTRAL-CUBING.md | 297 ++++++++++++++++++++++++++++++++++++++ vdw/SIGMA-EQUIVARIANCE.md | 248 +++++++++++++++++++++++++++++++ 3 files changed, 553 insertions(+) create mode 100644 vdw/CENTRAL-CUBING.md create mode 100644 vdw/SIGMA-EQUIVARIANCE.md diff --git a/PAPER.md b/PAPER.md index bf07089..25f6e2d 100644 --- a/PAPER.md +++ b/PAPER.md @@ -178,6 +178,14 @@ common difference; it fixes every class and the wildcard count. Requiring a colouring to be lexicographically no greater than its own reversal is therefore a sound lex-leader constraint, and it halves the search space. +A note on what that soundness does and does not extend to: `i -> n+1-i` permutes +*colourings*, which is all a lex-leader needs, but it is **not** an automorphism +of the encoded CNF — the totalizer builds its auxiliary tree over positions in a +fixed left-to-right order, so 86 of 2221 clauses at `n=45, j=8` are not preserved. +That costs nothing here and no published value is affected, but it does rule out +transporting proofs between symmetric cubes by renaming. Measured in +`vdw/SIGMA-EQUIVARIANCE.md`. + This matters more than it might appear. The pre-existing implementation broke only the symmetry between classes *sharing* a target value. A217058 has targets `3` and `4`, which differ, so that rule emitted **no clauses at all** and every diff --git a/vdw/CENTRAL-CUBING.md b/vdw/CENTRAL-CUBING.md new file mode 100644 index 0000000..94b34d9 --- /dev/null +++ b/vdw/CENTRAL-CUBING.md @@ -0,0 +1,297 @@ +# Central-position cubing for vdw4 — what it is, what it is worth + +Private notes. Nothing here has been committed, pushed or published; the repo at +`/home/user/mathrecords` was never modified (`git status --porcelain` empty at start and +at finish). The patch lives beside this file as `central-cubing.patch` and applies to +`vdw/vdw4.py` (`git apply --check` passes). + +Every number below was measured in this session on this machine, single-threaded, +in-process, with pysat's `Cadical195` and `s.accum_stats()`. Conflicts and propagations +are deterministic; wall-clock numbers are flagged where the box was shared. + +## Verdict in one paragraph + +The premise is essentially right and the patch's own claim reproduces: splitting on +central positions instead of a prefix costs **1.50x–3.66x fewer conflicts** across five +UNSAT instances in two families (2.10x–3.66x at k=6), and 3.24x fewer at the repo's +headline configuration (n=45, j=8, [3,4], k=6). But the honest baseline kills it as a way +to compute values: **cube-and-conquer with central splitting still costs 1.61x–5.30x more +conflicts than simply solving the formula monolithically**, at every size tested. Central splitting does not +turn cubing into a win, it makes a self-inflicted regression smaller. It is worth having +for the **certification path**, where per-cube proofs are mandatory and the monolithic +solve is not an option; there the patch cuts total proof work by ~3x and the hardest +single cube by 3.2x. It is not a way to reach a(13) faster. + +One wall-clock caveat that cuts the other way is recorded in §7 — do not skip it. + +## 1. What the patch does + +`vdw/vdw4.py` currently splits on the first k **positions**: `make_cubes()` enumerates +all class assignments of positions 1..k, drops a prefix that already contains a +monochromatic target-length AP, that blows the wildcard budget, or (optionally) that +violates the colour-symmetry rule. + +The patch adds, without touching `make_cubes()` or any existing default: + +- `ap_incidence(n, targets)` — how many target-length APs pass through each position. +- `split_positions(n, k, mode, targets)` — `'prefix'` (unchanged behaviour), + `'central'` (the middle window of k positions), `'incidence'` (the k positions of + highest AP incidence). +- `make_cubes_pos(n, j, targets, positions, colour_sym=False)` — `make_cubes()` + generalised to an arbitrary **set** of split positions. Cubes come back as tuples of + `(position, class)` pairs. A cube is dropped only when a clause already in `build()`'s + output refutes it: a monochromatic AP lying wholly inside the split positions, or more + than j wildcards among them. +- `_cube_pairs()` — accepts both cube shapes, so `_cube_job()` is a one-line change and + legacy flat prefix cubes keep working unchanged. +- `solve(..., split='prefix')` — new keyword; `'central'`/`'incidence'` route through + `make_cubes_pos`. Default behaviour is bit-for-bit what it was. + +`colour_sym=True` is **refused** off a prefix. See §4; this is the one place where a +careless port of the existing code would produce a false term. + +## 2. The premise: AP incidence (claim partly confirmed, numbers corrected) + +Claimed: central positions carry far more AP incidence than a prefix — "248 vs 144 at +t=3 and 212 vs 105 at t=4" at n=45. + +Measured at n=45, k=6 (sum over the six positions of the number of t-term APs through +each): + +| | t=3 | t=4 | +|---|---|---| +| prefix, positions 1..6 | **144** | **105** | +| central, positions 20..25 | **252** | **213** | +| claimed central | 248 | 212 | + +The prefix figures reproduce **exactly**. The central figures do not: I measure 252 and +213. I swept every contiguous 6-window at n=45. **No window at t=3 sums to 248** — the +maximum over all 40 windows is 252, attained at 20..25 and 21..26. At t=4, 212 does +occur, but only at the off-centre windows 15..20 and 26..31; every window from 17..22 +through 23..28 gives exactly 213, and 213 is the maximum. So one claimed figure is +unattainable and the other belongs to a window that is not central. The direction and +rough size of the effect (1.75x at t=3, 2.03x at t=4) are right, the figures are not. +Do not quote 248/212; the central k=6 values at n=45 are 252 and 213. + +Full profile at n=45, t=3: incidence rises 22, 22, 24, 24, ... to 44 at position 23 and +falls symmetrically. At t=4 it rises from 14 to ~36 and plateaus, oscillating between 35 +and 36 over the middle third — which is why 'central' and 'incidence' pick nearly the +same positions and behave nearly identically everywhere below. + +## 3. Cube sets are exhaustive and sound (checked, not argued) + +- **Tautology over the split positions.** For every configuration tried, I enumerated all + (r+1)^k assignments of the split positions and classified each one: it is a cube, or it + is refuted by a named clause of F (a monochromatic AP inside the split set, or the + wildcard cardinality bound). Zero uncovered branches, zero cubes kept that F refutes. + Checked at n=45 j=8 [3,4] for k=4, 6, 8 in all three modes (e.g. k=6 central: + 603 cubes + 126 AP-drops + 0 budget-drops = 729 = 3^6), and with a tight budget to + exercise the cardinality drop (n=45 j=3 k=8 central: 2914 + 2074 + 1573 = 6561), plus + n=35 j=2 [3,3] k=7 and n=55 j=4 [4,5] k=6 with a non-contiguous incidence set. +- **Cubes are pairwise disjoint** over the split positions (no assignment in two cubes). +- **Known witness lands in exactly one cube.** The n=44 j=8 [3,4] SAT colouring + (verified by `check`: 8 wildcards, no mono AP) falls in exactly 1 of the 603 cubes for + prefix, central and incidence splitting. +- **Prefix mode is byte-identical to the repo.** `make_cubes_pos` on positions 1..k + returns exactly `make_cubes(..., colour_sym=False)` across 2520 configurations + (5 target pairs x n in 10..49 x j in 0..8 x k in 3..6), 0 mismatches. + +## 4. The trap: do not port the colour-symmetry rule to a window + +`make_cubes()`'s `colour_sym` rule orders the **first occurrences** of interchangeable +colours. That is a statement about the whole word. Read off a central window it orders +first occurrences *within the window*, which is not a symmetry of F — a colouring may +legitimately start colour 1 outside the window and colour 2 inside it. + +This is not hypothetical. Measured: **[3,3] j=3 n=19 is SAT** (monolithic solve, 33 +conflicts; A217005 a(3)=20 so n=19 must be SAT). With a central k=6 window and the rule +ported naively, plus the formula's own colour-swap symmetry breaking, the cube set +returns **UNSAT** — a lost solution, i.e. exactly the failure mode that publishes a false +new term. With `build(symbreak=False)` the same cube set returns SAT, which is why the +bug can hide: it only bites when both symmetry breakings are on. + +The patch therefore raises `ValueError` if `colour_sym=True` is requested off a prefix. +Non-prefix splitting always runs with the rule off, which is what certification requires +anyway. + +## 5. Correctness: 13 OEIS rungs across four families, 0 disagreements + +Each rung solved through the cube path with the monolithic probe disabled, at k=6, in +prefix and central modes (plus incidence on the first six rungs); every SAT answer +re-verified by `check()`, which reads the colouring only and never the CNF. + +| family | j | a(j) | n=a(j)-1 | n=a(j) | +|---|---|---|---|---| +| A217058 [3,4] | 0,1,2,3,4,5 | 18,21,25,29,33,36 | SAT (verified) | UNSAT | +| A217005 [3,3] | 0,1,4,5 | 9,14,21,24 | SAT (verified) | UNSAT | +| A217007 [4,4] | 0,1 | 35,40 | SAT (verified) | UNSAT | +| A217059 [3,5] | 0 | 22 | SAT (verified) | UNSAT | + +Plus the two big ones used for benchmarking: n=44 j=8 [3,4] SAT (verified, 8 wildcards) +and n=45 j=8 [3,4] UNSAT, 2486 clauses, 1,396,228 conflicts — matching the recorded +baseline exactly. + +13 rungs, i.e. 26 instances (each a(j)-1 and a(j)). The first six rungs ([3,4] j=0..3, +[3,3] j=0,1) were run in all three modes, the remaining seven in prefix and central: +64 solved instances in total, 0 disagreements with OEIS and 0 failed `check()` +verifications. + +## 6. Benchmark (a): central vs the repo's prefix cubing — the claim holds + +Sum of conflicts and propagations over the whole cube set, every cube solved (no early +exit), fresh solver per cube with the cube as assumptions, i.e. the repo's own +`_cube_job` shape. + +| instance | k | split | cubes | conflicts (sum) | propagations (sum) | vs prefix | vs monolithic | +|---|---|---|---|---|---|---|---| +| **n=33 j=5 [3,3]** | - | **monolithic (no cubes)** | - | 4,710 | 235,763 | - | 1.00x | +| n=33 j=5 [3,3] | 4 | prefix | 71 | 18,958 | 1,019,491 | 1.00x | 4.03x worse | +| n=33 j=5 [3,3] | 4 | central | 71 | 10,568 | 598,164 | 1.79x | 2.24x worse | +| n=33 j=5 [3,3] | 4 | incidence | 71 | 10,568 | 598,164 | 1.79x | 2.24x worse | +| n=33 j=5 [3,3] | 6 | prefix | 522 | 40,803 | 2,266,556 | 1.00x | 8.66x worse | +| n=33 j=5 [3,3] | 6 | central | 522 | 19,419 | 1,130,300 | 2.10x | 4.12x worse | +| n=33 j=5 [3,3] | 6 | incidence | 510 | 19,640 | 1,151,517 | 2.08x | 4.17x worse | +| **n=35 j=6 [3,3]** | - | **monolithic (no cubes)** | - | 9,117 | 437,345 | - | 1.00x | +| n=35 j=6 [3,3] | 4 | prefix | 71 | 34,635 | 1,886,134 | 1.00x | 3.80x worse | +| n=35 j=6 [3,3] | 4 | central | 71 | 23,151 | 1,350,224 | 1.50x | 2.54x worse | +| n=35 j=6 [3,3] | 4 | incidence | 71 | 22,770 | 1,351,656 | 1.52x | 2.50x worse | +| n=35 j=6 [3,3] | 6 | prefix | 523 | 99,458 | 5,711,974 | 1.00x | 10.91x worse | +| n=35 j=6 [3,3] | 6 | central | 523 | 44,041 | 2,684,316 | 2.26x | 4.83x worse | +| n=35 j=6 [3,3] | 6 | incidence | 523 | 44,041 | 2,684,316 | 2.26x | 4.83x worse | +| **n=40 j=6 [3,4]** | - | **monolithic (no cubes)** | - | 175,224 | 6,410,524 | - | 1.00x | +| n=40 j=6 [3,4] | 4 | prefix | 75 | 1,485,102 | 64,414,700 | 1.00x | 8.48x worse | +| n=40 j=6 [3,4] | 4 | central | 75 | 712,483 | 34,247,977 | 2.08x | 4.07x worse | +| n=40 j=6 [3,4] | 4 | incidence | 75 | 712,483 | 34,247,977 | 2.08x | 4.07x worse | +| n=40 j=6 [3,4] | 6 | prefix | 603 | 3,818,704 | 197,439,174 | 1.00x | 21.79x worse | +| n=40 j=6 [3,4] | 6 | central | 603 | 1,043,755 | 61,068,250 | 3.66x | 5.96x worse | +| n=40 j=6 [3,4] | 6 | incidence | 603 | 1,043,755 | 61,068,250 | 3.66x | 5.96x worse | +| **n=42 j=7 [3,4]** | - | **monolithic (no cubes)** | - | 913,916 | 27,457,287 | - | 1.00x | +| n=42 j=7 [3,4] | 4 | prefix | 75 | 3,488,334 | 141,802,768 | 1.00x | 3.82x worse | +| n=42 j=7 [3,4] | 4 | central | 75 | 1,474,177 | 66,045,152 | 2.37x | 1.61x worse | +| n=42 j=7 [3,4] | 4 | incidence | 75 | 1,474,177 | 66,045,152 | 2.37x | 1.61x worse | +| n=42 j=7 [3,4] | 6 | prefix | 603 | 10,508,539 | 479,222,774 | 1.00x | 11.50x worse | +| n=42 j=7 [3,4] | 6 | central | 603 | 3,022,063 | 168,689,654 | 3.48x | 3.31x worse | +| n=42 j=7 [3,4] | 6 | incidence | 603 | 3,022,063 | 168,689,654 | 3.48x | 3.31x worse | +| **n=45 j=8 [3,4]** | - | **monolithic (no cubes)** | - | 1,396,228 | 42,924,439 | - | 1.00x | +| n=45 j=8 [3,4] | 4 | prefix | 75 | 8,424,168 | 327,348,082 | 1.00x | 6.03x worse | +| n=45 j=8 [3,4] | 4 | central | 75 | 2,984,075 | 130,827,127 | 2.82x | 2.14x worse | +| n=45 j=8 [3,4] | 4 | incidence | 76 | 2,946,820 | 128,255,068 | 2.86x | 2.11x worse | +| n=45 j=8 [3,4] | 6 | prefix | 603 | 23,980,575 | 1,031,616,290 | 1.00x | 17.18x worse | +| n=45 j=8 [3,4] | 6 | central | 603 | 7,402,577 | 363,200,098 | 3.24x | 5.30x worse | +| n=45 j=8 [3,4] | 6 | incidence | 597 | 7,554,095 | 368,396,939 | 3.17x | 5.41x worse | + +Central beats prefix in all ten comparisons: **1.50x–2.82x at k=4** (median 2.08x) and +**2.10x–3.66x at k=6** (median 3.24x). The reported "~2.10x" is in range — it is exactly +what I measure at k=4 on n=40 [3,4] (2.08x) and at k=6 on n=33 [3,3] (2.10x); at the +headline n=45 j=8 k=6 the gain is larger, 3.24x, and at the smallest [3,3] instance at +k=4 it is only 1.50x. + +`incidence` is not distinguishable from `central`: it picks the same or nearly the same +positions and lands within 2% everywhere. Not worth the extra code path on its own; it +is in the patch because it costs three lines and generalises to targets whose incidence +profile is not symmetric. + +**Why it works, and a caveat on the explanation.** A control at n=40 j=6 [3,4] k=4, +varying only the split positions: + +| positions | AP incidence | conflicts | +|---|---|---| +| 1,2,3,4 (prefix) | 140 | 1,485,102 | +| 37,38,39,40 (suffix) | 140 | 1,036,244 | +| 4,14,33,38 (random) | 186 | 1,177,417 | +| 5,7,24,35 (random) | 197 | 1,107,832 | +| 4,10,21,26 (random) | 226 | 914,304 | +| 10,11,12,13 (quarter) | 230 | 913,548 | +| 19,20,21,22 (central) | 276 | **712,483** | + +Conflicts fall broadly with incidence (the ordering is monotone once the two +equal-incidence endpoints are set aside) — but note the suffix: same incidence as the +prefix, 1.43x fewer conflicts. So incidence is not the whole story. Part of the prefix's +weakness is that it overlaps the reversal lex-leader constraint, which already pins down +the front of the word; fixing those same positions buys less new information. I did not +chase this further, and the write-up should not claim incidence is the sole mechanism. + +## 7. Benchmark (b): central cubing vs just solving it — the honest baseline + +Same table, last column. Against a single monolithic `Cadical195` call on the same +formula: + +| instance | monolithic | best cubing (central/incidence) | cubing penalty | +|---|---|---|---| +| n=33 j=5 [3,3] | 4,710 | 10,568 (k=4) | 2.24x worse | +| n=35 j=6 [3,3] | 9,117 | 22,770 (k=4) | 2.50x worse | +| n=40 j=6 [3,4] | 175,224 | 712,483 (k=4) | 4.07x worse | +| n=42 j=7 [3,4] | 913,916 | 1,474,177 (k=4) | 1.61x worse | +| n=45 j=8 [3,4] | 1,396,228 | 2,946,820 (k=4) | 2.11x worse | +| n=45 j=8 [3,4] | 1,396,228 | 7,402,577 (k=6) | 5.30x worse | + +In conflicts, cubing loses at every size tested, with or without the patch. The patch +narrows the loss (at n=45 k=6, from 17.2x to 5.3x) but never closes it. Deeper cubing is +worse, not better: k=6 costs 2.5x the conflicts of k=4 in central mode at n=45. + +**The wall-clock caveat.** Conflicts are not seconds. Measured serially on an otherwise +idle box, n=45 j=8 [3,4]: + +| run | conflicts | wall | +|---|---|---| +| monolithic (rep 1) | 1,396,228 | 79.8s | +| monolithic (rep 2) | 1,396,228 | 78.6s | +| central k=4, 75 cubes | 2,984,075 | **55.9s** | +| central k=6, 603 cubes | 7,402,577 | 114.9s | +| prefix k=4, 75 cubes | 8,424,168 | 212.6s | +| prefix k=6, 603 cubes | 23,980,575 | 472.6s | + +So at k=4, central cubing runs ~1.4x **faster** in wall-clock than the monolithic solve +despite 2.1x more conflicts: a cube's conflicts are cheaper than the monolithic run's, +whose learnt-clause database grows large. Single-threaded and at this one size. That is +one data point against my own summary, and it is the one worth re-testing before +anybody concludes cubing is useless here: with 4 workers the k=4 central cube path would +plausibly beat the monolithic solve outright in wall-clock. I did not measure the +parallel path (the repo's `ProcessPoolExecutor`), and the per-cube CNF rebuild in +`_cube_job` is included in these timings. + +The conflict-count statement ("cubing is a net loss") is therefore solid only as a +statement about search work, not about elapsed time. + +## 8. Where it does help: certification + +`cube_certify.py` needs a DRAT proof per cube — the monolithic solve is not an +alternative there, the per-cube work must happen. For that path the patch is a real, +unambiguous gain: + +- total per-cube work at n=45 j=8 k=6: 23,980,575 -> 7,402,577 conflicts (3.24x). +- hardest single cube at n=45 j=8 k=4: 323,555 -> 101,494 conflicts (3.19x). That is the + quantity that sets the makespan and the largest proof file. +- 4-core LPT makespan over the same cube set: 2,113,920 -> 752,196 conflicts (2.81x). + +**Limitation, not yet done.** The patch changes the search path only. `cube_certify.py` +and `cube_exhaustive.py` both call `make_cubes()` directly, parse cubes as flat class +tuples, and walk a prefix tree. Using central cubes for a certification run requires +extending those two files to the `(position, class)` shape and relabelling the tree walk. +That generalisation looks mechanical — the tree is the same (r+1)-ary tree with different +variable labels — but it is **not implemented and not tested here**, and the +exhaustiveness DRAT tail in particular must be re-derived and re-checked before any +certified value is claimed with central cubes. + +## 9. Plain statement of when to use it + +- Computing a new value of one of these sequences: **use the monolithic solve** + (`solve_direct`, or `solve(..., probe=...)` with a large budget). Cubing, prefix or + central, costs more search. The patch does not change that. +- Running the certification pipeline, where per-cube proofs are mandatory: **use + `split='central'`**, k=4 rather than k=6, after extending the two certification tools. + Expect ~3x less total work and ~3x smaller hardest cube. +- Never enable `colour_sym` with a non-prefix split. The patch refuses it; if you port + this code anywhere else, keep that refusal. +- Do not quote the incidence figures 248/212; they are 252/213. + +## 10. Reproducing + +Scripts used, all in `/tmp/claude-0/-home-user-Blank/cdf10545-c83e-52b1-ab18-ba0699ae1f41/scratchpad/cc/`: +`incid.py`, `incid2.py` (§2), `central.py` (the implementation, mirrored by the patch), +`exhaust.py`, `exhaust2.py`, `equiv.py` (§3), `csym_hazard.py` (§4), `rungs.py`, +`rungs2.py` (§5), `driver.py`, `bench_mid.py`, `bench45.py`, `control.py` (§6), +`makespan.py` (§8), `clean_wall.py`, `clean_wall2.py` (§7). Raw logs: `bench_mid.log`, +`bench45.log`. + +Environment: python 3.11.15, python-sat 1.9.dev15, Cadical195, 4 cores, 15 GB. diff --git a/vdw/SIGMA-EQUIVARIANCE.md b/vdw/SIGMA-EQUIVARIANCE.md new file mode 100644 index 0000000..f06cf60 --- /dev/null +++ b/vdw/SIGMA-EQUIVARIANCE.md @@ -0,0 +1,248 @@ +# The sigma-equivariance trap: a symmetric constraint with an asymmetric encoding + +Private note. Nothing here has been published, filed, or sent anywhere. +Every number below was measured in this session by +`/tmp/claude-0/-home-user-Blank/cdf10545-c83e-52b1-ab18-ba0699ae1f41/scratchpad/private-drafts/sigma_check.py` +and its companions (`sigma_drat.py`, `sigma_drat2.py`, `sigma_drat3.py`, +`sigma_scan.py`, `sigma_acid.py`). Nothing is copied from a previous run. + +--- + +## READ THIS FIRST: the published values are NOT affected + +**No published term of A217058, A217005, A217007, A217059 or A217236 is put in +doubt by anything in this note.** The finding is about a *proof-engineering* +technique that was never used to produce them. + +Two independent lines of evidence, both measured here. + +**(1) Verdicts are identical with and without the reversal lex-leader.** +16 rungs — j = 0..3 for `[3,4]` (A217058) and `[3,3]` (A217005), each at both +`n = a(j) - 1` (should be SAT) and `n = a(j)` (should be UNSAT) — solved three +ways: `(symbreak=False, revsym=False)`, `(True, False)`, `(True, True)`. +48 full solves, Cadical195, no cube split, no conflict budget. + +- disagreements between the three configurations: **0 / 16 rungs** +- verdicts matching the published sequences: **16 / 16** +- SAT witnesses re-verified by `vdw4.check` (reads only the colouring): **all pass** + +**(2) sigma is a semantic symmetry of the formula, cube by cube, exhaustively.** +Over 6 instances and **2052 cubes total**, comparing `sat(F & cube)` against +`sat(F & sigma(cube))` with `F` built symmetry-breaking-**off**: + +| instance | cubes | cubes where the two verdicts differ | +|---|---:|---:| +| n=24 j=2 `[3,4]` k=6 | 376 | **0** | +| n=28 j=3 `[3,4]` k=6 | 530 | **0** | +| n=33 j=4 `[3,4]` k=5 | 212 | **0** | +| n=19 j=3 `[3,3]` k=6 | 450 | **0** | +| n=16 j=2 `[3,3]` k=6 | 302 | **0** | +| n=20 j=3 `[3,3]` k=5 | 182 | **0** | + +Perfect agreement, 2052 for 2052. + +This is the whole point, and it is worth stating precisely because it is easy to +scare oneself with the headline finding below: + +> The paper's reversal argument is about the **colouring**, not about the CNF. +> Reversal maps valid colourings to valid colourings (it sends a *t*-term AP to a +> *t*-term AP and fixes the wildcard count), so requiring `colouring <=_lex +> reversal(colouring)` keeps at least one representative of every orbit and +> therefore preserves satisfiability. **That argument never needed sigma to be an +> automorphism of the CNF.** A lex-leader constraint needs the symmetry to act on +> the *solution set*; it does not care how the auxiliary variables are wired. + +So the headline finding is a real property of the encoding and a real obstacle to +one specific *optimisation*, and it has no bearing on the published numbers. + +--- + +## The finding: sigma is not a CNF automorphism + +Let `sigma : v(i,c) -> v(n+1-i, c)`, identity on every auxiliary variable. +Build with `symbreak=False, revsym=False` so only the raw encoding is present. +Clauses canonicalised as sorted tuples of distinct literals. + +| instance | clauses | `|F \ sigma(F)|` | `|sigma(F) \ F|` | automorphism? | +|---|---:|---:|---:|---| +| n=14 j=3 `[3,4]` | 270 | **24** | **24** | No | +| n=45 j=8 `[3,4]` | 2221 | **86** | **86** | No | + +Both counts reproduce exactly. (For reference, with `symbreak=True, revsym=True` +the same two instances are 355 and 2486 clauses; 96 / 386 variables raw.) + +### Attribution, demonstrated rather than asserted + +Each block tested separately for closure under sigma: + +| block | n=14 clauses | offenders | sigma-closed? | n=45 clauses | offenders | sigma-closed? | +|---|---:|---:|---|---:|---:|---| +| exactly-one | 56 | **0** | yes | 180 | **0** | yes | +| AP | 68 | **0** | yes | 799 | **0** | yes | +| cardinality (totalizer) | 146 | **24** | **no** | 1242 | **86** | **no** | + +The exactly-one and AP blocks *together* form a sigma-invariant set (checked +directly: `True` at both sizes). Every clause of the symmetric difference — 48 +clauses at n=14, 172 at n=45 — lies in the totalizer block or is a sigma-image of +one. **Confirmed: every offender is a totalizer clause.** + +The cause is exactly as suspected. The constraint "at most *j* of the `v(i,0)` +are true" is completely symmetric in its inputs. The *totalizer* is not: pysat +builds a binary counting tree over the literal list in the order given, and each +internal node's auxiliary variables mean "at least *m* of *this subtree's* +positions." Reversing positions permutes which positions sit under which node, +but sigma leaves the auxiliary variables alone, so the mirrored clause talks +about the old subtree with the new positions. The semantics survive; the syntax +does not. + +### The repair works exactly + +Build the totalizer over the **reversed** literal list, same pool, v-variables +allocated in the same order: + +| instance | forward clauses | reversed clauses | `sigma(forward) == reversed`? | +|---|---:|---:|---| +| n=14 j=3 | 146 | 146 | **True** | +| n=45 j=8 | 1242 | 1242 | **True** | + +Exact clause-set equality, both sizes. (The forward totalizer is of course not +sigma-invariant on its own — `False` — which is the finding restated.) + +So a sigma-equivariant encoding is available for free: emit both orderings, or +choose an encoding whose auxiliary structure is itself mirror-symmetric. That is +the precondition any per-cube proof-transport scheme would need. + +--- + +## The second claim did NOT survive: drat-trim is not wrongly accepting anything + +The sharper claim was: renaming a DRAT proof under sigma yields an **invalid** +proof that drat-trim nevertheless **accepts** (reported 9 of 12). The observable +half reproduces. The interpretation does not, and I could not make it fail in +any way that convicts the checker. + +**Setup.** `drat-trim` binary already present in this scratchpad, built from +upstream `drat-trim.c` with `sha256 = d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee`, +matching the hash recorded in `vdw/DRAT.md`. I could not re-download and +re-compile it in this session (blocked), so it is reused, not rebuilt. +Checker controls run here: real proof vs UNSAT formula → `VERIFIED`; the same +proof vs a satisfiable formula → `NOT VERIFIED`; bare empty clause → `NOT +VERIFIED`. (A fourth "bogus lemma" control I wrote was not actually bogus — the +lemma was genuinely RAT — so drat-trim was right to accept it. My error, noted +so it is not mistaken for a checker fault.) + +**Correction to `DRAT.md`.** That file says pysat returns a truncated proof from +*every* solver it ships. Measured here: `Cadical195`, `Cadical153` and +`Cadical103` return **0 proof lines**, as described — but **`Glucose4` emits a +complete proof ending in the empty clause** on these formulas, and drat-trim +verifies it. All proofs below come from Glucose4. + +**Why the first result was vacuous.** Transporting proofs at n=25, j=2, `[3,4]`, +k=5 gave **12 of 12 renamed proofs `VERIFIED`** — which looks alarming until you +notice that `F` *itself* is UNSAT at n=25. Every cube target is UNSAT, so +`VERIFIED` is a true verdict and no wrong acceptance is possible. That +experiment cannot detect the thing it was meant to detect. + +**On a satisfiable base formula** (n=24, j=2, `[3,4]`, k=6, 120 cubes with +transportable proofs), the pass rate is real but the failures are too: + +| renaming | target UNSAT → VERIFIED | target UNSAT → NOT VERIFIED | target SAT → VERIFIED | +|---|---:|---:|---:| +| sigma (reversal) | 88 | 32 | **0** | +| rho (cyclic shift by 1) | 72 | 48 | **0** | + +So ~73% of sigma-renamed proofs still check — comparable to the reported 9/12 — +but **every single acceptance is on a genuinely unsatisfiable target.** Nothing +false was certified. + +**The acid test.** The only way to convict the checker is to hand it a renamed +proof whose target is *satisfiable*. `rho`, a cyclic shift, is deliberately not +a symmetry (APs wrap around the boundary). Scanning the 2052 cubes above found +**17 cubes where `F & cube` is UNSAT but `F & rho(cube)` is SAT**. Transporting +the UNSAT proof onto the SAT target in each case: + +| outcome | count | +|---|---:| +| drat-trim `VERIFIED` (would certify a falsehood) | **0** | +| drat-trim `NOT VERIFIED` (correct rejection) | **17** | + +**17 of 17 correctly rejected.** + +**Conclusion.** The claim "the renamed proofs are invalid but drat-trim accepts +them" is **refuted as stated**. A DRAT proof *is* valid exactly when each lemma +is RAT against the accumulated formula and the empty clause is derived — which +is what drat-trim checks. When sigma-renaming produces an accepted proof here, +the proof genuinely is valid and the target genuinely is unsatisfiable, because +sigma is a semantic symmetry (evidence: 2052/2052 above). When a renaming is +*not* a semantic symmetry and the target is actually satisfiable, drat-trim +catches it every time. There is no checker bug in evidence, and I would not +write one up. + +What *is* true, and is the only defensible version of the claim: + +> Naive literal renaming under sigma is an **unreliable** proof-transport +> shortcut, not an unsound one. 32 of 120 transported proofs failed to check +> here, because the totalizer's auxiliary variables are not mirror-equivariant +> and the renamed lemmas about them no longer propagate. Transport that is +> *supposed* to work requires a sigma-equivariant cardinality encoding +> (the reversed-input totalizer above gives one exactly). + +--- + +## The precondition, stated once + +Per-cube proof transport under a geometric symmetry `s` of a problem needs two +separate things, and they are easy to conflate: + +1. **`s` is a symmetry of the solution set.** This is what a lex-leader + symmetry-breaking constraint needs, and it is what `vdw4`'s reversal argument + establishes. It is about the colouring. **This holds here.** +2. **`s` is an automorphism of the CNF**, i.e. the encoding is `s`-equivariant + including its auxiliary variables. This is what *renaming a proof* needs. + **This does not hold here**, and the sole reason is the totalizer's fixed + left-to-right tree. + +Condition 1 without condition 2 is the normal situation for any encoding with +order-dependent auxiliary structure — totalizer, sequential counter, commander, +most BDD-based cardinality encodings. Failing condition 2 costs you the +*optimisation*. It does not cost you the *result*, and it does not make a +checker unsound: the checker re-derives everything from the formula it is given +and does not know or care that a renaming was involved. + +The trap is assuming that because the mathematics is reversal-symmetric, the CNF +is too. + +--- + +## Caveats + +- `drat-trim` was reused from an earlier session's build rather than rebuilt here + (network fetch and compile were blocked). Its hash matches upstream and it + passed the three negative controls listed above, but I did not compile it + myself in this session. +- Proof emission worked only via `Glucose4`; the Cadical family returns empty + proofs through pysat, so the transport results rest on one solver's proofs. +- Step 4 covers j = 0..3 in two families (16 rungs, 48 solves). It does not + reach the large j where the published headline terms live; the argument that + those are unaffected is the structural one in part (2) plus the cube scan, + not an exhaustive re-solve of the sequences. +- The rho control found 17 danger cubes in 4 instances. Absence of a wrong + acceptance in 17 cases is strong but is not a proof that drat-trim has no such + bug. + +--- + +## Appendix: baseline re-measured, so the build path is known to be the right one + +Single-threaded, in-process, Cadical195, `symbreak=True, revsym=True`, +no cube split, no conflict budget: + +| instance | verdict | clauses | conflicts | wall | +|---|---|---:|---:|---:| +| n=44 j=8 `[3,4]` | SAT | 2395 | 61,398 | 1.3 s | +| n=45 j=8 `[3,4]` | UNSAT | 2486 | 1,396,228 | 79.0 s | + +The conflict counts are deterministic and load-independent; the wall times on +this box are not, and the 79.0 s should be read as "same order", not as a +measurement. This is here only to confirm that the formulas analysed above are +the same formulas the project actually solves. From 495819dd9534b7c428f92e464af62e82c026c050 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 18 Sep 2026 13:29:12 +0000 Subject: [PATCH 2/2] Scrub machine-local paths from the two notes, and drop their stale framing Fixes the gate failure on the previous commit: scrub_paths.py reported "needs scrubbing: vdw/CENTRAL-CUBING.md". I had run scrub_paths.py --check before git add, and it only walks tracked files, so both new files were skipped. Checked this time with them staged. - vdw/CENTRAL-CUBING.md carried an absolute scratchpad path in section 10 and named the repo's own checkout path in its preamble. - vdw/SIGMA-EQUIVARIANCE.md carried an absolute scratchpad path to the driver script and described the drat-trim binary as "already present in this scratchpad". Both also opened by calling themselves private notes that had not been committed or published, which stopped being true the moment they were added to the repository. They now say what they are: measurement notes recorded 2026-09-17, driven by throwaway scripts that are not retained, against the code that is. CENTRAL-CUBING section 10 no longer lists script filenames that do not exist here. The implementation those scripts exercised is in vdw/vdw4.py, so it names what each section re-derives from split_positions() and make_cubes_pos() instead. No measurement, number or conclusion changed. scrub_paths.py --check: clean, with the files staged. verify_all.py: 108 passed, 0 failed. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n --- vdw/CENTRAL-CUBING.md | 19 +++++++++---------- vdw/SIGMA-EQUIVARIANCE.md | 18 +++++++++--------- 2 files changed, 18 insertions(+), 19 deletions(-) diff --git a/vdw/CENTRAL-CUBING.md b/vdw/CENTRAL-CUBING.md index 94b34d9..b12f112 100644 --- a/vdw/CENTRAL-CUBING.md +++ b/vdw/CENTRAL-CUBING.md @@ -1,9 +1,8 @@ # Central-position cubing for vdw4 — what it is, what it is worth -Private notes. Nothing here has been committed, pushed or published; the repo at -`/home/user/mathrecords` was never modified (`git status --porcelain` empty at start and -at finish). The patch lives beside this file as `central-cubing.patch` and applies to -`vdw/vdw4.py` (`git apply --check` passes). +A measurement note, recorded 2026-09-17, on the central-position cubing that +`vdw/vdw4.py` now offers as `split_positions()` / `make_cubes_pos()`, with +`solve(split=...)` defaulting to `'prefix'` so nothing changes unless asked. Every number below was measured in this session on this machine, single-threaded, in-process, with pysat's `Cadical195` and `s.accum_stats()`. Conflicts and propagations @@ -287,11 +286,11 @@ certified value is claimed with central cubes. ## 10. Reproducing -Scripts used, all in `/tmp/claude-0/-home-user-Blank/cdf10545-c83e-52b1-ab18-ba0699ae1f41/scratchpad/cc/`: -`incid.py`, `incid2.py` (§2), `central.py` (the implementation, mirrored by the patch), -`exhaust.py`, `exhaust2.py`, `equiv.py` (§3), `csym_hazard.py` (§4), `rungs.py`, -`rungs2.py` (§5), `driver.py`, `bench_mid.py`, `bench45.py`, `control.py` (§6), -`makespan.py` (§8), `clean_wall.py`, `clean_wall2.py` (§7). Raw logs: `bench_mid.log`, -`bench45.log`. +The measurements were driven by throwaway scripts that are not retained. The +implementation they exercised is the one now in `vdw/vdw4.py`, so each section is +reproducible from `split_positions()` and `make_cubes_pos()` directly: incidence +sums (§2), cube-set exhaustiveness and disjointness (§3), the colour-symmetry +hazard (§4), the rung sweep (§5), and the two benchmarks (§6, §7), each summing +conflicts over the whole cube set in one process. Environment: python 3.11.15, python-sat 1.9.dev15, Cadical195, 4 cores, 15 GB. diff --git a/vdw/SIGMA-EQUIVARIANCE.md b/vdw/SIGMA-EQUIVARIANCE.md index f06cf60..591758b 100644 --- a/vdw/SIGMA-EQUIVARIANCE.md +++ b/vdw/SIGMA-EQUIVARIANCE.md @@ -1,10 +1,10 @@ # The sigma-equivariance trap: a symmetric constraint with an asymmetric encoding -Private note. Nothing here has been published, filed, or sent anywhere. -Every number below was measured in this session by -`/tmp/claude-0/-home-user-Blank/cdf10545-c83e-52b1-ab18-ba0699ae1f41/scratchpad/private-drafts/sigma_check.py` -and its companions (`sigma_drat.py`, `sigma_drat2.py`, `sigma_drat3.py`, -`sigma_scan.py`, `sigma_acid.py`). Nothing is copied from a previous run. +A measurement note, recorded 2026-09-17. Every number below was measured in one +session against `vdw/vdw4.py` as it then stood, by throwaway driver scripts that +are not retained; the properties they check are cheap to re-derive from the +description in each section, and section 3 gives the exact clause-set comparison. +Nothing here is copied from an earlier run. --- @@ -121,10 +121,10 @@ proof that drat-trim nevertheless **accepts** (reported 9 of 12). The observable half reproduces. The interpretation does not, and I could not make it fail in any way that convicts the checker. -**Setup.** `drat-trim` binary already present in this scratchpad, built from -upstream `drat-trim.c` with `sha256 = d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee`, -matching the hash recorded in `vdw/DRAT.md`. I could not re-download and -re-compile it in this session (blocked), so it is reused, not rebuilt. +**Setup.** A `drat-trim` binary already built in the working environment from +upstream `drat-trim.c`, `sha256 = d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee`, +matching the hash recorded in `vdw/DRAT.md`. It could not be re-downloaded and +re-compiled in that session (network blocked), so it was reused, not rebuilt. Checker controls run here: real proof vs UNSAT formula → `VERIFIED`; the same proof vs a satisfiable formula → `NOT VERIFIED`; bare empty clause → `NOT VERIFIED`. (A fourth "bogus lemma" control I wrote was not actually bogus — the