Arrow Research search

Author name cluster

Stephen A. Cook

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

31 papers
1 author row

Possible papers

31

FOCS Conference 2016 Conference Paper

Exponential Lower Bounds for Monotone Span Programs

  • Robert Robere
  • Toniann Pitassi
  • Benjamin Rossman
  • Stephen A. Cook

Monotone span programs are a linear-algebraic model of computation which were introduced by Karchmer and Wigderson in 1993 [1]. They are known to be equivalent to linear secret sharing schemes, and have various applications in complexity theory and cryptography. Lower bounds for monotone span programs have been difficult to obtain because they use non-monotone operations to compute monotone functions, in fact, the best known lower bounds are quasipolynomial for a function in (nonmonotone) P [2]. A fundamental open problem is to prove exponential lower bounds on monotone span program size for any explicit function. We resolve this open problem by giving exponential lower bounds on monotone span program size for a function in monotone P. This also implies the first exponential lower bounds for linear secret sharing schemes. Our result is obtained by proving exponential lower bounds using Razborov's rank method [3], a measure that is strong enough to prove lower bounds for many monotone models. As corollaries we obtain new proofs of exponential lower bounds for monotone formula size, monotone switching network size, and the first lower bounds for monotone comparator circuit size for a function in monotone P. We also obtain new polynomial degree lower bounds for Nullstellensatz refutations using an interpolation theorem of Pudlak and Sgall [4]. Finally, we obtain quasipolynomial lower bounds on the rank measure for the st-connectivity function, implying tight bounds for st-connectivity in all of the computational models mentioned above.

Details

FOCS Conference 2013 Conference Paper

Average Case Lower Bounds for Monotone Switching Networks

  • Yuval Filmus
  • Toniann Pitassi
  • Robert Robere
  • Stephen A. Cook

An approximate computation of a Boolean function by a circuit or switching network is a computation in which the function is computed correctly on the majority of the inputs (rather than on all inputs). Besides being interesting in their own right, lower bounds for approximate computation have proved useful in many sub areas of complexity theory, such as cryptography and derandomization. Lower bounds for approximate computation are also known as correlation bounds or average case hardness. In this paper, we obtain the first average case monotone depth lower bounds for a function in monotone P. We tolerate errors that are asymptotically the best possible for monotone circuits. Specifically, we prove average case exponential lower bounds on the size of monotone switching networks for the GEN function. As a corollary, we separate the monotone NC hierarchy in the case of errors -- a result which was previously only known for exact computations. Our proof extends and simplifies the Fourier analytic technique due to Potechin, and further developed by Chan and Potechin. As a corollary of our main lower bound, we prove that the communication complexity approach for monotone depth lower bounds does not naturally generalize to the average case setting.

Details

CSL Conference 2013 Conference Paper

Theories for Subexponential-size Bounded-depth Frege Proofs

  • Kaveh Ghasemloo
  • Stephen A. Cook

This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1), O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1), 2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs. We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs. Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon)) for all epsilon > 0.

Details

CSL Conference 2011 Conference Paper

A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem

  • Dai Tri Man Le
  • Stephen A. Cook
  • Yuli Ye

Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.

Details

CSL Conference 2010 Conference Paper

Formal Theories for Linear Algebra

  • Stephen A. Cook
  • Lila Fontes

Abstract We introduce two-sorted theories in the style of [CN10] for the complexity classes ⊕ L and DET, whose complete problems include determinants over ℤ 2 and ℤ, respectively. We then describe interpretations of Soltys’ linear algebra theory LA P over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over ℤ 2 and ℤ can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.

Details

MFCS Conference 2009 Conference Paper

Branching Programs for Tree Evaluation

  • Mark Braverman
  • Stephen A. Cook
  • Pierre McKenzie
  • Rahul Santhanam
  • Dustin Wehr

Abstract The problem \(FT^{h}_{d}(k)\) consists in computing the value in [ k ] = {1, .. ., k } taken by the root of a balanced d -ary tree of height h whose internal nodes are labelled with d -ary functions on [ k ] and whose leaves are labelled with elements of [ k ]. We propose \({FT^{h}_{d}(k)}\) as a good candidate for witnessing \({\mathbf{L}} \subsetneq{\mathbf{LogDCFL}}\). We observe that the latter would follow from a proof that k -way branching programs solving \({FT^{h}_{d}(k)}\) require \(\Omega(k^{\mbox{\scriptsize unbounded function}(h)})\) size. We introduce a “state sequence” method that can match the size lower bounds on \(FT^{h}_{d}(k)\) obtained by the Nec̆iporuk method and can yield slightly better (yet still subquadratic) bounds for some nonboolean functions. Both methods yield the tight bounds Θ( k 3 ) and Θ( k 5/2 ) for deterministic and nondeterministic branching programs solving \(FT^{3}_{2}(k)\) respectively. We propose as a challenge to break the quadratic barrier inherent in the Nec̆iporuk method by adapting the state sequence method to handle \(FT^{4}_{d}(k)\).

Details

CSL Conference 2007 Conference Paper

Relativizing Small Complexity Classes and Their Theories

  • Klaus Aehlig
  • Stephen A. Cook
  • Phuong Nguyen 0001

Abstract Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L and NL we define their relativizations using Wilson’s stack oracle model, but limit the height of the stack to a constant (instead of log( n )). We show that the collapse of any two classes in { AC 0 ( m ), TC 0, NC 1, L, NL } implies the collapse of their relativizations. Next we develop theories that characterize the relativizations of subclasses of P by modifying theories previously defined by the second two authors. A function is provably total in a theory iff it is in the corresponding relativized class. Finally we exhibit an oracle α that makes AC k ( α ) a proper hierarchy. This strengthens and clarifies the separations of the relativized theories in [Takeuti, 1995]. The idea is that a circuit whose nested depth of oracle gates is bounded by k cannot compute correctly the ( k + 1) compositions of every oracle function.

Details

FOCS Conference 1991 Conference Paper

A New Characterization of Mehlhorn's Polynomial Time Functionals (Extended Abstract)

  • Bruce M. Kapron
  • Stephen A. Cook

A. Cobham (1964) presented a machine-independent characterization of computational feasibility, via inductive definition. R. Constable (1973) was apparently the first to consider the notion of feasibility for type 2 functionals. K. Mehlhorn's (1976) study of feasible reducibilities proceeds from Constable's work. Here, a class of polytime operators is defined, using a generalization of Cobham's definition. The authors provide an affirmative answer to the question of whether there is a natural machine based definition of Mehlhorn's class. >

Details

FOCS Conference 1989 Conference Paper

Characterizations of the Basic Feasible Functionals of Finite Type (Extended Abstract)

  • Stephen A. Cook
  • Bruce M. Kapron

The authors define a simple typed while-programming language that generalizes the sort of simple language used in computability texts to define the familiar numerical computable functions and corresponds roughly to the mu -recursion of R. O. Gandy (1967). This language does not fully capture the notion of higher type computability. The authors define run times for their programs and prove that the feasible functionals of S. Cook and A. Urquhart (1988) are precisely those functionals computable by typed while-programs with run times feasibly length-bounded. The authors introduce the notion of a bounded typed loop program and prove that a finite type functional is feasible if it is computable by a bounded typed loop program. >

Details

FOCS Conference 1984 Conference Paper

Log Depth Circuits for Division and Related Problems

  • Paul Beame
  • Stephen A. Cook
  • H. James Hoover

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.

Details