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}$?

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}$?

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 only shows $BFB \in \mathsf{NC^2}$.

I have 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 (uniform) $\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{NC^1}$)?
2. Is there a simpler argument (e.g. not relying on $BFE\in \mathsf{NC^1}$) for $BFB\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}$?

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 the complexity classes are all 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 only shows $BFB \in \mathsf{NC^2}$.

I have 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 (uniform) $\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{NC^1}$)?
2. Is there a simpler argument (e.g. not relying on $BFE\in \mathsf{NC^1}$) for $BFB\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 only shows $BFB \in \mathsf{NC^2}$.

I have 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 (uniform) $\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{NC^1}$)?
2. Is there a simpler argument (e.g. not relying on $BFE\in \mathsf{NC^1}$) for $BFB\in\mathsf{AC^0}$?