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 $N^{\log_2 N}$ (and like all formulas have Resolution refutations of space $N$) for ... more >>>

We prove a time-space tradeoff lower bound of $T =
\Omega\left(n\log(\frac{n}{S}) \log \log(\frac{n}{S})\right) $ 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.

In ... more >>>

We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most $k$ (known as ${\rm Th}(k)$ proofs). Such systems include: Lovasz-Schrijver ... more >>>

We prove an n^{Omega(1)}/2^{O(k)} lower bound on the randomized k-party communication complexity of read-once depth 4 AC^0 functions in the number-on-forehead (NOF) model for O(log n) players. These are the first non-trivial lower bounds for general NOF multiparty communication complexity for any AC^0 function for omega(log log n) players. For ... more >>>

We prove n^Omega(1) lower bounds on the multiparty communication complexity of AC^0 functions in the number-on-forehead (NOF) model for up to Theta(log n) players. These are the first lower bounds for any AC^0 function for omega(loglog n) players. In particular we show that there are families of depth 3 read-once ... more >>>

Recently, an extension of the standard data stream model has been introduced in which an algorithm can create and manipulate multiple read/write streams in addition to its input data stream. Like the data stream model, the most important parameter for this model is the amount of internal memory used by ... more >>>

We consider extensions of the DPLL approach to satisfiability testing that add a version of memoization, in which formulas that the algorithm has previously shown to be unsatisfiable are remembered for later use. Such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability. We formalize these methods by ... more >>>

We prove that an \omega(log^3 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 tree-like Lovasz-Schrijver systems that refute unsatisfiable CNFs. More generally, we prove that an n^\Omega(1) lower bound for the (k+1)-party NOF communication complexity of set-disjointness ... more >>>

We consider the resolution proof complexity of propositional formulas which encode random instances of graph $k$-colorability. We obtain a tradeoff between the graph density and the resolution proof complexity.
For random graphs with linearly many edges we obtain linear-exponential lower bounds on the length of resolution refutations. For any $\epsilon>0$, ... more >>>

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 ... more >>>

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 Ajtai in his ... more >>>

Proof complexity, the study of the lengths of proofs in
propositional logic, is an area of study that is fundamentally connected
both to major open questions of computational complexity theory and
to practical properties of automated theorem provers. In the last
decade, there have been a number of significant advances ... more >>>

We obtain the first non-trivial time-space tradeoff lower bound for
functions f:{0,1}^n ->{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 cn, for some constant c>1. We also give the first
separation result between the ... more >>>

We obtain improved lower bounds for a class of static and dynamic
data structure problems that includes several problems of searching
sorted lists as special cases.

These lower bounds nearly match the upper bounds given by recent
striking improvements in searching algorithms given by Fredman and
Willard's fusion ... more >>>