Time-space tradeoffs and functional representations via branching programs and their generalizations

This thesis is primarily focussed on time-space tradeoffs for decision problems. Branching programs have turned out to be very useful for this study.; We first resolve some long-standing open problems regarding upper bounds on the branching program size for certain simple functions. We construct branching programs of size o(n log2 n/ log log n) for threshold functions and of size o(n log4 n) for determining the sum of the input bits modulo a fixed divisor. These improve the previously best constructions of O(n 3/2) due to Lupanov [Lup65].; We then consider a restricted class called syntactic read-k branching programs [BRS93] where each variable is tested at most k times on any path. For every k, we exhibit two explicit functions that can be computed by linear-sized read-(k + 1) branching programs but require size $expWn1/k+12-2kk-4$ to be computed by non-deterministic or randomized syntactic read- k branching programs with 2-sided error $3$, for some $3$ > 0. This exponential separation was conjectured by various authors [Weg88, SS93a, Pon95], and was previously known only between k = 1 and k = 2 [Weg88]. For the stronger semantic read- k model, where the read restriction applies only to computation paths, we give the first separation result showing that polynomial-size semantic read-twice branching programs can compute functions that require exponential size on syntactic read-k branching programs.; On the general Boolean branching program model, we obtain the first non-trivial timespace tradeoff lower bound for computing decision problems by exhibiting a Boolean function requiring exponential size to be computed by any branching program of length cn, for some constant c > 1. For the more general R-way branching programs [BRS93], we give, for any k, a function that requires exponential size to be computed by length kn q-way branching programs, for some q = q(k).; Finally, we consider branching programs and their variants such as OBDDs [Bry86], *-BMDs [BC95], HDDs [CFZ95], MTBDDs [CMZ+93] and EVBDDs [LS92], that have been used as representations of Boolean and integer functions for symbolic model checking [McM93]. We introduce a lower bound technique that applies to a broad spectrum of such functional representations. We apply this technique to show exponential size bounds for many integer and Boolean functions that arise in symbolic model checking. We give the first examples of integer functions including integer division, remainder, high/low-order words of multiplication, square root and reciprocal that require exponential size in all these representations.