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]