Boolean formulas and deterministic branching programs

A Boolean formula is a finite rooted tree whose leaves are labelled by input variables or constants $0,1$, and whose internal nodes are NOT gates with one child or AND/OR gates with two children. The root is the output, and evaluation proceeds from leaves to root. A variable or constant may label several distinct leaves; all occurrences of a variable receive the same input value. Thus computed subformulas are not shared, but input variables may be used repeatedly. In the gate-count convention of Boolean circuits: basis, fan-in, size, and depth, its size counts connective gates and constant occurrences, but not variable leaves.

A deterministic branching program is a finite acyclic query graph with a start node and sinks labelled $0$ or $1$. Each internal node is labelled by an input bit and has one outgoing edge labelled $0$ and one outgoing edge labelled $1$; computation follows the edge whose label is the queried bit's value. Its size is its number of vertices. These are distinct size models.