The satisfiability problem asks whether a given Boolean formula in conjunctive normal form has an assignment that makes the formula "true." Cook (1971) showed that the problem is NP-complete.
Carenini (2026) announced existence of a limiting satisfiability threshold for every fixed clause size 
. In the model of independent uniformly signed clauses
on 
distinct variables, sampled with replacement, there
is a finite positive 
such that the probability
of satisfiability with 
clauses tends to 1 for 
and to 0 for 
as the number 
of variables tends to infinity.
Here 
is the floor function.
For random k-SAT with 
, Vorobyev (2026) reported that a formula with 
variables and 
clauses is unsatisfiable
with probability tending to 1 as 
. This is an upper bound
rather than an exact threshold. Vorobyev (2026) states that language models developed
the mathematical argument, numerical code, and Lean formalization under the author's
direction.
-SAT
and a Proof of the Satisfiability Conjecture." Electronic Colloquium on Computational
Complexity, Report TR26-229, 2026.