Random SAT: preserve the sampling law and incomplete evidence

9 October 2026. Opportunity 033 remains a low-confidence benchmark integration for SAT/verification teams. The source collection sharpens a precise asymptotic model; it does not establish a faster solver, an economical threshold-digit service or a buyer. The Facility Plan Auditor remains the first commercial experiment.

What the four manuscripts claim

For each fixed k>=3 and n>=k, a proper clause uses k distinct variables chosen uniformly and independent fair signs. Whole clauses are sampled independently with replacement. H is the first unsatisfiable prefix index; the empty prefix is SAT, and P(H>m) is the probability that the first m clauses remain SAT. Repeated whole clauses must not be silently removed. These results do not cover arbitrary industrial formulas or planted/biased/no-replacement generators.

The limiting-threshold paper asserts a positive finite alpha_k, with satisfiability tending to one at every fixed density below it and zero above it. It makes no equality claim and does not supply its numerical value. The collection explicitly credits Gaia Carenini with priority for resolving threshold existence; her primary ECCC report TR26-229 is dated 5 October 2026. This collection presents an alternative proof and companion results, not sole priority for threshold existence.

The older variance manuscript gives Theta_k(n) for k>=4, with a linear lower bound and O(n log n) upper bound for k=3. Its upper bounds also apply to min(H,floor(Bn)) for every fixed B>0; the linear lower bound requires a sufficiently late cap, with B>U_k=log(2)/[-log(1-2^-k)] sufficient. Equality at U_k is not the stated condition. A separate 5 October companion claims Var(H)=Theta(n) for proper 3-SAT, removing the logarithmic upper loss. It uses a bounded cumulative two-clause killing potential and a drift argument. The selected formal scope still describes the older k=3 O(n log n) result. Reading the new paper does not extend that formal badge.

Finite concentration is around E[H], not automatically alpha_k*n at the same scale. The reviewed results supply neither a practical finite-size bias bound nor constants for turning these tiny experiments into certified limiting digits. Low sample variance after clipping is not evidence of a narrow uncapped transition.

Computability is not a practical precision service

The threshold-computation paper claims one finite Turing machine returning a rational within 2^-r on unary precision input. It dovetails lower certificates and rational upper trials whose interval evaluation certifies a strictly negative value. It never needs to decide equality of arbitrary computable reals. Completeness ensures eventual finite witnesses, without a useful bound on witness size or running time. The paper explicitly gives no efficiency estimate. It computes a limiting density rather than solving a supplied SAT instance.

Its lower construction uses f_n/n - 2^67*n^(-1/6), where f_n is a capped hitting-time expectation in a relaxed Poisson clause process. In that auxiliary model, three variable indices are independently drawn and may repeat within a clause; arrivals form a rate-one Poisson process, and the time cap is 20n. It is not the mean of the proper, deterministic-clause-count samples in this prototype. The finite integration proof enumerates (8n^3)^m ordered signed lists and all 2^n assignments, with explicit Poisson-tail and exponential-series interval bounds.

Making this additive penalty alone at most one requires n>=2^402; making it at most 2^-r requires n>=2^(402+6r). These are exact algebraic conditions on that particular error term, not a lower bound on every possible threshold algorithm, not a sufficient total-accuracy guarantee, and not a measured runtime. The companion upper search could admit smaller witnesses; no practical witness search was implemented. Direct threshold-digit commercialization is deferred.

Runnable evidence workflow

random_sat_stream_audit.py accepts a strict JSON schema naming the law, variable count, clause size and ordered clauses. It enforces proper distinct variables with canonical literal order, while preserving duplicate whole clauses. The generator maps a uniformly selected rank bijectively to a variable subset and sign pattern. Python's seeded pseudorandom generator provides replayable fixtures, not a proof of independent fair randomness. Supplied law declarations cannot authenticate how an observed stream was generated.

Exact mode represents all assignments as a bitset, applies each original clause and retains a satisfying assignment until the first empty set. It caps n at 16 and charges bounded word/literal work. The general input caps are one MiB, 128 variables, k<=8 and 2,048 clauses; exhaustion leaves an unknown result and the last independently supported lower bound. Work charges are a resource policy, not an exact wall-clock model. Unsupported schemas/laws, duplicate JSON keys, nonfinite values, booleans in numeric fields, repeated variables within clauses and extra fields are refused.

The optional adapter uses existing OR-Tools CP-SAT 9.15.6755. It retains the growing model and reuses a still-valid SAT assignment; each needed solve is a fresh CP-SAT call, without preserved learned solver state. Every returned SAT assignment is checked directly against the complete prefix. An INFEASIBLE status becomes a solver-claimed upper bound only. It is not an independently checked UNSAT certificate. UNKNOWN and MODEL_INVALID do not become UNSAT. Per-call and between-call time budgets are recorded; these are not a hard process watchdog. Official CP-SAT statuses.

The report keeps independently supported bounds and solver claims separate. SAT at L proves H>L. Exact exhaustive UNSAT at U proves H<=U. H is independently determined only when these meet at adjacent prefix lengths. Surviving an entire M-clause stream proves H>M, not H=M, although min(H,M)=M is then known. Even SAT only through M-1 already determines that clipped value, without proving survival through M. Empty-stream and first-failure/last-SAT endpoints have explicit controls. A first-moment bound min(1,2^n*(1-2^-k)^M) is reported conditional on the declared ideal law; it does not validate the law.

The CLI refuses existing output directories, archives exact input bytes and writes a JSON report with input/checker hashes. Hashes bind bytes, not provenance or correctness. Source-derived theorem algorithms are not executed. The exact solver, rank mapping, coupon calculation and CP-SAT adapter are conventional finite controls.

Exact control: three variables expose two easy mistakes

When n=k=3, there are eight clauses and each rules out exactly one of the eight assignments. H is therefore the coupon-collector time to observe all eight clause types. Its exact mean is 761/35, approximately 21.742857, and variance is 838034/11025, approximately 76.012154. Sampling without replacement instead forces H=8 and variance zero. Deduplicating a saved stream destroys its hitting-time meaning.

Independently of that wrong-law example, clipping the correct stream at eight also gives min(H,8)=8 with variance zero, because fewer than eight proper clauses cannot eliminate every assignment. Thus the same reported number can arise from different errors or different valid questions. A saved fixture with ten initial copies of one clause followed by all eight types has H=18, not eight, with ten duplicate clauses preserved.

The exact occupancy recursion was cross-checked against inclusion-exclusion at every m from zero through 100. The figure is a finite exact law, with no sampling noise and no limiting-density estimate. Its moment curves refer to the clipped variable; dropping unresolved runs and averaging only completed H values would introduce a different selection bias.

Rational coupon probabilities and moments, duplicate fixture, exact duplicate report, genuine tiny-budget UNKNOWN, work-limit report.

Preserved finite experiments

Sixty generated proper 3-SAT streams use twenty saved seeds at n=6,10,16, with cap 10n. All reached an exactly checked first failure before the cap. The following sample moments therefore coincide with the observed uncapped H values on this batch; they do not certify an uncensored population estimate or asymptotic scaling. Reusing the same seed numbers across sizes is not a claim of mathematically independent cross-size samples.

Nine of those inputs were also evaluated with the conventional CP-SAT adapter. All nine solver-claimed first failures agreed with the exact oracle. Six additional inputs at n=40 and 80 reached solver-reported UNSAT, but their independent upper bound remains unknown because exhaustive verification is outside the declared limit. An actual 1e-9-second solver budget produced UNKNOWN, retained as such. These are functionality/evidence comparisons, not a fair solver speed benchmark, an industrial workload study or a universal solver ranking.

All sixty exact input streams and observations, fifteen CP-SAT input streams and observations, summary with budgets/versions, rank bijections. Each full stream is retained even when solving stops at its first failure.

679 passing controls include all 256 subsets of the eight three-variable clauses, 200 generated cases checked against independent direct assignment enumeration, complete rank bijections for twelve small n/k pairs, 101 inclusion-exclusion probabilities, invalid inputs, caps, duplicates, resource limits, solver evidence and preservation of an existing CLI output. These controls do not accept the source proofs. Four PDF first pages were visually inspected; the reading ledger gives exact selected TeX/interface extents. No source-native theorem program or Lean/kernel run occurred.

Product decision

Potential integration: a verification team's regression pipeline archives a declared generator, input streams, solver version/budgets, independently checked SAT witnesses, checked or unverified UNSAT evidence, and censored first-failure intervals. A buyer might pay if this prevents consequential benchmark errors that current practice misses. PySAT already provides established solver wrappers and incremental interfaces; support is engine-specific, and its documented Kissat404 interface is nonincremental. CP-SAT already handles the preserved examples. A wrapper alone has weak differentiation.

Keep the earlier AUD 3,000-10,000 integration and AUD 300-1,000 monthly figures as untested hypotheses. The earlier AUD 5,000 fee minus 25 assumed hours at AUD 150 leaves only AUD 1,250 before compute/support/overhead. No customer has validated that workflow or price. Random-suite results may fail to predict regressions on structured customer inputs. Require a permissioned regression corpus, an accepted independent UNSAT-proof path and a recurring costly failure before a standalone product. The module belongs below facility-planning assurance in the build queue.