Research article:
Samuel R. Buss.
"Algorithms for Boolean formula evaluation and for
tree-contraction."
In Proof Theory, Complexity, and Arithmetic,
P. Clote and J. Krajicek (eds), Oxford University Press, 1993, pp. 95-115.
Download article: postscript or PDF.
Abstract: This paper presents a new, simpler
ALOGTIME (alternating logtime) algorithm for the Boolean sentence value problem (BSVP).
Unlike prior work, this algorithm avoids the use of postfix-longer-operand-first formulas.
This paper also shows that tree-contraction can be made ALOGTIME uniform.
The Boolean sentence problem restricted to balanced sentences with only
the connectives $\land$ and $\lor$ is in online $O(\log(\log n))$ space. Hence every
ALOGTIME predicate is deterministic log-time reducible to $\log(\log n)$ space. This
balanced and/or BSVP has logarithmic width, linear length, branching programs.