# Random SAT benchmark and transition calibration

Initial decision: **Conditional benchmark workflow**. First dossier, 9 October 2026 Australia/Brisbane. No buyer validation or profitability evidence has been established.

## Research finding

The collection states limiting random-k-SAT thresholds, hitting-time variance Θk(n), and computability of the random 3-SAT threshold. Clauses contain distinct variables, independent uniform signs and sampling with replacement. The selected formal variance is sharp for k≥4 but retains O(n log n) above a linear lower bound for k=3. Threshold computability supplies no practical runtime or finite-size convergence rate. The repository credits Gaia Carenini’s concurrent threshold-existence result with priority.

## Problem and buyer

SAT solver researchers and verification-tool teams need reproducible stress suites whose clause law, transition regime and timeout handling are explicit. A suite can otherwise confuse solver timeouts with unsatisfiability or compare runs across different random distributions.

## What the finding could enable

A benchmark service can record first-unsatisfiable prefix measurements, finite-size transition estimates, variance diagnostics and reproducible seeds. The new results sharpen theoretical expectations for this precisely defined law. A custom CI pipeline can monitor solver changes near hard regimes; it does not turn threshold computability into a faster SAT solver.

## Technical and commercial limits

Random formulas differ from structured industrial verification instances. No assertion is made about the limiting threshold itself at exact equality. Finite-size uncertainty, solver censored runs and repeated-variable clauses need explicit treatment. Computability alone does not give an economical precision calculator.

## Minimal architecture

Exact clause-law generator -> saved seed and clause stream -> incremental SAT adapter -> verified SAT/UNSAT evidence or timeout -> first-unsatisfiable prefix ledger -> replicated finite-size statistics -> regression report. Store unknown separately from false, and record solver build and per-run budgets.

## Existing alternatives and differentiation

PySAT already wraps established SAT engines and supports incremental calls; its bounded calls can return unknown when a budget is exhausted. The proposed addition is distribution and transition calibration with disciplined evidence, rather than another solver wrapper. Carenini’s primary report confirms an independent threshold-existence proof and should be credited when describing novelty. [PySAT solver API](https://pysathq.github.io/docs/html/api/solvers.html), [ECCC TR26-229](https://eccc.weizmann.ac.il/report/2026/229/).

## Monetization hypothesis

Hypothesis: AUD 3,000–10,000 for benchmark integration, then AUD 300–1,000 monthly for recurring regression analysis. At an illustrative AUD 5,000 integration fee, 25 engineering hours costed at AUD 150/hour leave AUD 1,250 before compute, support and overhead. A solver vendor may already maintain equivalent suites for less.

## Validation experiment

For several small n and fixed k, generate independent proper clauses, measure first-unsatisfiable prefixes with an existing exact solver and compare repeated variance estimates. Include a deliberately tiny solver budget and verify that censored runs remain unknown rather than becoming UNSAT. No limiting-theorem verification or universal solver ranking is inferred from this finite experiment.

## Conditions to reject or defer

Reject if random suites fail to predict regressions on the buyer’s workloads, if open tooling already satisfies the workflow, or if solver compute dominates a realistic fee. Defer threshold-digit generation until the source algorithm’s practical cost is understood.

## Next concrete action

Implement a deterministic clause-law fixture generator and a schema preserving timeout censoring, before building a paid service.

## Pinned research sources

- Family 235: [A Limiting Satisfiability Threshold for Every Fixed Clause Size](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf).
- Family 235: [selected formal scope](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/235.md); not independently checked here.