CMP.1:5.4 - Recover a witness through adaptive decision queries

The required answer is the lexicographically least satisfying assignment of a Boolean circuit C on n ordered input bits, or UNSAT. An available solver decides whether a supplied circuit has any satisfying assignment and terminates on either answer.

First query C. A negative answer gives UNSAT. After a positive answer, retain a prefix with a satisfying extension. Try its next bit as 0 and query the circuit with that prefix fixed. Keep 0 if the answer is yes; otherwise keep 1. The retained prefix still has a satisfying extension. After n bit choices it is a complete satisfying assignment; preferring 0 at each position makes it the least one.

For C(a,b,c)=(a or b) and (not a or c), the answers are:

C: yes -> prefix 0: yes -> prefix 00: no -> prefix 010: yes.

The recovered answer is 010. For circuit size N, copying each restricted circuit takes O(N) work. There are at most n+1 calls, giving total work bounded by (n+1)T_B(O(N))+O(nN+n) and sequential-call space O(N+n+S_B(O(N))).

If the solver only recognizes satisfiable inputs and may diverge otherwise, the query at prefix 00 can fail to return. This construction then lacks its required guarantee. Obtain a total decider or use finite enumeration, whose worst-case work is O(2^n N).