[proofplan] We first ask the decision oracle whether the input formula is satisfiable at all. If it is not, the search problem is solved by reporting failure. If it is satisfiable, we reveal a satisfying assignment one variable at a time by testing whether satisfiability survives after fixing the next variable to $0$; if not, fixing it to $1$ must preserve satisfiability. The maintained invariant is that after each choice the restricted formula remains satisfiable, so after all variables are fixed the resulting assignment satisfies the original formula. [/proofplan]

[step:Query the decision oracle to handle the unsatisfiable case] Let $\varphi$ be a Boolean formula, and let $V(\varphi)=\{x_1,\dots,x_n\}$ be the set of variables appearing in $\varphi$, listed in any fixed order. Define an oracle algorithm $A^{\operatorname{SAT}}$ as follows. First query the $\operatorname{SAT}$ oracle on $\varphi$. If the oracle returns no, then $A^{\operatorname{SAT}}$ outputs that no satisfying assignment exists. This output is correct because the oracle answer no means, by the definition of the decision problem $\operatorname{SAT}$, that there is no map $a:V(\varphi)\to\{0,1\}$ such that $\varphi(a)=1$. [/step]

[step:Maintain a satisfiable restricted formula while assigning variables]Assume now that the first oracle query returns yes. Define $\varphi_0:=\varphi$, and define a partial assignment after stage $i$ to be a map $a_i:\{x_1,\dots,x_i\}\to\{0,1\}$. For $0\leq i\leq n$, let $\varphi_i$ denote the formula obtained from $\varphi$ by substituting $x_j=a_i(x_j)$ for each $1\leq j\leq i$; for $i=0$, this means no substitution has been made. We construct $a_i$ and $\varphi_i$ inductively so that $\varphi_i$ is satisfiable as a formula in the remaining variables $x_{i+1},\dots,x_n$. The base case holds because $\varphi_0=\varphi$ and the first oracle query returned yes. Suppose $0\leq i<n$ and $\varphi_i$ is satisfiable. Let $\psi_{i,0}$ be the formula obtained from $\varphi_i$ by substituting $x_{i+1}=0$. Query the $\operatorname{SAT}$ oracle on $\psi_{i,0}$. If the oracle returns yes, define $a_{i+1}(x_{i+1})=0$ and set $\varphi_{i+1}:=\psi_{i,0}$. If the oracle returns no, define $\psi_{i,1}$ to be the formula obtained from $\varphi_i$ by substituting $x_{i+1}=1$, define $a_{i+1}(x_{i+1})=1$, and set $\varphi_{i+1}:=\psi_{i,1}$. In the first case, $\varphi_{i+1}$ is satisfiable by the oracle answer. In the second case, $\varphi_i$ is satisfiable by the inductive hypothesis, so some satisfying assignment of $\varphi_i$ gives either value $0$ or value $1$ to $x_{i+1}$. Since the oracle has certified that no satisfying extension exists with $x_{i+1}=0$, at least one satisfying extension must have $x_{i+1}=1$. Hence $\psi_{i,1}=\varphi_{i+1}$ is satisfiable. The invariant is preserved.[/step]

[guided]The purpose of this step is to turn a yes-or-no satisfiability test into actual bits of a satisfying assignment. After the first oracle query, we are in the case where $\varphi$ is satisfiable, so there exists at least one map $a:V(\varphi)\to\{0,1\}$ with $\varphi(a)=1$. We do not know this map, but we can discover it one coordinate at a time. Define $\varphi_0:=\varphi$. For each integer $i$ with $0\leq i\leq n$, define a partial assignment $a_i:\{x_1,\dots,x_i\}\to\{0,1\}$, and let $\varphi_i$ be the formula obtained from $\varphi$ after substituting the chosen values for $x_1,\dots,x_i$. The invariant we maintain is: \begin{align*} \varphi_i \text{ is satisfiable as a formula in the unassigned variables } x_{i+1},\dots,x_n. \end{align*} For $i=0$, this is exactly the first oracle answer yes, because $\varphi_0=\varphi$. Now assume $0\leq i<n$ and the invariant holds for $\varphi_i$. We test whether we can safely set the next variable to $0$. Let $\psi_{i,0}$ denote the formula obtained from $\varphi_i$ by substituting $x_{i+1}=0$, and query the $\operatorname{SAT}$ oracle on $\psi_{i,0}$. If the oracle returns yes, then $\psi_{i,0}$ is satisfiable, so we set $a_{i+1}(x_{i+1})=0$ and define $\varphi_{i+1}:=\psi_{i,0}$. The invariant remains true. If the oracle returns no, then no satisfying assignment of $\varphi_i$ can have $x_{i+1}=0$. But the inductive hypothesis says that $\varphi_i$ is satisfiable. Therefore some satisfying assignment of $\varphi_i$ exists, and since every Boolean assignment gives $x_{i+1}$ either value $0$ or value $1$, such an assignment must give $x_{i+1}=1$. Let $\psi_{i,1}$ denote the formula obtained from $\varphi_i$ by substituting $x_{i+1}=1$. The preceding sentence proves that $\psi_{i,1}$ is satisfiable. Thus we set $a_{i+1}(x_{i+1})=1$ and define $\varphi_{i+1}:=\psi_{i,1}$. In both cases, after assigning $x_{i+1}$, the new restricted formula remains satisfiable. This proves the invariant by induction for all $i=0,\dots,n$.[/guided]

[step:Read off a satisfying assignment after all variables are fixed] After $n$ stages, the partial assignment is a total assignment $a_n:V(\varphi)\to\{0,1\}$. The invariant says that $\varphi_n$ is satisfiable as a formula in no remaining variables. A Boolean formula with no remaining variables is satisfiable exactly when its truth value is $1$. Since $\varphi_n$ is obtained from $\varphi$ by substituting $a_n(x_j)$ for every variable $x_j$, this means $\varphi(a_n)=1$. Therefore $a_n$ is a satisfying assignment for $\varphi$, and the algorithm correctly solves $\operatorname{SearchSAT}$. [/step]

[step:Bound the number of oracle calls and the running time] The algorithm makes one initial oracle call on $\varphi$ and then at most one oracle call for each variable $x_i$. Hence the number of oracle calls is at most $n+1$. At each stage, forming the restricted formula by substituting a Boolean value for one variable and simplifying, or simply recording the substitution without simplification, can be done in time polynomial in the length of the original input formula. Each oracle query has size polynomial in the length of $\varphi$ under any standard encoding of Boolean formulas. Therefore $A^{\operatorname{SAT}}$ is a polynomial-time oracle algorithm for $\operatorname{SearchSAT}$. If $\operatorname{SAT}$ is decidable by a deterministic polynomial-time algorithm, replace each oracle query by that algorithm. Since there are at most $n+1$ queries and each query has polynomial size, the total running time remains polynomial in the input length. Thus $\operatorname{SearchSAT}$ is solvable in polynomial time whenever $\operatorname{SAT}$ is solvable in polynomial time. [/step]