Fórmula booleana equilibrada en

Estoy buscando referencias sobre la complejidad del problema de equilibrio de la fórmula booleana . En particular,

1. ¿Se sabía que las fórmulas booleanas se pueden equilibrar en ?$\mathsf{AC^0}$
2. ¿Hay alguna prueba simple de que el equilibrio de la fórmula booleana esté en ?$\mathsf{AC^0}$

Por "simple" me refiero a una prueba más simple que la que menciono a continuación, en particular, estoy buscando una prueba que no dependa de que la evaluación de la fórmula booleana esté en .$\mathsf{NC^1}$

Antecedentes

Aquí todas las clases de complejidad mencionadas son las uniformes.

BFB (equilibrio de la fórmula booleana):
dada una fórmula booleana , encuentre una fórmula booleana equilibrada equivalente.$\varphi$

Estoy interesado en la complejidad de este problema, en particular las pruebas simples que muestran que el problema está en (o incluso T C 0 o N C 1 ). Los argumentos de equilibrio comunes como los basados ​​en el lema de Spira aplican modificaciones estructurales repetidas al árbol de fórmulas que parecen dar solo B F B ∈ N C 2 .$\mathsf{AC^0}$$\mathsf{TC^0}$$\mathsf{NC^1}$$BFB \in \mathsf{NC^2}$

Tengo una prueba para , sin embargo, la prueba no es simple y depende de la prueba de B F E ∈ N C 1 .$BFB \in \mathsf{AC^0}$$BFE \in \mathsf{NC^1}$

$\varphi$$\tau$$\varphi$
$\tau$$\varphi$$\tau \vDash \varphi$

$BFE$$\mathsf{NC^1} = \mathsf{ALogTime}$

$BFB$$\mathsf{NC^1}$

$\varphi$$BFE$$\varphi$$\mathsf{AC^0}$$BFE$$\varphi$

Motivación

Un argumento más simple para que esté en (o o incluso ) daría una nueva prueba más simple de ya que es fácil ver que la versión balanceada de BFE se puede resolver en y podemos componerla con y el resultado estará en .$BFB$$\mathsf{AC^0}$$\mathsf{TC^0}$$\mathsf{NC^1}$$BFE \in \mathsf{NC^1}$$\mathsf{NC^1}$$BFB$$\mathsf{NC^1}$

Preguntas

1. ¿Se sabía que las fórmulas booleanas se pueden equilibrar en ( )?$\mathsf{AC^0}$$BFB\in \mathsf{AC^1}$
2. ¿Existe un argumento más simple (por ejemplo, no confiar en ) para ?$BFE\in \mathsf{NC^1}$$BFB\in\mathsf{AC^0}$

No estoy seguro de si esto es muy relevante, pero en Algoritmos de espacio de registro para rutas y coincidencias en k-Trees (basándose en una larga historia de trabajo pasado y específicamente en clases de Aritmetización alrededor de NC1 y L por Limaye-Mahajan-Rao) mostramos cómo encontrar separadores balanceados recursivos para un árbol en Logspace. Este límite puede muy bien mejorarse a si el árbol de entrada se da directamente en la representación de cadena.$\mathsf{NC}^1$

La idea básica es representar el árbol como una expresión de paréntesis y encontrar separadores equilibrados para estos. Observe que encontramos separadores de hojas, es decir, subárboles que están equilibrados con el número de hojas.