SAT search polynomial-time Turing reduces to SAT decision

Query the $SAT$ oracle on $\phi$ itself. If the answer is "no", halt and report that no satisfying assignment exists. If the answer is "yes", initialize the current residual formula to ${\psi }_0:=\phi$.

For $i=1,\dots ,n$, form the two residual formulas obtained from ${\psi }_{i-1}$ by substituting $x_i=1$ and $x_i=0$. Query the oracle on the first one. If it is satisfiable, record $x_i=1$ and set ${\psi }_i$ equal to that first residual formula. Otherwise record $x_i=0$ and set ${\psi }_i$ equal to the second residual formula. At least one branch is satisfiable, because any satisfying assignment of ${\psi }_{i-1}$ gives one of the two values to $x_i$.

By induction on $i$, the maintained residual formula ${\psi }_i$ is satisfiable and is obtained from $\phi$ by fixing the first $i$ variables to the recorded values. After the final stage, every variable has been assigned, so the recorded bits form a satisfying assignment for $\phi$. This is exactly the witness demanded in [L1].

The algorithm makes at most $n+1$ oracle calls, and each intermediate substitution and formula rewrite is polynomial in $\mathrm{\mid }\phi \mathrm{\mid }$. Since the satisfying assignment itself has length $n\le \mathrm{\mid }\phi \mathrm{\mid }$, this stays within the polynomial witness regime of [L2]. Therefore SAT search polynomial-time Turing reduces to SAT decision.