Whether a solution exists and whether an algorithm can find it are distinct questions governed by different mechanisms. In random 3-SAT, the first moment method gives P (SAT) ≈ Nₑff · e^ (−δ), where δ = αn|ln (7/8) | is a reparameterization of the clause density (the exponent in the first moment method). This characterizes existence but says nothing about discovery. We introduce the computational budget μ (solver operations) and ask: can the conditional success probability P (found|SAT) be multiplicatively decomposed as a function of μ/μc (δ)? Experiments on three solver families (CDCL, WalkSAT, Random search) across n = 100–300 variables, α = 3. 0–4. 0, yield three findings. (1) Median runtime scales as μc ∝ e^ (cδ), where the sensitivity exponent c is solver-dependent: c ≈ 0. 24 (CDCL), c ≈ 0. 21 (WalkSAT), c = 1. 0 (Random, exact) in the floor-free regime α ≥ 3. 5. (2) The ratio μ/μc is a valid normalizing variable: both solvers transition monotonically near μ/μc = 1, but transition shapes differ by 14–15%. (3) The ordering cCDCL > cWalkSAT is robust across problem sizes, though both estimates show moderate n-dependence. The parameter δ governs both existence (c = 1, mathematical identity) and discovery (c < 1, algorithm-dependent), but with qualitatively different sensitivities. Notably, c measures sensitivity to δ, not efficiency: WalkSAT has the smallest c but the largest absolute cost, meaning low sensitivity can arise from ignoring structure rather than exploiting it.
Akihito Sunagawa (Wed,) studied this question.