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, ECCC TR26-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.
• Family 235: selected formal scope; not independently checked here.