Search-to-decision reduction

A search-to-decision reduction reconstructs a valid witness by querying a procedure that answers only whether an appropriate witness exists. The reduction must specify how it restricts the original task after each answer and how many queries it uses.

For Boolean satisfiability, first ask whether the propositional formula is satisfiable. If it is, consider its Boolean variables in order. Tentatively fix the next variable to zero and ask whether a satisfying extension remains. Keep zero after a positive answer; after a negative answer, fix it to one. The previously satisfiable partial assignment must have an extension using one of those values, so this step preserves existence of an extension.

After all $n$ variables are fixed, the resulting assignment is a witness. There are at most $n+1$ decision queries, and each restricted propositional formula has size bounded by the original size. Thus a polynomial-time algorithm for deciding Boolean satisfiability would also give a polynomial-time algorithm for finding a satisfying assignment. The procedure proves this relation for the specified task rather than assuming arbitrary search specifications have the same reduction.