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

10

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

  1. Было ли известно, что булевы формулы могут быть сбалансированы в ?AC0
  2. Есть ли простое доказательство балансировки булевой формулы в ?AC0

Под «простым» я подразумеваю доказательство, более простое, чем упомянутое ниже, в частности, я ищу доказательство, которое не зависит от оценки булевой формулы в .NC1


Фон

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

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

Меня интересует сложность этой проблемы, в частности, простые доказательства, показывающие, что проблема находится в (или даже или ). Обычные аргументы балансировки, подобные тем, которые основаны на лемме Спиры, применяют повторяющиеся структурные модификации дерева формул, которые, похоже, дают только .AC0TC0NC1BFBNC2

У меня есть доказательство для , однако доказательство не простое и зависит от доказательства .BFBAC0BFENC1

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

Из знаменитого результата Сэма Бусса известно, что вычисление булевой формулы ( ) может быть вычислено в (см. [Buss87] и [BCGR92] ).BFENC1=ALogTime

Из этого (довольно удивительно, по крайней мере для меня) следует, что балансировка булевых формул ( ) также находится в :BFBNC1

Идея состоит в том, что мы можем жестко кодировать во входных воротах чтобы получить формулу, эквивалентную и это полностью синтаксическая операция, вычисляемая в . Поскольку имеет сбалансированные формулы, мы получаем эквивалентную сбалансированную формулу для . Другими словами, алгоритм:φBFEφAC0BFEφ

φλp.Eval(φ,p)

мотивация

Более простой аргумент в пользу того, что находится в (или или даже ), даст новое более простое доказательство поскольку легко увидеть, что сбалансированная версия BFE может быть решена в и мы можем составить ее с помощью и результат будет в .BFBAC0TC0NC1BFENC1NC1BFBNC1


Вопросов

  1. Было ли известно, что булевы формулы могут быть сбалансированы в ( )?AC0BFBAC1
  2. Есть ли более простой аргумент (например, не полагаться на ) для ?BFENC1BFBAC0
Кава
источник
3
Какое определение «баланса» вы используете?
Дана Мошковиц
1
@ Дана, мы можем использовать что-то вроде (т.е. с конкретными константами). См. Также статью Боннета и Бусса « Соотношение размера и глубины для булевых формул », 2002 г.Depth<10lgSize+100Depth=O(lgSize)
Каве,
согласился, что определение "балансировки" должно быть ясно это похоже на концепцию балансировки в бинарных деревьях? например, "самоуравновешенные деревья"
vzn

Ответы:

3

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

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

SamiD
источник