Formally the theorem states that polynomial-size bounded-width branching programs have the same computation power as Boolean formulas. A branching program is a directed acyclic graph where all but two nodes are labelled by a variable name and has out-degree two: one edge labelled true and the other false. The other two nodes are the terminal nodes labelled accept and reject. There is a single root of in-degree zero. From the root, one follows a path following the true node if the labelled input variable is true and false otherwise and accepting or rejecting the input based on the terminal node reached. Layer the branching program based on the distance of each node from the root and the width is the maximum number of nodes in any layer.
Barrington showed that width-five branching program can simulate any Boolean formula and thus the complexity class NC1 which includes the majority function. But the branching program in any layer can only remember one of five nodes, less than three bits of information as it processes through the graph. Yet you still can tell if a majority of input variables are true. Amazing.
The key to Barrington's proof is that the group S5 (permutations on five elements) is non-solvable i.e., there are permuatations σ = (12345) and τ = (13542) such that στσ-1τ-1 is not the identity permutation. There is a simple write-up of the proof on page 60-61 of the Boppana-Sipser survey.
Some neat consequences of Barrington's theorem.
- Regular languages are NC1-complete under projections of the inputs.
- One can compute any language in PSPACE using not much more than a clock and constant bits of memory. (Cai and Furst)