Withdraw two unsupported performance claims; add opt-in central-position cubing

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

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

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.

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

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.

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]