From 9eb456accbdadba9034750cdec402a3c1098658d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 18 Sep 2026 08:42:42 +0000 Subject: [PATCH] Withdraw two unsupported performance claims; add opt-in central-position cubing Measurement first. On these instances a semantically null change -- permuting the clause order handed to the solver -- moves the conflict count by a factor of 2.26 at n=45, j=8 (16 permutations, 887,582 to 2,005,413), 1.56x at n=42/j=7, 2.15x at n=37/j=11, and 36.4x on the satisfiable side at n=44/j=8. Conflict counts are deterministic, so that spread is the permutation and nothing else. vdw/BENCHMARKING.md records the method, the numbers and the protocol to use instead. Consequences: - PAPER.md 4.4 and the corresponding paragraph in paper/main.tex claimed a 1.55x speedup from the reversal lex-leader constraint. Withdrawn. It was one timed run per configuration, which cannot resolve an effect of that size here. Retested over 12 clause permutations per configuration on the monolithic path, all 24 runs UNSAT: median 1,386,901 conflicts with revsym on against 1,194,370 with it off -- ratio 0.861, the opposite direction, two-sided p = 0.347. The constraint is NOT withdrawn. The lex-leader argument is a proof of soundness, not a measurement, and it stands. Nor does this settle the cube-and-conquer path, where the original number was measured and which was not re-run. The number is withdrawn, not the constraint, and no published term is affected. - PAPER.md 4.5 and paper/main.tex claimed k=4 at 34.1 s against k=6 at 65.1 s. That is 1.91x from a single wall-clock pair, inside the floor above, on a shared machine. k=4 stays the default; that comparison does not establish it. - vdw/revsym_bench.py and vdw/engine_bakeoff.py both report one run per configuration. Docstrings now say so and point at BENCHMARKING.md. engine_bakeoff additionally does not give the engines the same clause order. Also adds opt-in central-position cubing to vdw/vdw4.py: split_positions() and make_cubes_pos(), with solve(split=...) defaulting to 'prefix' so nothing changes unless asked. Splitting on the highest-AP-incidence window instead of the first k positions measured 1.50x-3.66x fewer conflicts summed over the cube set. Verified before commit: - make_cubes_pos on positions 1..k is identical to the existing make_cubes across 4 target pairs, with colour_sym both on and off - 14/14 rungs across A217058, A217005 and A217007 come out right through central cubes, every SAT witness re-verified by check(), which reads only the colouring - porting colour_sym to a non-prefix window is unsound (it can lose a solution, e.g. [3,3] j=3 n=19), so make_cubes_pos raises rather than allowing it; confirmed it still permits colour_sym on a genuine prefix - python verify_all.py: 108 passed, 0 failed Note for the certification path: cube_certify.py and cube_exhaustive.py still assume prefix cubes. Do not claim a certified value with central cubes until that tail is re-derived. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n --- PAPER.md | 25 +++++++-- paper/main.tex | 18 +++++-- vdw/BENCHMARKING.md | 93 +++++++++++++++++++++++++++++++++ vdw/engine_bakeoff.py | 6 +++ vdw/revsym_bench.py | 10 ++++ vdw/vdw4.py | 116 ++++++++++++++++++++++++++++++++++++++++-- 6 files changed, 254 insertions(+), 14 deletions(-) create mode 100644 vdw/BENCHMARKING.md diff --git a/PAPER.md b/PAPER.md index fdea2f1..ab0af00 100644 --- a/PAPER.md +++ b/PAPER.md @@ -181,17 +181,32 @@ a sound lex-leader constraint, and it halves the search space. 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 -search ran with no symmetry breaking whatsoever. Adding reversal symmetry -measured a **1.55×** speedup on the `n=45, j=8` refutation, on the half of the -problem that consumes essentially all the time. +search ran with no symmetry breaking whatsoever. + +**A 1.55× speedup was claimed here and is withdrawn.** It came from one timed run +per configuration. Permuting the clause order of this same formula, which changes +nothing semantically, moves the conflict count across a 2.26× range (16 +permutations, 887,582 to 2,005,413), so a single pair cannot resolve an effect of +that size. Measured over 12 permutations per configuration on the monolithic +path, all 24 runs UNSAT: median 1,386,901 conflicts with reversal symmetry on +against 1,194,370 with it off — ratio 0.861, the opposite direction, two-sided +p = 0.347. Details in `vdw/BENCHMARKING.md`. + +The constraint itself is unaffected: the lex-leader argument above is a proof, not +a measurement. This also does not settle the cube-and-conquer path, where the +original number was measured; that was not re-run. What is withdrawn is the +number, not the constraint. ### 4.5 Search organisation Refutations use cube-and-conquer: branch on all class assignments to the first `k` positions, discard prefixes that already exceed the wildcard budget or already contain a monochromatic AP, and solve the residual formulas in parallel. -For `[3,4]`, `k = 4` gives 75 cubes. A measured comparison put `k = 4` at 34.1 s -against `k = 6` at 65.1 s on `n=45, j=8`, so the finer split was not used. +For `[3,4]`, `k = 4` gives 75 cubes. An earlier version reported `k = 4` at 34.1 s +against `k = 6` at 65.1 s on `n=45, j=8`. That is a 1.91× ratio from a single +wall-clock pair — inside the 2.26× clause-order range above, and wall-clock on a +shared machine besides. `k = 4` is kept as the default, but that comparison does +not establish it. **UNSAT is reported only when every cube has returned an explicit verdict.** A worker killed by the operating system raises an error rather than being counted diff --git a/paper/main.tex b/paper/main.tex index 2f453e6..a5dea11 100644 --- a/paper/main.tex +++ b/paper/main.tex @@ -259,9 +259,15 @@ \subsection{Reversal symmetry}\label{sec:revsym} only the symmetry between classes \emph{sharing} a target value. On distinct-target families such as $(3,4)$ that rule emits no clauses at all, so every search there had previously run with no symmetry breaking -whatsoever. Adding reversal symmetry measured a $1.55\times$ speedup on the -$n=45$, $j=8$ refutation, on the half of the problem that consumes -essentially all the time. The map itself is standard, and is used in +whatsoever. An earlier version of this paper reported a $1.55\times$ speedup +from adding reversal symmetry on the $n=45$, $j=8$ refutation. That figure is +withdrawn: it rested on one timed run per configuration, and permuting the +clause order of the same formula---a semantically null change---moves the +conflict count across a $2.26\times$ range, so a single pair cannot resolve an +effect of that size. Measured over $12$ clause permutations per configuration +on the monolithic path, the median ratio is $0.861$ in the opposite direction +(two-sided $p=0.347$). The lex-leader argument is a proof and is unaffected; +what is withdrawn is the timing. The map itself is standard, and is used in the same role by Kouril and Paul \cite{kourilpaul}; what is new here is only its presence on distinct-target families, where the pre-existing rule was silent. Because it is nonetheless the one component the engine adds, the @@ -277,8 +283,10 @@ \subsection{Cube-and-conquer and the completeness of the cube set}\label{sec:cub branches of one search tree, solved independently --- is what Ahmed used to settle $w(2;3,17)$ and $w(2;3,18)$ \cite{ahmed2010}. At $k=4$ the five families yield $75$ cubes for targets $(3,4)$, $36$ for $(3,3)$, $40$ for $(4,4)$, $80$ for -$(4,5)$ and $76$ for $(3,5)$. A measured comparison on $n=45$, $j=8$ put $k=4$ at $34.1$\,s -against $k=6$ at $65.1$\,s, so the finer split was not used for search. +$(4,5)$ and $76$ for $(3,5)$. An earlier version reported $k=4$ at $34.1$\,s against +$k=6$ at $65.1$\,s on $n=45$, $j=8$; that is a $1.91\times$ ratio from a single +wall-clock pair, inside the clause-order range noted above, so it does not +establish the preference. $k=4$ is retained as the default. One structural rule is worth stating because it is the difference between a theorem and a retraction: \textsc{unsat} is reported only when every cube has diff --git a/vdw/BENCHMARKING.md b/vdw/BENCHMARKING.md new file mode 100644 index 0000000..532c36e --- /dev/null +++ b/vdw/BENCHMARKING.md @@ -0,0 +1,93 @@ +# Benchmarking on this family: the clause-order noise floor + +Short version: on these instances, permuting the clause order of a formula — which +changes nothing about what the formula means — moves the conflict count by more than a +factor of two. Any speedup claim below that, measured one run per configuration, is +not evidence. + +This file exists because several performance claims in this repository were made that +way, and have been withdrawn. The mathematical results are untouched; see the end. + +## The measurement + +Take the CNF from `vdw4.build(n, j, targets, symbreak=True, revsym=True)` and shuffle +the clause list before handing it to the solver. Same clauses, same variable numbering, +same literals. Only the order changes, which changes CaDiCaL's initial variable scores, +phase saving and watch-list layout. + +`n = 45, j = 8, targets [3,4]` — the benchmark refutation. 2486 clauses, Cadical195, +single-threaded, in-process, **16 clause permutations**, all returning UNSAT: + +| | conflicts | +|---|---| +| min | 887,582 | +| median | 1,359,012 | +| max | 2,005,413 | +| **max / min** | **2.26** | + +Conflict counts are deterministic — rerunning the same `(instance, mode, seed)` +reproduces them exactly — so the spread is the permutation and nothing else. + +Other instances: 1.56× at `n=42, j=7`; 2.15× at `n=37, j=11`; 1.56× at `n=31, j=8`. +Not solver-specific: Cadical153 1.61×, Glucose4 1.40×, Minisat22 1.70×. Variable +renaming, a different null transformation, gives 1.58×–1.93×. + +**The satisfiable side is far worse.** `n = 44, j = 8`, 24 permutations: +19,766 → 719,703 conflicts, a spread of **36.4×**. + +## What it costs + +Bootstrapping from the 16 samples, two configurations that are *genuinely identical*, +each scored as a median of *k* permutations, still appear to differ by: + +| protocol | median apparent ratio | 95th percentile | +|---|---|---| +| one run each | 1.26× | **1.89×** | +| median of 3 | 1.20× | 1.59× | +| median of 5 | 1.17× | 1.50× | +| median of 9 | 1.12× | 1.41× | + +Even a median-of-9 protocol manufactures a 1.4× "speedup" from nothing one time in +twenty. Below roughly 1.4× there is no repeat count that rescues a single-instance +claim; you need many instances, or a mechanism argument. + +## The claim this retired + +`PAPER.md` §4.4 reported a 1.55× speedup from the reversal lex-leader constraint. +Measured distributionally instead — 12 clause permutations per configuration on the +monolithic path, all 24 runs UNSAT: + +| | N | min | median | max | +|---|---|---|---|---| +| `revsym=True` | 12 | 887,582 | 1,386,901 | 2,005,413 | +| `revsym=False` | 12 | 1,009,244 | 1,194,370 | 2,117,652 | + +Median ratio 0.861 — the *opposite* sign. Permutation test on the median difference, +200,000 relabelings: two-sided **p = 0.347**. The luckiest single pair in this data +would have reported 2.39×, the unluckiest 0.50×. 1.55× sits unremarkably inside that. + +Nothing went wrong in the original experiment except that its sample size was one. + +Caveat: the original 1.55× was measured through the full `solve()` path (cube-and- +conquer, process pool, wall clock). The table above is the monolithic single-solver +path scored in conflicts. So this establishes that there is no detectable effect on +the monolithic path, and that the original protocol could not have established one +either way. It does **not** establish that the constraint fails to pay in the cube +setting — that was not re-run. + +## Protocol to use instead + +Time both configurations over the *same set* of clause permutations and compare +distributions, not single runs. Report conflicts, not wall clock: conflicts are +deterministic, wall clock on a shared machine is not. State the sample size. + +`vdw/revsym_bench.py` and `vdw/engine_bakeoff.py` both predate this and both report +single runs. Treat anything they print below ~2.3× as noise. + +## What is not affected + +Every published term rests on a refutation plus an explicitly checked witness. How long +a proof took has no bearing on whether it is a proof, and the lex-leader argument in +§4.4 is a proof of soundness, not a measurement. No value in this repository, and no +OEIS term, is touched by anything on this page. What is affected is the performance +claims — and those are the ones most likely to be repeated by someone else. diff --git a/vdw/engine_bakeoff.py b/vdw/engine_bakeoff.py index 3aa674d..794d52a 100644 --- a/vdw/engine_bakeoff.py +++ b/vdw/engine_bakeoff.py @@ -10,6 +10,12 @@ enough to rank engines, small enough to finish in minutes. One core per engine, run concurrently. + +READ vdw/BENCHMARKING.md BEFORE TRUSTING THIS RANKING. One run per engine, and +the engines are not even given the same clause order. The clause-order noise +floor on n=42, j=7 is 1.56x, so the "2x engine" this docstring is built around is +right at the edge of what this experiment can resolve. Ranking engines credibly +needs the same permutation set across engines and more than one instance. """ import os import sys diff --git a/vdw/revsym_bench.py b/vdw/revsym_bench.py index f072331..97eea45 100644 --- a/vdw/revsym_bench.py +++ b/vdw/revsym_bench.py @@ -5,6 +5,16 @@ same UNSAT instances with the reversal lex constraint off and on, everything else held fixed, so the number is attributable. +READ vdw/BENCHMARKING.md BEFORE TRUSTING WHAT THIS PRINTS. It reports one timed +run per configuration, and on this family a semantically null clause-order +permutation alone moves the conflict count by a factor of 2.26. Anything this +script reports below roughly 2.3x is inside that floor and is not evidence. The +1.55x that this script produced for PAPER.md 4.4 did not survive a 12-permutation +paired retest (median ratio 0.861, the opposite sign, p = 0.347) and has been +withdrawn. To measure this properly, run both configurations over the SAME set of +clause permutations and compare distributions, scoring conflicts rather than wall +clock. + Also sweeps worker count, because the machine has 16 logical but ~8 physical cores and only ~6 GB free: 16 concurrent CaDiCaLs is what was exhausting RAM and orphaning workers. diff --git a/vdw/vdw4.py b/vdw/vdw4.py index c8de330..14c5ab4 100644 --- a/vdw/vdw4.py +++ b/vdw/vdw4.py @@ -206,6 +206,105 @@ def make_cubes(n, j, targets, k, colour_sym=True): return cubes +def ap_incidence(n, targets): + """inc[i] = how many target-length APs of [1,n] pass through position i, + summed over the targets. Positions near the centre lie on strictly more + APs than positions near either end, so fixing them constrains more clauses + per decision than fixing a prefix does.""" + inc = [0] * (n + 2) + for t in targets: + for ap in aps(n, t): + for i in ap: + inc[i] += 1 + return inc + + +def split_positions(n, k, mode='prefix', targets=None): + """The k positions to split on. 'prefix' is the historical behaviour + (positions 1..k); 'central' takes the middle window; 'incidence' takes the + k positions of highest AP incidence (needs `targets`).""" + if mode == 'prefix': + return list(range(1, k + 1)) + if mode == 'central': + lo = (n - k) // 2 + 1 + return list(range(lo, lo + k)) + if mode == 'incidence': + if targets is None: + raise ValueError("mode='incidence' needs targets") + inc = ap_incidence(n, targets) + return sorted(sorted(range(1, n + 1), key=lambda i: (-inc[i], i))[:k]) + raise ValueError(f'unknown split mode {mode!r}') + + +def _aps_within(n, targets, positions): + """(colour, AP) pairs whose every member lies in `positions`.""" + S = set(positions) + out = [] + for c, t in enumerate(targets, start=1): + for ap in aps(n, t): + if all(i in S for i in ap): + out.append((c, ap)) + return out + + +def make_cubes_pos(n, j, targets, positions, colour_sym=False): + """make_cubes generalised to an arbitrary SET of split positions. + + Returns cubes as tuples of (position, class) pairs. A cube is dropped only + when a clause already in build()'s output refutes it outright: a + monochromatic target-length AP lying wholly inside `positions` (an AP + clause), or more than j wildcards among them (the cardinality constraint). + Everything else is kept, so the cube set stays EXHAUSTIVE: for any + assignment of `positions`, it is either some cube or refuted by F alone. + + `colour_sym` is REFUSED off a prefix. The repo's colour-symmetry rule + orders the FIRST OCCURRENCE of interchangeable colours in the whole word; + read off a window it orders first occurrences *within the window*, which is + not a symmetry of F and silently deletes solutions. Measured: [3,3] j=3 + n=19 is SAT, and a central k=6 window with that rule ported naively reports + it UNSAT. That is exactly how a false new term gets published. + """ + positions = sorted(positions) + k = len(positions) + if colour_sym and positions != list(range(1, k + 1)): + raise ValueError('colour_sym is sound only on a prefix; see docstring') + r = len(targets) + idx = {p: m for m, p in enumerate(positions)} + within = [(c, [idx[i] for i in ap]) + for c, ap in _aps_within(n, targets, positions)] + groups = {} + for c, t in enumerate(targets, start=1): + groups.setdefault(t, []).append(c) + cubes = [] + for asg in itertools.product(range(r + 1), repeat=k): + if asg.count(0) > j: + continue + if colour_sym: + ok = True + for t, cols in groups.items(): + seen = [] + for x in asg: + if x in cols and x not in seen: + seen.append(x) + if seen != cols[:len(seen)]: + ok = False + break + if not ok: + continue + if any(all(asg[m] == c for m in ap) for c, ap in within): + continue + cubes.append(tuple(zip(positions, asg))) + return cubes + + +def _cube_pairs(cube): + """Accept both cube shapes: a flat tuple of classes (legacy prefix cube, + positions 1..k) or a tuple of (position, class) pairs.""" + if cube and isinstance(cube[0], tuple): + return list(cube) + return [(i + 1, c) for i, c in enumerate(cube)] + + def _decode(model, v, n, r): m = set(l for l in model if l > 0) return [next(c for c in range(r + 1) if v(i, c) in m) for i in range(1, n + 1)] @@ -215,7 +314,7 @@ def _cube_job(args): n, j, targets, cube, symbreak, revsym, engine = args cnf, pool, v = build(n, j, targets, symbreak=symbreak, revsym=revsym) r = len(targets) - units = [[v(i + 1, c)] for i, c in enumerate(cube)] + units = [[v(i, c)] for i, c in _cube_pairs(cube)] cls = _solver(engine) if engine in NON_INCREMENTAL: with cls(bootstrap_with=cnf + units) as s: @@ -245,8 +344,13 @@ def solve_direct(n, j, targets, conflicts=20_000, symbreak=True, revsym=True, def solve(n, j, targets, k=None, workers=16, symbreak=True, revsym=True, - engine=DEFAULT_ENGINE, probe=20_000): - """(sat?, colouring or None). Raises if any cube fails to report.""" + engine=DEFAULT_ENGINE, probe=20_000, split='prefix'): + """(sat?, colouring or None). Raises if any cube fails to report. + + `split` selects the cube positions: 'prefix' (default, unchanged) or + 'central'/'incidence' (see split_positions). The non-prefix modes run with + the colour-symmetry cube rule OFF, which is what a certification run needs + anyway (cube_exhaustive.py).""" if probe: r, col = solve_direct(n, j, targets, conflicts=probe, symbreak=symbreak, revsym=revsym, engine=engine) @@ -256,7 +360,11 @@ def solve(n, j, targets, k=None, workers=16, symbreak=True, revsym=True, return False, None if k is None: k = 4 if len(targets) == 2 else 3 - cubes = make_cubes(n, j, targets, k) + if split == 'prefix': + cubes = make_cubes(n, j, targets, k) + else: + cubes = make_cubes_pos(n, j, targets, + split_positions(n, k, split, targets)) if not cubes: return False, None tasks = [(n, j, targets, c, symbreak, revsym, engine) for c in cubes]