Bilansowanie formuł boolowskich w

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

1. Czy było wiadomo, że formuły logiczne można wyważyć w $\mathsf{AC^0}$ ?
2. 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 N C 1 = A L O g T i m e (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ż N C 1 :$BFB$$\mathsf{NC^1}$

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

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

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

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.