Abstract. We consider the time and space required for quantum computers to solve a wide variety of problems involving matrices, many of which have only been analyzed classically in prior work. Our main results show that for a range of linear algebra problems—including matrix-vector product, matrix inversion, matrix multiplication and powering—existing classical time-space tradeoffs, several of which are tight for every space bound, also apply to quantum algorithms with at most a constant factor loss. For example, for almost all fixed matrices [Formula: see text], including the discrete Fourier transform matrix, we prove that quantum circuits with at most [Formula: see text] input queries and [Formula: see text] qubits of memory require [Formula: see text] to compute matrix-vector product [Formula: see text] for [Formula: see text]. We similarly prove that matrix multiplication for [Formula: see text] binary matrices requires [Formula: see text]. Because many of our lower bounds are matched by deterministic algorithms with the same time and space complexity, our results show that quantum computers cannot provide any asymptotic advantage for these problems with any space bound. We obtain matching lower bounds for the stronger notion of quantum cumulative memory complexity—the sum of the space per layer of a circuit. We also consider Boolean (i.e., AND-OR) matrix multiplication and matrix-vector products, improving the previous quantum time-space tradeoff lower bounds for [Formula: see text] Boolean matrix multiplication to [Formula: see text] from [Formula: see text]. Our improved lower bound for Boolean matrix multiplication is based on a new coloring argument that extracts more from the strong direct product theorem that was the basis for prior work. To obtain our tight lower bounds for linear algebra problems, we require much stronger bounds than strong direct product theorems. We obtain these bounds by adding a new bucketing method to the quantum recording-query technique of Zhandry that lets us apply classical arguments to upper bound the success probability of quantum circuits.

We prove lower bounds on the time and space required for quantum computers to solve a wide variety of problems involving matrices, many of which have only been analyzed classically in prior work. Using a novel way of applying recording query methods we show that for many linear algebra problems—including matrix-vector product, matrix inversion, matrix multiplication and powering—existing classical time-space tradeoffs also apply to quantum algorithms with at most a constant factor loss. For example, for almost all fixed matrices A, including the discrete Fourier transform (DFT) matrix, we prove that quantum circuits with at most T input queries and S qubits of memory require T=Ω(n2/S) to compute matrix-vector product Ax for x ∈ {0,1}n. We similarly prove that matrix multiplication for n× n binary matrices requires T=Ω(n3 / √S). Because many of our lower bounds are matched by deterministic algorithms with the same time and space complexity, our results show that quantum computers cannot provide any asymptotic advantage for these problems at any space bound. We also improve the previous quantum time-space tradeoff lower bounds for n× n Boolean (i.e. AND-OR) matrix multiplication from T=Ω(n2.5/S1/2) to T=Ω(n2.5/S1/4) which has optimal exponents for the powerful query algorithms to which it applies. Our method also yields improved lower bounds for classical algorithms.

Cumulative memory - the sum of space used per step over the duration of a computation - is a fine-grained measure of time-space complexity that was introduced to analyze cryptographic applications like password hashing. It is a more accurate cost measure for algorithms that have infrequent spikes in memory usage and are run in environments such as cloud computing that allow dynamic allocation and de-allocation of resources during execution, or when many multiple instances of an algorithm are interleaved in parallel. We prove the first lower bounds on cumulative memory complexity for both sequential classical computation and quantum circuits. Moreover, we develop general paradigms for bounding cumulative memory complexity inspired by the standard paradigms for proving time-space tradeoff lower bounds that can only lower bound the maximum space used during an execution. The resulting lower bounds on cumulative memory that we obtain are just as strong as the best time-space tradeoff lower bounds, which are very often known to be tight. Although previous results for pebbling and random oracle models have yielded time-space tradeoff lower bounds larger than the cumulative memory complexity, our results show that in general computational models such separations cannot follow from known lower bound techniques and are not true for many functions. Among many possible applications of our general methods, we show that any classical sorting algorithm with success probability at least 1/poly(n) requires cumulative memory ̃ Ω(n²), any classical matrix multiplication algorithm requires cumulative memory Ω(n⁶/T), any quantum sorting circuit requires cumulative memory Ω(n³/T), and any quantum circuit that finds k disjoint collisions in a random function requires cumulative memory Ω(k³n/T²).

Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer mul-tipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.

Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SATbased bit-vector solvers.Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved.Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bit-level reasoning.We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses.Theoretically, we show that there are optimal-length cutting planes proofs for a large class of bit-level properties of some well known multiplier circuits.This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods.We also show that cutting planes reasoning can extract bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases.Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods.We then go further than previous approaches and also verify these properties at the bit-level.Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers.

We study the bias of random bounded-degree polynomials over odd prime fields and show that, with probability exponentially close to 1, $n$-variate polynomials of degree $d$ over $\mathbb{F}_p$ have bias at most $p^{-\Omega(n/d)}$. This also yields an exponential tail bound on the weight distribution of Reed--Muller codes over odd prime fields. These results generalize bounds of Ben-Eliezer, Hod, and Lovett [ Comput. Complexity, 21 (2012), pp. 63--81] who proved similar results over $\mathbb{F}_2$. Our bounds are based on an extremal property of the rank of sub-matrices of the generator matrices of Reed--Muller codes over odd prime fields that generalizes a property shown by Keevash and Sudakov [ SIAM J. Discrete Math., 18 (2005), pp. 713--727] for the case of $\mathbb{F}_2$. Our tail bounds on the bias can be used to derive exponential lower bounds on the time for space-bounded learning of bounded-degree polynomials from their evaluations over odd prime fields.

We study the task of estimating the number of edges in a graph, where the access to the graph is provided via an independent set oracle. Independent set queries draw motivation from group testing and have applications to the complexity of decision versus counting problems. We give two algorithms to estimate the number of edges in an n -vertex graph, using (i) polylog( n ) bipartite independent set queries or (ii) n 2/3 polylog( n ) independent set queries.

We study the task of smoothing a circuit, i.e., ensuring that all children of a plus-gate mention the same variables. Circuits serve as the building blocks of state-of-the-art inference algorithms on discrete probabilistic graphical models and probabilistic programs. They are also important for discrete density estimation algorithms. Many of these tasks require the input circuit to be smooth. However, smoothing has not been studied in its own right yet, and only a trivial quadratic algorithm is known. This paper studies efficient smoothing for structured decomposable circuits. We propose a near-linear time algorithm for this task and explore lower bounds for smoothing decomposable circuits, using existing results on range-sum queries. Further, for the important case of All-Marginals, we show a more efficient linear-time algorithm. We validate experimentally the performance of our methods.

We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give n O (1) size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and n O (log n ) size proofs for these identities on Wallace tree multipliers.

We develop an extension of recent analytic methods for obtaining time-space tradeoff lower bounds for problems of learning from uniformly random labelled examples. With our methods we can obtain bounds for learning concept classes of finite functions from random evaluations even when the sample space of random inputs can be significantly smaller than the concept class of functions and the function values can be from an arbitrary finite set. At the core of our results, we reduce the time-space complexity of learning from random evaluations to the question of how much the corresponding evaluation matrix amplifies the 2-norms of “almost uniform” probability distributions. To analyze the latter, we formulate it as a semidefinite program, and we analyze its dual. In order to handle function values from arbitrary finite sets, we apply this norm amplification analysis to complex matrices. As applications that follow from our new techniques, we show that any algorithm that learns $n$-variate polynomial functions of degree at most $d$ over $\mathbb{F}_2$ with success at least $2^{-O(n)}$ from evaluations on randomly chosen inputs either requires space $\Omega(nm/d)$ or $2^{\Omega(n/d)}$ time where $m=(n/d)^{\Theta(d)}$ is the dimension of the space of such polynomials. These bounds are asymptotically optimal for polynomials of arbitrary constant degree since they match the tradeoffs achieved by natural learning algorithms for the problems. We extend these results to learning polynomials of degree at most $d$ over any odd prime field $\mathbb{F}_p$ where we show that $\Omega((mn/d)\log p)$ space or time $p^{\Omega(n/d)}$ is required. To derive our bounds for learning polynomials over finite fields, we show that an analysis of the dual of the corresponding semidefinite program follows from an understanding of the distribution of the bias of all degree $d$ polynomials with respect to uniformly random inputs.

We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane a x >= b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x >= b, the points satisfying a x <= b-1, and the middle slab b-1 < a x < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show somewhat surprisingly that Stabbing Planes can efficiently simulate Cutting Planes, and moreover, is strictly stronger than Cutting Planes under a reasonable conjecture. We prove linear lower bounds on the rank of Stabbing Planes refutations, by adapting a lifting argument in communication complexity.

We study distributed protocols for finding all pairs of similar vectors in a large dataset. Our results pertain to a variety of discrete metrics, and we give concrete instantiations for Hamming distance. In particular, we give improved upper bounds on the overhead required for similarity defined by Hamming distance r > 1 and prove a lower bound showing qualitative optimality of the overhead required for similarity over any Hamming distance r. Our main conceptual contribution is a connection between similarity search algorithms and certain graph-theoretic quantities. For our upper bounds, we exhibit a general method for designing one-round protocols using edge-isoperimetric shapes in similarity graphs. For our lower bounds, we define a new combinatorial optimization problem, which can be stated in purely graph-theoretic terms yet also captures the core of the analysis in previous theoretical work on distributed similarity joins. As one of our main technical results, we prove new bounds on distance correlations in subsets of the Hamming cube.

We study the problem of computing conjunctive queries over large databases on parallel architectures without shared storage. Using the structure of such a queryqand the skew in the data, we study tradeoffs between the number of processors, the number of rounds of communication, and the per-processorload—the number of bits each processor can send or can receive in a single round—that are required to computeq. Since each processor must store its received bits, the load is at most the number of bits of storage per processor. When the data are free of skew, we obtain essentially tight upper and lower bounds for one round algorithms, and we show how the bounds degrade when there is skew in the data. In the case of skewed data, we show how to improve the algorithms when approximate degrees of the (necessarily small number of) heavy-hitter elements are available, obtaining essentially optimal algorithms for queries such as skewed simple joins and skewed triangle join queries. For queries that we identify astreelike, we also prove nearly matching upper and lower bounds for multi-round algorithms for a natural class of skew-free databases. One consequence of these latter lower bounds is that for any ε > 0, usingpprocessors to compute the connected components of a graph, or to output the path, if any, between a specified pair of vertices of a graph withmedges and per-processor load that isO(m/p1−ε) requires Ω(logp) rounds of communication. Our upper bounds are given by simple structured algorithms using MapReduce. Our one-round lower bounds are proved in a very general model, which we call theMassively Parallel Communication (MPC)model, that allows processors to communicate arbitrary bits. Our multi-round lower bounds apply in a restricted version of the MPC model in which processors in subsequent rounds after the first communication round are only allowed to send tuples.

We prove exponential lower bounds on the running time of the state-of-the-art exact model counting algorithms—algorithms for exactly computing the number of satisfying assignments, or the satisfying probability, of Boolean formulas. These algorithms can be seen, either directly or indirectly, as building Decision-Decomposable Negation Normal Form (decision-DNNF) representations of the input Boolean formulas. Decision-DNNFs are a special case of d -DNNFs where d stands for deterministic . We show that any knowledge compilation representations from a class (called DLDDs in this article) that contain decision-DNNFs can be converted into equivalent Free Binary Decision Diagrams (FBDDs) , also known as Read-Once Branching Programs , with only a quasi-polynomial increase in representation size. Leveraging known exponential lower bounds for FBDDs, we then obtain similar exponential lower bounds for decision-DNNFs, which imply exponential lower bounds for model-counting algorithms. We also separate the power of decision-DNNFs from d -DNNFs and a generalization of decision-DNNFs known as AND-FBDDs. We then prove new lower bounds for FBDDs that yield exponential lower bounds on the running time of these exact model counters when applied to the problem of query evaluation in tuple-independent probabilistic databases—computing the probability of an answer to a query given independent probabilities of the individual tuples in a database instance. This approach to the query evaluation problem, in which one first obtains the lineage for the query and database instance as a Boolean formula and then performs weighted model counting on the lineage, is known as grounded inference . A second approach, known as lifted inference or extensional query evaluation , exploits the high-level structure of the query as a first-order formula. Although it has been widely believed that lifted inference is strictly more powerful than grounded inference on the lineage alone, no formal separation has previously been shown for query evaluation. In this article, we show such a formal separation for the first time. In particular, we exhibit a family of database queries for which polynomial-time extensional query evaluation techniques were previously known but for which query evaluation via grounded inference using the state-of-the-art exact model counters requires exponential time.

In this paper, we study the communication complexity for the problem of computing a conjunctive query on a large database in a parallel setting with p servers. In contrast to previous work, where upper and lower bounds on the communication were specified for particular structures of data (either data without skew, or data with specific types of skew), in this work we focus on worst-case analysis of the communication cost. The goal is to find worst-case optimal parallel algorithms, similar to the work of (Ngo et al. 2012) for sequential algorithms. We first show that for a single round we can obtain an optimal worst-case algorithm. The optimal load for a conjunctive query q when all relations have size equal to M is O(M/p^{1/psi^*}), where psi^* is a new query-related quantity called the edge quasi-packing number, which is different from both the edge packing number and edge cover number of the query hypergraph. For multiple rounds, we present algorithms that are optimal for several classes of queries. Finally, we show a surprising connection to the external memory model, which allows us to translate parallel algorithms to external memory algorithms. This technique allows us to recover (within a polylogarithmic factor) several recent results on the I/O complexity for computing join queries, and also obtain optimal algorithms for other classes of queries.

We give the first time-space trade-off lower bounds for resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size $N$ that have resolution refutations of size (and space) $T(N)= N^{\Theta(\log N)}$ (and like all formulas have another resolution refutation of space $N$) but for which no resolution refutation can simultaneously have space $S(N) = T(N)^{o(1)}$ and size $T(N)^{O(1)}$. In other words, any substantial reduction in space results in a super-polynomial increase in total size. We also show somewhat stronger time-space trade-off lower bounds for regular resolution, which are also the first to apply to superlinear space. For any function $T$ that is at most weakly exponential, $T(N) = 2^{o(N^{1/4})}$, we give a tautology that has regular resolution proofs of size and space $T(N)$, but no such proofs with space $S(N) = T(N)^{1-\Omega(1)}$ and size $T(N)^{O(1)}$. Thus, any polynomial reduction in space has a superpolynomial cost in size. These tautologies are width 4 disjunctive normal form (DNF) formulas.

The FO Model Counting problem (FOMC) is the following: given a sentence Φ in FO and a number n, compute the number of models of Φ over a domain of size n; the Weighted variant (WFOMC) generalizes the problem by associating a weight to each tuple and defining the weight of a model to be the product of weights of its tuples. In this paper we study the complexity of the symmetric WFOMC, where all tuples of a given relation have the same weight. Our motivation comes from an important application, inference in Knowledge Bases with soft constraints, like Markov Logic Networks, but the problem is also of independent theoretical interest. We study both the data complexity, and the combined complexity of FOMC and WFOMC. For the data complexity we prove the existence of an FO3 formula for which FOMC is #P1-complete, and the existence of a Conjunctive Query for which WFOMC is #P1-complete. We also prove that all γ-acyclic queries have polynomial time data complexity. For the combined complexity, we prove that, for every fragment FOk, k ≥ 2, the combined complexity of FOMC (or WFOMC) is #P-complete.

Propositional satisfiability (SAT) solvers based on conflict directed clause learning (CDCL) implicitly produce resolution refutations of unsatisfiable formulas. The precise class of formulas for which they can produce polynomial size refutations has been the subject of several studies, with special focus on the clause learning aspect of these solvers. The results, however, assume the use of non-standard and non-asserting learning schemes, or rely on polynomially many restarts for simulating individual steps of a resolution refutation, or work with a theoretical model that significantly deviates from certain key aspects of all modern CDCL solvers such as learning only one asserting clause from each conflict and other techniques such as conflict guided backjumping and phase saving. We study non-restarting CDCL solvers that learn only one asserting clause per conflict and show that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. We show, moreover, that this preprocessing allows one to convert any CDCL solver to one that is non-restarting.

We study the problem of computing a conjunctive query q in parallel, using p of servers, on a large database. We consider algorithms with one round of communication, and study the complexity of the communication. We are especially interested in the case where the data is skewed, which is a major challenge for scalable parallel query processing. We establish a tight connection between the fractional edge packing of the query and the amount of communication in two cases. First, in the case when the only statistics on the database are the cardinalities of the input relations, and the data is skew-free, we provide matching upper and lower bounds (up to a polylogarithmic factor of p) expressed in terms of fractional edge packings of the query q. Second, in the case when the relations are skewed and the heavy hitters and their frequencies are known, we provide upper and lower bounds expressed in terms of packings of residual queries obtained by specializing the query to a heavy hitter. All our lower bounds are expressed in the strongest form, as number of bits needed to be communicated between processors with unlimited computational power. Our results generalize prior results on uniform databases (where each relation is a matching) [4], and lower bounds for the MapReduce model [1].

We derive new time-space tradeoff lower bounds and algorithms for exactly computing statistics of input data, including frequency moments, element distinctness, and order statistics, that are simple to calculate for sorted data. We develop a randomized algorithm for the element distinctness problem whose time T and space S satisfy T ∈ Õ (n3/2/S1/2), smaller than previous lower bounds for comparison-based algorithms, showing that element distinctness is strictly easier than sorting for randomized branching programs. This algorithm is based on a new time and space efficient algorithm for finding all collisions of a function f from a finite set to itself that are reachable by iterating f from a given set of starting points. We further show that our element distinctness algorithm can be extended at only a polylogarithmic factor cost to solve the element distinctness problem over sliding windows, where the task is to take an input of length 2n-1 and produce an output for each window of length n, giving n outputs in total. In contrast, we show a time-space tradeoff lower bound of T ∈ Ω(n2/S) for randomized branching programs to compute the number of distinct elements over sliding windows. The same lower bound holds for computing the low-order bit of F0and computing any frequency moment Fk,≠1. This shows that those frequency moments and the decision problem F0mod 2 are strictly harder than element distinctness. We complement this lower bound with a T ∈ Õ(n2/S) comparison-based deterministic RAM algorithm for exactly computing Fkover sliding windows, nearly matching both our lower bound for the sliding-window version and the comparison-based lower bounds for the single-window version. We further exhibit a quantum algorithm for F0over sliding windows with T ∈ O(n3/2/S1/2). Finally, we consider the computations of order statistics over sliding windows.

We consider the problem of computing a relational query q on a large input database of size n, using a large number p of servers. The computation is performed in rounds, and each server can receive only O(n/p1-ε) bits of data, where ε ∈[0,1] is a parameter that controls replication. We examine how many global communication steps are needed to compute q. We establish both lower and upper bounds, in two settings. For a single round of communication, we give lower bounds in the strongest possible model, where arbitrary bits may be exchanged; we show that any algorithm requires ε ≥ 1--1/τ*, where τ* is the fractional vertex cover of the hypergraph of q. We also give an algorithm that matches the lower bound for a specific class of databases. For multiple rounds of communication, we present lower bounds in a model where routing decisions for a tuple are tuple-based. We show that for the class of tree-like queries there exists a tradeoff between the number of rounds and the space exponent ε. The lower bounds for multiple rounds are the first of their kind. Our results also imply that transitive closure cannot be computed in O(1) rounds of communication.

We show how to approximate any function in AC0by decision trees of much smaller height than its number of variables. More precisely, we show that any function in n variables computable by an unbounded fan-in circuit of AND, OR, and NOT gates that has size S and depth d can be approximated by a decision tree of height n - βn to within error exp(-βn), where β = β(S, d) = 2-O(d log4/5S). Our proof is constructive and we use its constructivity to derive a deterministic algorithm for #AC0SAT with multiplicative factor savings over the naive 2nS algorithm of 2-Ω(βn), when applied to any n-input AC0circuit of size S and depth d. Indeed, in the same running time we can deterministically construct a decision tree of size at most 2n-βnthat exactly computes the function given by such a circuit. Recently, Impagliazzo, Matthews, and Paturi derived an algorithm for #AC0SAT with greater savings over the naive algorithm but their algorithm is only randomized rather than deterministic. The main technical result we prove to show the above is that for every family F of k-DNF formulas in n variables and every 1poly(k)|F|, one can construct a distribution on restrictions that each set at most n/C variables such that, except with probability at most2-n/(2O(k)Clog|T|), after application of the restriction, all formulas in F simultaneously reduce to logpoly(k)|F|-juntas where an s-junta is a function whose value depends on only s of its inputs. Previously, Ajtai showed simultaneous approximations for k-DNF formulas by juntas related to the one we show but with a dependence on exp(k) rather than poly(k), resulting in a weaker height-approximation tradeoff than ours.

We give the first time-space tradeoff lower bounds for Resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size N that have Resolution refutations of space and size each roughly Nlog2 N (and like all formulas have Resolution refutations of space N) for which any Resolution refutation using space S and length T requires T ≥ (N0.58 log2 N/S)Ω(log log N/log log log N). By downward translation, a similar tradeoff applies to all smaller space bounds.

We prove an $n^{\Omega(1)}/4^k$ lower bound on the randomized k-party communication complexity of depth 4 $\ensuremath {\sf AC}^0$ functions in the number-on-forehead (NOF) model for up to $\Theta(\log n)$ players. These are the first nontrivial lower bounds for general NOF multiparty communication complexity for any $\ensuremath {\sf AC}^0$ function for $\omega(\log\log n)$ players. For nonconstant k the bounds are larger than all previous lower bounds for any $\ensuremath {\sf AC}^0$ function even for simultaneous communication complexity. Our lower bounds imply the first superpolynomial lower bounds for the simulation of $\ensuremath {\sf AC}^0$ by $\ensuremath {\sf MAJ\circ SYM\circ AND}$ circuits, showing that the well-known quasi-polynomial simulations of $\ensuremath {\sf AC}^0$ by such circuits due to Allender (1989) and Yao (1990) are qualitatively optimal,-1pt even for formulas of small constant depth. We also exhibit a depth 5 formula in ${\ensuremath {\sf NP}^{cc}_k}-{\ensuremath {\sf BPP}^{cc}_k}$ for k up to $\Theta(\log n)$ and derive $\Omega(2^{\sqrt{\log n}/\sqrt{k}})$ lower bound on the randomized k-party NOF communication complexity of set disjointness for up to $\Theta(\log^{1/3} n)$ players, which is significantly larger than the $O(\log\log n)$ players allowed in the best previous lower bounds for multiparty set disjointness. We prove other strong results for depth 3 and 4 $\ensuremath {\sf AC}^0$ functions.

We prove a time-space tradeoff lower bound of T = Ω (n log(n/s) log log(n/s)) for randomized oblivious branching programs to compute 1GAP, also known as the pointer jumping problem, a problem for which there is a simple deterministic time n and space O(log n) RAM (random access machine) algorithm. We give a similar time-space tradeoff of T = Ω (n log(n/s) log log(n/s)) for Boolean randomized oblivious branching programs computing GIP-MAP, a variation of the generalized inner product problem that can be computed in time n and space O(log2n) by a deterministic Boolean branching program. These are also the first lower bounds for randomized oblivious branching programs computing explicit functions that apply for T = ω(n log n). They also show that any simulation of general branching programs by randomized oblivious ones requires either a superlogarithmic increase in time or an exponential increase in space.

We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems -- tree resolution -- into formulas that require large rank in very strong proof systems, including any proof system that manipulates polynomials of degree at most k (known as Th(k) proofs). These include high degree versions of Lovasz-Schrijver and Cutting Planes proofs.

We prove an n¿(-1)/4klower bound on the randomized k-party communication complexity of depth 4 AC0functions in the number-on-forehead (NOF) model for up to ¿(log n) players. These are the first non-trivial lower bounds for general NOF multiparty communication complexity for any AC0function for ¿ (log log n) players. For non-constant k the bounds are larger than all previous lower bounds for any AC0function even for simultaneous communication complexity. Our lower bounds imply the first superpolynomial lower bounds for the simulation of AC0by MAJ o SYMM o AND circuits, showing that the well-known quasipolynomial simulations of AC0by such circuits are qualitatively optimal, even for formulas of small constant depth. We also exhibit a depth 5 formula in NPkcc- BPPkccfor k up to ¿(log n) and derive an ¿(2¿(log n/ ¿(k))) lower bound on the randomized k-party NOF communication complexity of set disjointness for up to ¿(log1/3n) players which is significantly larger than the O (log log n) players allowed in the best previous lower bounds for multiparty set disjointness. We prove other strong results for depth 3 and 4 AC0functions.

We consider the read/write streams model, an extension of the standard data stream model in which an algorithm can create and manipulate multiple read/write streams in addition to its input data stream. We show that any randomized read/write stream algorithm with a fixed number of streams and a sublogarithmic number of passes that produces a constant factor approximation of the k-th frequency moment Fkof an input sequence of length of at most N from {1, ..., N} requires space Omega(N1-4/k-delta) for any delta > 0. For comparison, it is known that with a single read-only data stream there is a randomized constant- factor approximation for Fkusing O(N1-2/k) space and that there is a deterministic algorithm computing Fkexactly using 3 read/write streams, O(log N) passes, and O(log N) space. Therefore, although the ability to manipulate multiple read/write streams can add substantial power to the data stream model, with a sub-logarithmic number of passes this does not significantly improve the ability to approximate higher frequency moments efficiently. Our lower bounds also apply to (1 + epsi)-approximations of Fkfor epsi ges 1/N.

Motivated by the capabilities of modern storage architectures, we consider the following generalization of the data stream model where the algorithm has sequential access to multiple streams. Unlike the data stream model, where the stream is read only, in this new model (introduced in [8,9]) the algorithms can also write onto streams. There is no limit on the size of the streams but the number of passes made on the streams is restricted. On the other hand, the amount of internal memory used by the algorithm is scarce, similar to data stream model.

We prove that an $\omega(\log^4 n)$ lower bound for the three-party number-on-the-forehead (NOF) communication complexity of the set-disjointness function implies an $n^{\omega(1)}$ size lower bound for treelike Lovász–Schrijver systems that refute unsatisfiable formulas in conjunctive normal form (CNFs). More generally, we prove that an $n^{\Omega(1)}$ lower bound for the $(k+1)$-party NOF communication complexity of set disjointness implies a $2^{n^{\Omega(1)}}$ size lower bound for all treelike proof systems whose formulas are degree k polynomial inequalities.

We prove that two-party randomized communication complexity satisfies a strong direct product property, so long as the communication lower bound is proved by a “corruption” or “one-sided discrepancy” method over a rectangular distribution. We use this to prove new n Ω(1) lower bounds for 3-player number-on-the-forehead protocols in which the first player speaks once and then the other two players proceed arbitrarily. Using other techniques, we also establish an Ω(n 1/(k−1)/(k − 1)) lower bound for k-player randomized number-on-the-forehead protocols for the disjointness function in which all messages are broadcast simultaneously. A simple corollary of this is that general randomized number-on-the-forehead protocols require Ω(log n/(k − 1)) bits of communication to compute the disjointness function.

We prove that corruption, one of the most powerful measures used to analyze 2-party randomized communication complexity, satisfies a strong direct sum property under rectangular distributions. This direct sum bound holds even when the error is allowed to be exponentially close to 1. We use this to analyze the complexity of the widely-studied set disjointness problem in the usual "number-on-the-forehead" (NOF) model of multiparty communication complexity.

Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as verification, planning and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system (CL), and begins the task of understanding its power by relating it to the well-studied resolution proof system. In particular, we show that with a new learning scheme, CL can provide exponentially shorter proofs than many proper refinements of general resolution (RES) satisfying a natural property. These include regular and Davis-Putnam resolution, which are already known to be much stronger than ordinary DPLL. We also show that a slight variant of CL with unlimited restarts is as powerful as RES itself. Translating these analytical results to practice, however, presents a challenge because of the nondeterministic nature of clause learning algorithms. We propose a novel way of exploiting the underlying problem structure, in the form of a high level problem description such as a graph or PDDL specification, to guide clause learning algorithms toward faster solutions. We show that this leads to exponential speed-ups on grid and randomized pebbling problems, as well as substantial improvements on certain ordering formulas.

We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle $PHP^{m}_n$ where $m= (1+1/{ípolylog n})n$. This lower bound qualitatively matches the known quasi-polynomial-size bounded-depth Frege proofs for these principles. Our technique, which uses a switching lemma argument like other lower bounds for bounded-depth Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.

A fruitful connection between algorithm design and proof complexity is the formalization of the DPLL approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions of the DPLL approach that add some version of memoization, remembering formulas the algorithm has previously shown unsatisfiable. Various versions of such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability (S. M. Majercik et al., 1998; F. Bacchus et al., 2003). We formalize this method, and characterize the strength of various versions in terms of proof systems. These proof systems seem to be both new and simple, and have a rich structure. We compare their strength to several studied proof systems: tree-like resolution, regular resolution, general resolution, and Res(k). We give both simulations and separations.

We prove the first time-space lower bound trade-offs for randomized computation of decision problems. The bounds hold even in the case that the computation is allowed to have arbitrary probability of error on a small fraction of inputs. Our techniques are extension of those used by Ajtai and by Beame, Jayram, and Saks that applied to deterministic branching programs. Our results also give a quantitative improvement over the previous results.Previous time-space trade-off results for decision problems can be divided naturally into results for functions with Boolean domain , that is, each input variable is {0,1}-valued, and the case of large domain , where each input variable takes on values from a set whose size grows with the number of variables.In the case of Boolean domain, Ajtai exhibited an explicit class of functions, and proved that any deterministic Boolean branching program or RAM using space S = o ( n ) requires superlinear time T to compute them. The functional form of the superlinear bound is not given in his paper, but optimizing the parameters in his arguments gives T = Ω( n log log n /log log log n ) for S = O ( n 1-ϵ ). For the same functions considered by Ajtai, we prove a time-space trade-off (for randomized branching programs with error) of the form T = Ω( n √ log( n/S )/log log ( n/S )). In particular, for space O ( n 1-ϵ ), this improves the lower bound on time to Ω( n √ log n /log log n ).In the large domain case, we prove lower bounds of the form T = Ω( n √ log( n/S )/log log ( n/S )) for randomized computation of the element distinctness function and lower bounds of the form T = Ω( n log ( n/S )) for randomized computation of Ajtai's Hamming closeness problem and of certain functions associated with quadratic forms over large fields.

The first non-trivial time-space tradeoff lower bounds have been shown for decision problems in P using notions derived from the study of two-party communication complexity. These results are proven directly for branching programs, natural generalizations of decision trees to directed graphs that provide elegant models of both non-uniform time T and space S simultaneously. We develop a new lower bound criterion, based on extending two-party communication complexity ideas to multiparty communication complexity. Applying this criterion to an explicit Boolean function based on a multilinear form over F/sub 2/. for suitable s, we show lower bounds that yield T = /spl Omega/(n log/sup 2/ n) when S /spl les/ n/sup 1-/spl epsi// log |D| for large input domain D. Finally, we develop lower bounds for nearest-neighbor problems involving n data points in a variety of d-dimensional metric spaces.

We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHP/sub n//sup m/ where m = (1 + 1/polylog n)n. This lower bound qualitatively matches the known quasipolynomial-size bounded-depth Frege proofs for these principles. Our technique, which uses a switching lemma argument like other lower bounds for bounded-depth Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.

(MATH) We extend recent techniques for time-space tradeoff lower bounds using multiparty communication complexity ideas. Using these arguments, for inputs from large domains we prove larger tradeoff lower bounds than previously known for general branching programs, yielding time lower bounds of the form $T=\Omega(n\log^2 n)$ when space $S=n^{1-\epsilon}$, up from $T=\Omega(n\log n)$ for the best previous results. We also prove the first unrestricted separation of the power of general and oblivious branching programs by proving that \onegap, which is trivial on general branching programs, has a time-space tradeoff of the form $T=\Omega(n\log^2 (n/S))$ on oblivious branching programs.Finally, using time-space tradeoffs for branching programs, we improve the lower bounds on query time of data structures for nearest neighbor problems in $d$ dimensions from $\Omega(d/\log n)$, proved in the cell-probe model \cite{bor:nn-lb,br:nn-lb}, to $\Omega(d)$ or $\Omega(d\sqrt{\log d/\log\log d})$ or even $\Omega(d\log d)$ (depending on the metric space involved) in slightly less general but more reasonable data structure models.

We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisfiable. First, building on the work of Clegg, Edmonds, and Impagliazzo in [Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, Philadelphia, PA, 1996, ACM, New York, 1996, pp. 174--183], we give an algorithm for unsatisfiability that when given an unsatisfiable formula of F finds a resolution proof of F. The runtime of our algorithm is subexponential in the size of the shortest resolution proof of F. Next, we investigate a class of backtrack search algorithms for producing resolution refutations of unsatisfiability, commonly known as Davis--Putnam procedures, and provide the first asymptotically tight average-case complexity analysis for their behavior on random formulas. In particular, for a simple algorithm in this class, called ordered DLL, we prove that the running time of the algorithm on a randomly generated k-CNF formula with n variables and m clauses is $2^{\Theta(n(n/m)^{1/(k-2)})}$ with probability $1-o(1)$. Finally, we give new lower bounds on $\mbox{res}(F)$, the size of the smallest resolution refutation of F, for a class of formulas representing the pigeonhole principle and for randomly generated formulas. For random formulas, Chvatal and Szemeredi [J. ACM, 35 (1988), pp. 759--768] had shown that random 3-CNF formulas with a linear number of clauses require exponential size resolution proofs, and Fu [On the Complexity of Proof Systems, Ph.D. thesis, University of Toronto, Toronto, ON, Canada, 1995] extended their results to k-CNF formulas. These proofs apply only when the number of clauses is $\Omega(n \log n)$. We show that a lower bound of the form $2^{n^{\gamma}}$ holds with high probability even when the number of clauses is $n^{(k+2)/4-\epsilon}$.

We consider the problem of providing a resolution proof of the statement that a given graph with n vertices and /spl Delta/n edges does not contain an independent set of size k. For randomly chosen graphs with constant /spl Delta/, we show that such proofs almost surely require size exponential in n. Further, for /spl Delta/=o(n/sup 1/5/) and any k/spl les/n/5, we show that these proofs almost surely require size 2(n/sup /spl delta//) for some global constant /spl delta/>0, even though the largest independent set in graphs with /spl Delta//spl ap/n/sup 1/5/ is much smaller than n/5. Our result shows that almost all instances of the independent set problem are hard for resolution. It also provides a lower bound on the running time of a certain class of search algorithms for finding a largest independent set in a given graph.

We give the first example of a sharp threshold in proof complexity. More precisely, we show that for any sufficiently small � and � � �, random formulas consisting of 2-clauses and 3-clauses, which are known to be unsatisfiable almost certainly, almost certainly require resolution and Davis-Putnam proofs of unsatisfiability of exponential size, whereas it is easily seen that random formulas with 2-clauses (and 3-clauses) have linear size proofs of unsatisfiability almost certainly. A consequence of our result also yields the first proof that typical random 3-CNF formulas at ratios below the generally accepted range of the satisfiability threshold (and thus expected to be satisfiable almost certainly) cause natural Davis-Putnam algorithms to take exponential time to find satisfying assignments.

Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic modal checking for systems specified as statecharts. We used these techniques in our analyses of the models of a collision avoidance system and a fault-tolerant electrical power distribution (EPD) system, both used on commercial aircraft. The techniques together reduce the time and space requirements by orders of magnitude, making feasible some analysis that was previously intractable. We also elaborate on the results of verifying the EPD model. The analysis disclosed subtle modeling and logical flaws not found by simulation.

We prove the first time-space lower bound tradeoffs for randomized computation of decision problems. The bounds hold even in the case that the computation is allowed to have arbitrary probability of error on a small fraction of inputs. Our techniques are an extension of those used by M. Ajtai (1999) in his time-space tradeoffs for deterministic RAM algorithms computing element distinctness and for deterministic Boolean branching programs computing an explicit function based on quadratic forms over GF(2). Our results also give a quantitative improvement over those given by Ajtai. Ajtai shows, for certain specific functions, that any branching program using space S=o(n) requires time T that is superlinear. The functional form of the superlinear bound is not given in his paper, but optimizing the parameters in his arguments gives T= /spl Omega/(n log log n/log log log n) for S=0(n/sup 1-/spl epsiv//). For the same functions considered by Ajtai, we prove a time-space tradeoff of the form T=/spl Omega/(n/spl radic/(log(n/S)/log log(n/S))). In particular for space 0(n/sup 1-/spl epsiv//), this improves the lower bound on time to /spl Omega/(n/spl radic/(log n/log log n)).

Article Free Access Share on Decoupling synchronization from local control for efficient symbolic model checking of statecharts Authors: William Chan Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , Richard J. Anderson Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , Paul Beame Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , David H. Jones The Boeing Company, Seattle, Washington The Boeing Company, Seattle, WashingtonView Profile , David Notkin Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, WashingtonView Profile , William E. Warner The Boeing Company, Seattle, Washington The Boeing Company, Seattle, WashingtonView Profile Authors Info & Claims ICSE '99: Proceedings of the 21st international conference on Software engineeringMay 1999 Pages 142–151https://doi.org/10.1145/302405.302460Online:16 May 1999Publication History 13citation235DownloadsMetricsTotal Citations13Total Downloads235Last 12 Months7Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

We obtain matching upper and lower bounds for the amount of time to find the predecessor of a given element among the elements of a fixed efficiently stored set.Our algorithms are for the unit-cost word-level RAM with multiplication and extend to give optimal dynamic algorithms.The lower bounds are proved in a much stronger communication game model, but they apply to the cell probe and RAM models and to both static and dynamic predecessor problems.

We prove a time-space tradeoff for traversing undirected graphs, using a structured model that is a nonjumping variant of Cook and Rackoff's "jumping automata for graphs."

We obtain the first non-trivial time-space tradeoff lower bound for functions f: {0,1}/sup n//spl rarr/{0,1} on general branching programs by exhibiting a Boolean function f that requires exponential size to be computed by any branching program of length (1+/spl epsiv/)n, for some constant /spl epsiv/>0. We also give the first separation result between the syntactic and semantic read-k models for k>1 by showing that polynomial-size semantic read-twice branching programs can compute functions that require exponential size on any syntactic read-k branching program. We also show a time-space tradeoff result on the more general R-way branching program model: for any k, we give a function that requires exponential size to be computed by length kn q-way branching programs, for some q=q(k).

We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques in our analysis of the system requirements specification of TCAS II, a complex aircraft collision avoidance system. They together reduce the time and space complexities by orders of magnitude, making feasible some analysis that was previously intractable. The TCAS II requirements were written in RSML, a dialect of state-charts.

Article Free Access Share on On the complexity of unsatisfiability proofs for random k-CNF formulas Authors: Paul Beame Computer Science, and Engineering, University of Washington, Box 352350, Seattle, WA Computer Science, and Engineering, University of Washington, Box 352350, Seattle, WAView Profile , Richard Karp Computer Science and Engineering, University of Washington Box, 352350, Seattle, WA Computer Science and Engineering, University of Washington Box, 352350, Seattle, WAView Profile , Toniann Pitassi Computer Science Department, University of Arizona, Tucson, AZ Computer Science Department, University of Arizona, Tucson, AZView Profile , Michael Saks Department of Mathematics, Rutgers University, New Brunswick, NJ Department of Mathematics, Rutgers University, New Brunswick, NJView Profile Authors Info & Claims STOC '98: Proceedings of the thirtieth annual ACM symposium on Theory of computingMay 1998 Pages 561–571https://doi.org/10.1145/276698.276870Online:23 May 1998Publication History 47citation495DownloadsMetricsTotal Citations47Total Downloads495Last 12 Months24Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems.

We give simple new lower bounds on the lengths of resolution proofs for the pigeonhole principle and for randomly generated formulas. For random formulas, our bounds significantly extend the range of formula sizes for which non-trivial lower bounds are known. For example, we show that with probability approaching 1, any resolution refutation of a randomly chosen 3-CNF formula with at most n/sup 6/5-/spl epsiv// clauses requires exponential size. Previous bounds applied only when the number of clauses was at most linear in the number of variables. For the pigeonhole principle our bound is a small improvement over previous bounds. Our proofs are more elementary than previous arguments, and establish a connection between resolution proof size and maximum clause size.

In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in the question of whether or not model checking techniques can be applied to large software specifications.To investigate this, we translated a portion of the finite-state requirements specification of TCAS II (Traffic Alert and Collision Avoidance System) into a form accepted by a model checker (SMV). We successfully used the model checker to investigate a number of dynamic properties of the system.We report on our experiences, describing our approach to translating the specification to the SMV language and our methods for achieving acceptable performance in model checking, and giving a summary of the properties that we were able to check. We consider the paper as a data point that provides reason for optimism about the potential for successful application of model checking to software systems. In addition, our experiences provide a basis for characterizing features that would be especially suitable for model checkers built specifically for analyzing software systems.The intent of this paper is to evaluate symbolic model checking of state-machine based specifications, not to evaluate the TCAS II specification. We used a preliminary version of the specification, the version 6.00, dated March, 1993, in our study. We did not have access to later versions, so we do not know if the properties identified here are present in later versions.

We consider the problem of determining, given a graph G and specified nodes s and t, whether or not there is a path of at most k edges in G from s to t. We show that solving this problem on polynomial-size unbounded fan-in circuits, requires depth /spl Omega/(loglogk), improving on a depth lower bound of n(log*k) when k=log/sup O(1/) n. In addition we show that there is a constant c such that for k/spl les/logn, any depth d unbounded fan-in circuit for this problem requires size at least n/sup ck/spl epsiv/d/ where /spl epsiv//sub d/=/spl phi//sup -2d//3 and /spl phi/ is the golden mean. This latter result improves on an n/sup /spl Omega/(log(d+3/k)) bound where log/sup (i/) is the i-fold composition of log with itself. The key to our technique is a new form of switching lemma which combines some of the features of iteratively shortening terms due to Furst, Saxe, and Sipser (1981) and Ajtai (1983) with the kinds of switching lemma arguments introduced by Yao (1985), Hastad (1986), and Cai (1986) that have been the methods of choice for subsequent results.

Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems.Many interesting search problems not known to be solvable in polynomial time are contained in these classes, and a number of them are complete problems.We consider the question of the relative complexity of these search problem classes.We prove several separations which show that in a generic relativized world, the search classes are distinct and there is a standard search problem in each of them that is not computationally equivalent to any decision problem.(Naturally, absolute separations would imply that P 6 = NP.)Our separation proofs have interesting combinatorial content and go to the heart of the combinatorial principles on which the classes are based.We derive one result via new lower bounds on the degrees of polynomials asserted to exist by Hilbert's Nullstellensatz over nite elds.

The weak form of the Hilbert's Nullstellensatz says that a system of algebraic equations over a field, Q/sub i/(x~)=0, does not have a solution in the algebraic closure iff 1 is in the ideal generated by the polynomials Q/sub i/(x~). We shall prove a lower bound on the degrees of polynomials P/sub i/(x~) such that /spl Sigma//sub i/ P/sub i/(x~)Q/sub i/(x~)=1. This result has the following application. The modular counting principle states that no finite set whose cardinality is not divisible by q can be partitioned into q-element classes. For each fixed cardinality N, this principle can be expressed as a propositional formula Count/sub q//sup N/. Ajtai (1988) proved recently that, whenever p, q are two different primes, the propositional formulas Count/sub q//sup qn+1/ do not have polynomial size, constant-depth Frege proofs from instances of Count/sub p//sup m/, m/spl ne/0 (mod p). We give a new proof of this theorem based on the lower bound for the Hilbert's Nullstellensatz. Furthermore our technique enables us to extend the independence results for counting principles to composite numbers p and q. This results in an exact characterization of when Count/sub q/ can be proven efficiently from Count/sub p/, for all p and q.>

This paper introduces communicating branching programs and develops a general technique for demonstrating communication-space tradeoffs for pairs of communicating branching programs. This technique is then used to prove communication-space tradeoffs for any pair of communicating branching programs that hashes according to a universal family of hash functions. Other tradeoffs follow from this result. As an example, any pair of communicating Boolean branching programs that computes matrix-vector products over ${\text{GF}}(2)$ requires communication-space product $\Omega (n^2 )$, provided the space used is $o({n / {\log n}})$. These are the first examples of communication-space tradeoffs on a completely general model of communicating processes.

The combinatorial matching principle states that there is no perfect matching on an odd number of vertices. This principle generalizes the pigeonhole principle, which states that for a fixed bipartition of the vertices, there is no perfect matching between them. Therefore, it follows from recent lower bounds for the pigeonhole principle that the matching principle requires exponential-size bounded-depth Frege proofs. M. Ajtai (1990) previously showed that the matching principle does not have polynomial-size bounded-depth Frege proofs even with the pigeonhole principle as an axiom schema. His proof utilizes nonstandard model theory and is nonconstructive. We improve Ajtai's lower bound from barely superpolynomial to exponential, and eliminate the nonstandard model theory. Our lower bound is also related to the inherent complexity of particular search classes. In particular, oracle separations between the complexity classes PPA and PPAD and between PPA and PPP follow from our techniques.>

In this paper we prove an exponential lower bound on the size of bounded-depth Frege proofs for the pigeonhole principle (PHP).We also obtain an ~(log log rz)depth lower bound for any polynomial-sized Frege proof of the pigeonhole principle.Our theorem nearly completes the search for the exact complexity of the PHP, as Sam Buss has constructed polynomial-size, log ndepth Frege proofs for the PHP.The main lemma in our proof can be viewed as a general H&.stad-style Switching Lemma for restrictions that are partial matchings.Our lower bounds for the pigeonhole principle improve on previous superpolynomial lower bounds.

Our main result is the demonstration of a Boolean function f with nondeterministic and co-nondeterministic complexities O(log n) and ε-error randomized complexity Ω(log2 n), for 0 ≤ ε < 1/2. This is the first separation of this kind for a decision problem.

An optimal $\Omega (n^2 )$ lower bound is shown for the time-space product of any R branching program that determines those values which occur exactly once in a list of n integers in the range $[1,R]$ where $R \geqq n$. This $\Omega (n^2 )$ tradeoff also applies to the sorting problem and thus improves the previous time-space tradeoffs for sorting. Because the R-way branching program is such a powerful model, these time-space product tradeoffs also apply to all models of sequential computation that have a fair measure of space such as off-line multitape Turing machines and off-line log-cost random access machines (RAMs).

Time-space tradeoffs for traversing undirected graphs are proved. One of these tradeoffs is a quadratic lower bound on a deterministic model that closely matches the probabilistic upper bound of A.Z. Broder et al. (1989). The models used are variants of S.A. Cook and C.W. Rackoff's (1980) jumping automata for graphs. Some open problems are stated.>

Communicating branching programs are introduced, and a general technique for demonstrating communication-space tradeoffs for pairs of communicating branching programs is developed. The technique is used to prove communication-space tradeoffs for any pair of communicating branching programs that hashes according to a universal family of hash functions. Other tradeoffs follow from this result. For example any pair of communicating Boolean branching programs that computes matrix-vector products over GF(2) requires communication-space product Omega (n/sup 2/). These are the first examples of communication-space tradeoffs on a completely general model of communicating processes.>

We give the first efficient parallel algorithms for solving the arrangement problem. We give a deterministic algorithm for the CREW PRAM which runs in nearly optimal bounds of O(log n log * n) time and n²/log n processors. We generalize this to obtain an O(logn log* n) time algorithm using n^d/logn processors for solving the problem in d dimensions. We also give a randomized algorithm for the EREW PRAM that constructs an arrange-ment of n lines on-line, in which each insertion is done in optimal O(logn) time using n / log n processors. Our algorithms develop new parallel data structures and new methods for traversing an arrangement.

We introduce a task scheduling model which is useful in the design and analysis of algorithms for small parallel machines.We prove that under our model, the overhead experienced in scheduling an n x n grid graph is O(loglogn) for p processors, p > 2. We also prove a matching lower bound of Q(loglog n) for p processors, p 1 2. We give an extension of the model to cover the case where the processors can have varying speed or are subject to delay.

An optimal Ω(n2) lower bound is shown for the time-space product of any R-way branching program that determines those values which occur exactly once in a list of n integers in the range [1, R] where R ≥ n. This Ω(n2) tradeoff also applies to the sorting problem and thus improves the previous time-space tradeoffs for sorting. Because the R-way branching program is a such a powerful model these time-space product tradeoffs also apply to all models of sequential computation that have a fair measure of space such as off-line multi-tape Turing machines and off-line log-cost RAMs.

Optimal Ω(log n /log log n ) lower bounds on the time for CRCW PRAMS with polynomially bounded numbers of processors or memory cells to compute parity and a number of related problems are proven. A strict time hierarchy of explicit Boolean functions of n bits on such machines that holds up to Ο(log n /log log n ) time is also exhibited. That is, for every time bound T within this range a function is exhibited that can be easily computed using polynomial resources in time T but requires more than polynomial resources to be computed in time T - 1. Finally, it is shown that almost all Boolean functions of n bits require log n - log log n + Ω(1) time when the number of processors is at most polynomial in n . The bounds do not place restrictions on the uniformity of the algorithms nor on the instruction sets of the machines.

We prove optimal Ω(log n/log log n) lower bounds on the time for CRCW PRAM's with polynomially bounded numbers of processors or memory cells to compute parity and a number of related problems. We also exhibit a strict time hierarchy of explicit Boolean functions of n bits on such machines which holds up to Ο(log n/log log n) time. Furthermore, we show that almost all Boolean functions of n bits require log n - log log n + Ω(1) time when the number of processors is at most polynomial in n. Our bounds do not place restrictions on the uniformity of the algorithms nor on the instruction sets of the machines.

We prove lower bounds for the computation of simple functions on generalized versions of parallel random access machines which allow both concurrent reads and concurrent writes.In particular we show that if the number of processors is limited by a polynomial in n then computing the sum of n n-bit integers requires time f2(log n ) and computing the parity of n input bits requires time fl(x/~n ).The latter result, using reductions given by Chandra, Stockmeyer, and Vishkin (1984), implies that a host of problems including sorting or adding n input bits, or multiplying two n/2-bit integers also require time fl(x/~ n ) to compute.

We present optimal depth Boolean circuits (depth $O(\log n)$) for integer division, powering, and multiple products. We also show that these three problems are of equivalent uniform depth and space complexity. In addition, we describe an algorithm for testing divisibility that is optimal for both depth and space.

We present optimal depth Boolean circuits (depth O(log n)) for integer division, powering, and multiple products. We also show that these three problems are of equivalent uniform depth and space complexity. In addition, we describe an algorithm for testing divisibility that is optimal for both depth and space.