Given a boolean circuit $C$ on $n$ variables (which uses just NOT,AND and OR gates), what is the most efficient way to extract the boolean formula represented by the circuit? Is there a polytime algorithm for this problem?
If I understand your question correctly, I'd say you could use the standard reduction from CIRCUIT-SAT to SAT: Represent each gate as a new variable, and then represent the entire circuit in CNF form, with each clause having the form $(v\leftrightarrow\phi)$, where $v$ is the new variable, and the formula for the gate is given by $\phi$, using the variables for other gates to represent the inputs. This can be done by a simple traversal (in linear time, which is clearly optimal).
For example, if you hade three inputs, $x_1$, $x_2$, and $x_3$, with AND gates linking $x_1$ and $x_2$ as well as $x_2$ and $x_3$, and an OR gate linking their outputs, you could introduce three variables to represent the gates—$v_1$, $v_2$, and $v_3$, respectively—and rewrite the formula to $$(v_1\leftrightarrow(x_1\land x_2))\land (v_2\leftrightarrow(x_2\land x_3))\land (v_3\leftrightarrow(v_1\lor v_2))\land v_3\,.$$ Note that the output variable is included explicitly.
Introduction to Algorithms by Cormen et al. explains this in detail, in the chapter on NP-Completeness.