Constructing solution to 3SAT formulas using oracle queries I'm interested in 3SAT and querying an oracle. Suppose we had an oracle that can decide, on an input boolean formula $\phi$, whether there exists any assignment to the variables that makes the formula true. Note: this does not say what the assignment to the variables is, just that there exists one.

My main question is: can we get the actual solution of the formula in polynomial time, using the oracle?

My first thought was that no, it is impossible because the oracle cannot help you with an assignment (i.e., if I gave an assignment to the variables, the oracle's answer does not change). However, just because this technique does not work does not mean that no techniques will.

I then thought to give an assignment to the first variable $x_1$, and then use that to work on the next variables; however, I don't know how to progress from there without trying all possible combinations (i.e., running in time $O(2^n)$).
You have the right idea. Suppose you have a SAT oracle and an instance $I$ of 3SAT (or whatever SAT-ish class you like) containing $n$ variables, $x_1, x_2, \dotsc x_n$. You could then do this:

send I to the oracle
if the oracle answers "not satisfiable"
   quit
else
   j = 1
   I_0 = I
   repeat
      transform I_{j-1} to I_j by substituting x_j = 1
      send I_j to the oracle
      if the answer is "satisfiable"
         save x_j = 1
      else 
         save x_j = 0
         transform I_{j-1} to I_j by substituting x_j = 0
      j = j + 1
  until j = n


When the algorithm terminates, you'll have saved a satisfying collection of values for all the variables. This will be linear in $n$ (times the steps necessary to do the substitutions, which will be polynomial in the length of $I$).