I. Introduction
A non-deterministic boolean branching program (NBP) in its most general form, is a directed acyclic graph (DAG) with a designated source node and a number of output nodes . Non-output nodes can have arbitrary in/out-degree. Some of edges are labeled by an input variable or its negation Given an input assignment values to , we disconnect all edges whose label is false. The value of each is set to if (after disconnecting all edges whose label is false) there is a path (with marked and unmarked edges) from the source node to and otherwise. An NBP is equivalent to a boolean circuit (BC) with inputs and outputs if for every input assignment, the value of each is the same in and in . Figure 1 depicts how parity of six variables can be computed by a BC of depth 6 and size 31 (number of gates) and an equivalent NBP with 11 nodes and 20 edges. By selecting the proper edges the equivalent NBP will compute the correct values in the odd/even outputs. In terms of size, the NBP is smaller than the original . Note that this parity BC is obtained from for-loop (Figure 1 top) via: 1) full unrolling, 2) replacing the assignments by equivalent graph algebraic operations and 3) substituting the BC of each algebraic operation. We refer to this process as converting a computation into an equivalent BC. In this work we consider computation that are for-loops, whose body satisfies that: A) All the addresses of the memory references made during execution can be computed based on the for-Ioop's iteration index, and B) There are no store operations. Clearly, such computations can be converted to an equivalent BCs by full unrolling. In addition, we can also unroll the body times and transform the unrolled body to an equivalent BC.
Parity: BCs and an equivalent NBPs.