Балансировка булевой формулы в

Я ищу ссылки на сложность проблемы балансировки булевых формул . В частности,

1. Было ли известно, что булевы формулы могут быть сбалансированы в ?$\mathsf{AC^0}$
2. Есть ли простое доказательство балансировки булевой формулы в ?$\mathsf{AC^0}$

Под «простым» я подразумеваю доказательство, более простое, чем упомянутое ниже, в частности, я ищу доказательство, которое не зависит от оценки булевой формулы в .$\mathsf{NC^1}$

Фон

Здесь все упомянутые классы сложности являются единообразными.

BFB (Логическая формула балансировка):
Учитывая булеву формулу , Найти эквивалентную сбалансированную булеву формулу.$\varphi$

Меня интересует сложность этой проблемы, в частности, простые доказательства, показывающие, что проблема находится в (или даже или ). Обычные аргументы балансировки, подобные тем, которые основаны на лемме Спиры, применяют повторяющиеся структурные модификации дерева формул, которые, похоже, дают только .$\mathsf{AC^0}$$\mathsf{TC^0}$$\mathsf{NC^1}$$BFB \in \mathsf{NC^2}$

У меня есть доказательство для , однако доказательство не простое и зависит от доказательства .$BFB \in \mathsf{AC^0}$$BFE \in \mathsf{NC^1}$

BFE (оценка булевой формулы)
Учитывая булеву формулу и присваивание правды для переменных в , удовлетворяет ли ( )?$\varphi$$\tau$$\varphi$
$\tau$$\varphi$$\tau \vDash \varphi$

Из знаменитого результата Сэма Бусса известно, что вычисление булевой формулы ( ) может быть вычислено в (см. [Buss87] и [BCGR92] ).$BFE$$\mathsf{NC^1} = \mathsf{ALogTime}$

Из этого (довольно удивительно, по крайней мере для меня) следует, что балансировка булевых формул ( ) также находится в :$BFB$$\mathsf{NC^1}$

Идея состоит в том, что мы можем жестко кодировать во входных воротах чтобы получить формулу, эквивалентную и это полностью синтаксическая операция, вычисляемая в . Поскольку имеет сбалансированные формулы, мы получаем эквивалентную сбалансированную формулу для . Другими словами, алгоритм:$\varphi$$BFE$$\varphi$$\mathsf{AC^0}$$BFE$$\varphi$

мотивация

Более простой аргумент в пользу того, что находится в (или или даже ), даст новое более простое доказательство поскольку легко увидеть, что сбалансированная версия BFE может быть решена в и мы можем составить ее с помощью и результат будет в .$BFB$$\mathsf{AC^0}$$\mathsf{TC^0}$$\mathsf{NC^1}$$BFE \in \mathsf{NC^1}$$\mathsf{NC^1}$$BFB$$\mathsf{NC^1}$

Вопросов

1. Было ли известно, что булевы формулы могут быть сбалансированы в ( )?$\mathsf{AC^0}$$BFB\in \mathsf{AC^1}$
2. Есть ли более простой аргумент (например, не полагаться на ) для ?$BFE\in \mathsf{NC^1}$$BFB\in\mathsf{AC^0}$

Я не уверен, что это очень актуально, но в алгоритмах лог-пространства для путей и сопоставлений в k-деревьях (основанных на долгой истории прошлой работы и, в частности, на арифметизирующих классах вокруг NC1 и L, выполненных Limaye-Mahajan-Rao), мы показываем Как найти рекурсивные сбалансированные разделители для дерева в Logspace. Эта граница вполне может быть улучшенной до если входное дерево напрямую задано в строковом представлении.$\mathsf{NC}^1$

Основная идея состоит в том, чтобы представить дерево в виде выражения в скобках и найти для них сбалансированные разделители. Обратите внимание, что мы находим разделители листьев, то есть поддеревья, которые сбалансированы по числу листьев.