Bilansowanie formuł boolowskich w

Szukam referencji na temat złożoności problemu równoważenia formuł logicznych . W szczególności,

Czy było wiadomo, że formuły logiczne można wyważyć w $\mathsf{AC^0}$ ?
Czy istnieje prosty dowód na to, że równoważenie boolowskiej formuły jest w $\mathsf{AC^0}$ ?

Przez „proste” mam na myśli dowód prostsze niż ten wspominam poniżej, w szczególności szukam dowodu, który nie zależy od oceny formuła logiczna istoty w . $\mathsf{NC^1}$

tło

Tutaj wszystkie wspomniane klasy złożoności są jednolite.

BFB (równoważenie formuły boolowskiej):
Biorąc pod uwagę formułę boolowską , Znajdź równoważną zrównoważoną formułę boolowską. $\varphi$

Interesuje mnie złożoność tego problemu, w szczególności proste dowody pokazujące, że problem występuje w $\mathsf{AC^0}$ (a nawet $\mathsf{TC^0}$ lub $\mathsf{NC^1}$ ). Typowe argumenty równoważenia, takie jak te oparte na lemacie Spiry, stosują powtarzane modyfikacje strukturalne w drzewie formuł, które wydają się dawać tylko $BFB \in \mathsf{NC^2}$ .

Mam dowód na $BFB \in \mathsf{AC^0}$ , jednak dowód nie jest prosty i zależy od dowodu $BFE \in \mathsf{NC^1}$ .

BFE (ocena formuły boolowskiej)
Biorąc pod uwagę formułę boolowską i przypisanie prawdy dla zmiennych w , Czy spełnia ( )? $\varphi$ $\tau$ $\varphi$
$\tau$ $\varphi$ $\tau \vDash \varphi$

Z słynnego wyniku Sama Bussa wiadomo, że ocenę wzoru logicznego ( ) można obliczyć w (patrz [Buss87] i [BCGR92] ). $BFE$ $\mathsf{NC^1} = \mathsf{ALogTime}$

Wynika z (całkiem nieoczekiwanie, że przynajmniej mi), które logiczne wzory równoważenia ( ) jest również : $BFB$ $\mathsf{NC^1}$

Chodzi o to, że możemy zakodować na stałe w bramkach wejściowych aby otrzymać formułę równoważną i jest to całkowicie składniowa operacja obliczalna w . Ponieważ ma zbilansowane wzory, otrzymujemy równoważną zbilansowaną formułę dla . Innymi słowy, algorytm to: $\varphi$ $BFE$ $\varphi$ $\mathsf{AC^0}$ $BFE$ $\varphi$

⌜ φ ⌝ \mapsto ⌜ λ \vec{p} . E v a l (⌜ φ ⌝, \vec{p}) ⌝

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

Motywacja

Prostszy argument dla znajdującego się w (lub lub nawet ) dałby nowy prostszy dowód ponieważ łatwo zauważyć, że zrównoważoną wersję BFE można rozwiązać w a my możemy skomponować ją z a wynik będzie w . $BFB$ $\mathsf{AC^0}$ $\mathsf{TC^0}$ $\mathsf{NC^1}$ $BFE \in \mathsf{NC^1}$ $\mathsf{NC^1}$ $BFB$ $\mathsf{NC^1}$

pytania

Czy wiadomo, że formuły logiczne można wyważyć w ( )? $\mathsf{AC^0}$ $BFB\in \mathsf{AC^1}$
Czy istnieje prostszy argument (np. Nie poleganie na ) dla ? $BFE\in \mathsf{NC^1}$ $BFB\in\mathsf{AC^0}$

— Kaveh
źródło

Jakiej definicji „równowagi” używasz?

— Dana Moshkovitz

@Dana, możemy użyć czegoś takiego jak (tj. z określonymi stałymi). Zobacz także artykuł Bonneta i Bussa „ Kompromis głębokości w odniesieniu do formuł boolowskich ”, 2002.

D e p t h < 10 \lg S i z e + 100

$Depth < 10\lg Size + 100$

D e p t h = O (\lg S i z e)

$Depth = O(\lg Size)$

— Kaveh

uzgodniono, że definicja „bilansowania” powinna zostać wyjaśniona. czy jest to podobne do koncepcji równoważenia drzew binarnych? np. „

— samowyrównujące się

Nie jestem pewien, czy jest to bardzo istotne, ale w Algorytmach przestrzeni logów dla ścieżek i dopasowań w drzewach k (bazując na długiej historii wcześniejszych prac, a konkretnie na klasach arytmetycznych wokół NC1 i L autorstwa Limaye-Mahajan-Rao) pokazujemy jak znaleźć rekurencyjne zrównoważone separatory dla drzewa w Logspace. Ta granica może równie dobrze być poprawialna do jeśli drzewo wejściowe jest podane bezpośrednio w reprezentacji ciągu. $\mathsf{NC}^1$

Podstawową ideą jest przedstawienie drzewa jako wyrażenia w nawiasie i znalezienie dla nich zrównoważonych separatorów. Zauważ, że znajdujemy separatory liści, tj. Poddrzewa, które są zrównoważone względem liczby liści.

— SamiD
źródło