# Boolean formula balancing in $\mathsf{AC^0}$

I am looking for references about the complexity of Boolean formula balancing problem. In particular,

1. Was it known that Boolean formulas can be balanced in $$\mathsf{AC^0}$$?
2. Is there a simple proof of Boolean formula balancing being in $$\mathsf{AC^0}$$?

By "simple" I mean a proof simpler than the one I mention below, in particular I am looking for a proof which doesn't depend on Boolean formula evaluation being in $$\mathsf{NC^1}$$.

### Background

Here all mentioned complexity classes are the uniform ones.

BFB (Boolean formula balancing):
Given a Boolean formula $$\varphi$$,
Find an equivalent balanced Boolean formula.

I am interested in the complexity of this problem, in particular simple proofs showing the problem is in $$\mathsf{AC^0}$$ (or even $$\mathsf{TC^0}$$ or $$\mathsf{NC^1}$$). The common balancing arguments like those based on Spira's lemma apply repeated structural modifications to the formula tree which seem to only give $$BFB \in \mathsf{NC^2}$$.

I have a proof for $$BFB \in \mathsf{AC^0}$$, however the proof is not simple and depends on the proof of $$BFE \in \mathsf{NC^1}$$.

BFE (Boolean formula evaluation)
Given a Boolean formula $$\varphi$$ and a truth assignment $$\tau$$ for variables in $$\varphi$$,
Does $$\tau$$ satisfy $$\varphi$$ ($$\tau \vDash \varphi$$)?

It is known from Sam Buss's celebrated result that Boolean formula evaluation ($$BFE$$) can be computed in $$\mathsf{NC^1} = \mathsf{ALogTime}$$ (see [Buss87] and [BCGR92]).

It follows (quite surprisingly, at least to me) that Boolean formulas balancing ($$BFB$$) is also in $$\mathsf{NC^1}$$:

The idea is that we can hardcode $$\varphi$$ in the input gates of $$BFE$$ to obtain a formula equivalent to $$\varphi$$ and this is a completely syntactic operation computable in $$\mathsf{AC^0}$$. Since $$BFE$$ has balanced formulas we obtain a equivalent balanced formula for $$\varphi$$. In other words, the algorithm is:

$$\ulcorner \varphi \urcorner \mapsto \ulcorner \lambda \vec{p}. Eval(\ulcorner \varphi \urcorner, \vec{p} )\urcorner$$

### Motivation

A simpler argument for $$BFB$$ being in $$\mathsf{AC^0}$$ (or $$\mathsf{TC^0}$$ or even $$\mathsf{NC^1}$$) would give a new simpler proof of $$BFE \in \mathsf{NC^1}$$ since it is easy to see that the balanced version of BFE can be solved in $$\mathsf{NC^1}$$ and we can compose it with $$BFB$$ and the result will be in $$\mathsf{NC^1}$$.

### Questions

1. Was it known that Boolean formulas can be balanced in $$\mathsf{AC^0}$$ ($$BFB\in \mathsf{AC^1}$$)?
2. Is there a simpler argument (e.g. not relying on $$BFE\in \mathsf{NC^1}$$) for $$BFB\in\mathsf{AC^0}$$?
• What definition of "balance" do you use? – Dana Moshkovitz Dec 31 '12 at 17:24
• @Dana, we can use something like $Depth < 10\lg Size + 100$ (i.e. $Depth = O(\lg Size)$ with specific constants). See also Bonnet and Buss's paper "Size-Depth Tradeoff for Boolean Formulae", 2002. – Kaveh Jan 3 '13 at 8:09
• agreed the defn of "balancing" should be made clear. is this similar to the concept of balancing in binary trees? eg "self balanced trees" – vzn Oct 23 '13 at 20:57

I am not sure if this is very relevant but in Log-Space Algorithms for Paths and Matchings in k-Trees (building on a long history of past work and specifically on Arithmetizing classes around NC1 and L by Limaye-Mahajan-Rao) we show how to find recursive balanced separators for a tree in Logspace. This bound may very well be improvable to $\mathsf{NC}^1$ if the input tree is directly given in the string representation.