Is the Balanced Boolean Formula problem solvable in sublogarithmic space if the input has a tree structure? Suppose that instead of the usual linear work tape the input is given in a binary tree structure with n leaves and log n depth, the initial position being the root. At every node, we can step to its parent, left child or right child.

I am interested in what "tree-languages" can be accepted by what machines. More specifically, take the language where in every non-leaf we have the gate of a boolean circuit (ie. and or not), in the leaves either a constant or a variable (different for each leaf) and such a "tree-word" is in the language if and only if it has a satisfying assignment. Can this language be decided by a turing machine that has an o(log n) space worktape?

Note that it is accepted by a non-deterministic finite state machine and also by a deterministic turing machine with O(log n) space. Similarly, if all the variables are constant, then it can be decided by a deterministic finite state machine. (If there are no constants, then every formula is satisfiable.)
It seems to me that the problem can be solved in constant space.

We perform a recursive procedure, and store only the parity of the number of negation gates seen on the path from the root to the current node.

At a leaf, if we have a variable and have seen an even number of negation gates, we set the variable to be true. Otherwise, if we have seen an odd number of negation gates, we set the variable to be false.

As before, at an AND or OR gate we first call recusively to the left, and then to the right if the value has not been determined.

Now if there exists a satisfying assignment, then the assignment defined above will satisfy the formula.