Converting Boolean circuit to Boolean formula in parallel Let t be a fixed constant. I would like to convert a Boolean circuit C of depth t on n inputs over AND, OR and NOT gates (of fan-in 2, say) to an equivalent Boolean formula F on the same n inputs, in the sense that for each input vector x of length n, we have C(x) = 1 if and only if F(x) = 1. Some restrictions on the problem: the circuit has size m and depth t, and I would like the function mapping C to F to be computable by a PRAM (say) using a number of processors polynomial in m and time polylogarithmic in m. I don't mind that the size of the resulting formula is O(mt), I consider t to be a constant.

The approach I envision is to enumerate each path of length t from the output gate to each input gate and transform that set of paths into a trie. This trie will then be a tree of branching factor m and depth t representing a Boolean formula of size O(mt), observing that this is a polynomial in m if I consider t to be a fixed constant. My problem then reduces to the problem of constructing a trie from a set of at most mt strings, each one a string of length at most t over an alphabet of cardinality m.

Can I construct a trie of strings of length t over an alphabet of size m in parallel time polylogarithmic in m? More generally, can I convert a Boolean circuit of size m and depth t to a Boolean formula in parallel time polylogarithmic in m?
Take a look at the Tseitin transform.  The Tseitin transform can be applied in parallel, working separately on each gate.  Consequently, this can be implemented using one processor per gate, $O(1)$ time per gate, and the resulting formula has size $O(m)$.  Here I'm not counting the time to build the final formula; the final formula is a conjunction of the clauses produced by the processors, with each processor adding $O(1)$ clauses to the final conjunction.