We study the relationship between size and depth for Boolean circuits. Over four decades, very few results were obtained for either special or general Boolean circuits. Spira showed in 1971 that any Boolean formula of size s can be simulated in depth O(log s). Spira's result means that an arbitrary Boolean expression can be replaced by an equivalent "balanced" expression, that can be evaluated very efficiently in parallel. For general Boolean circuits, the strongest known result is that Boolean circuits of size s can be simulated in depth O(s / log s). We obtain significant improvements over the general bounds for the size versus depth problem for special classes of Boolean circuits. We show that every layered Boolean circuit of size s can be simulated by a layered Boolean circuit of depth O(sqrt{s log s}). For planar circuits and synchronous circuits of size s, we obtain simulations of depth O(sqrt{s}). Improving any of the above results by polylog factors would immediately improve the bounds for general circuits. We generalize Spira's theorem and show that any Boolean circuit of size s with segregators of size f(s) can be simulated in depth O(f(s)log s). This improves and generalizes a simulation of polynomial-size Boolean circuits of constant treewidth k in depth O(k² log n) by Jansen and Sarma. Since the existence of small balanced separators in a directed acyclic graph implies that the graph also has small segregators, our results also apply to circuits with small separators. Our results imply that the class of languages computed by non-uniform families of polynomial size circuits that have constant size segregators equals non-uniform NC¹. As an application of our simulation of circuits in small depth, we show that the Boolean Circuit Value problem for circuits with constant size segregators (or separators) is in deterministic SPACE (log² n). Our results also imply that the Planar Circuit Value problem, which is known to be P-Complete, is in SPACE (sqrt{n} log n). We also show that the Layered Circuit Value and Synchronous Circuit Value problems, which are both P-complete, are in SPACE(sqrt{n}). Our study of circuits with small separators and segregators led us to obtain space efficient algorithms for computing balanced graph separators. We extend this approach to obtain space efficient approximation algorithms for the search and optimization versions of the SUBSET SUM problem, which is one of the most studied NP-complete problems. Finally we study the relationship between simultaneous time and space bounds on Turing machines and Boolean circuit depth. We observe a new connection between planar circuit size and simultaneous time and space products of input-oblivious Turing machines. We use this to prove quadratic lower bounds on the product of time and space for several explicit functions for input-oblivious Turing machines. / text

ropositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. In this thesis we are concerned with the size and space of proofs, and in particular with the latter. Different approaches to reasoning are captured by corresponding proof systems. The simplest and most well studied proof system is resolution, and we try to get our understanding of other proof systems closer to that of resolution. In resolution we can prove a space lower bound just by showing that any proof must have a large clause. We prove a similar relation between resolution width and polynomial calculus space that lets us derive space lower bounds, and we use it to separate degree and space. For cutting planes we show length-space trade-offs. This is, there are formulas that have a proof in small space and a proof in small length, but there is no proof that can optimize both measures at the same time. We introduce a new measure of space, cumulative space, that accounts for the space used throughout a proof rather than only its maximum. This is exploratory work, but we can also prove new results for the usual space measure. We define a new proof system that aims to capture the power of current SAT solvers, and we show a landscape of length-space trade-offs comparable to those in resolution. To prove these results we build and use tools from other areas of computational complexity. One area is pebble games, very simple computational models that are useful for modelling space. In addition to results with applications to proof complexity, we show that pebble game cost is PSPACE-hard to approximate. Another area is communication complexity, the study of the amount of communication that is needed to solve a problem when its description is shared by multiple parties. We prove a simulation theorem that relates the query complexity of a function with the communication complexity of a composed function. / <p>QC 20170509</p>

Dans ce mémoire de thèse, nous développons d'abord des multiplications matricielles efficaces. Nous créons de nouveaux ordonnancements qui permettent de réduire la taille de la mémoire supplémentaire nécessaire lors d'une multiplication du type Winograd tout en gardant une bonne complexité, grâce au développement d'outils externes ad hoc (jeu de galets), à des calculs fins de complexité et à de nouveaux algorithmes hybrides. Nous utilisons ensuite des technologies parallèles (multicœurs et GPU) pour accélérer efficacement la multiplication entre matrice creuse et vecteur dense (SpMV), essentielles aux algorithmes dits /boîte noire/, et créons de nouveaux formats hybrides adéquats. Enfin, nous établissons des méthodes de /design/ générique orientées vers l'efficacité, notamment par conception par briques de base, et via des auto-optimisations. Nous proposons aussi des méthodes pour améliorer et standardiser la qualité du code de manière à pérenniser et rendre plus robuste le code produit. Cela permet de pérenniser de rendre plus robuste le code produit. Ces méthodes sont appliquées en particulier à la bibliothèque de calcul exact LinBox. / We first expose in this memoir efficient matrix multiplication techniques. We set up new schedules that allow us to minimize the extra memory requirements during a Winograd-style matrix multiplication, while keeping the complexity competitive. In order to get them, we develop external tools (pebble game), tight complexity computations and new hybrid algorithms. Then we use parallel technologies (multicore CPU and GPU) in order to accelerate efficiently the sparse matrix--dense vector multiplication (SpMV), crucial to /blackbox/ algorithms and we set up new hybrid formats to store them. Finally, we establish generic design methods focusing on efficiency, especially via building block conceptions or self-optimization. We also propose tools for improving and standardizing code quality in order to make it more sustainable and more robust. This is in particular applied to the LinBox computer algebra library.