Search-to-decision reduction (source code)

= Search-to-decision reduction
{wiki}

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.