Workshop on Theoretical Computer Science
Workshop consists of several survey talks by well-known experts in Theoretical Computer Science. The talks will be aimed at a wide audience in all areas of Computer Science and all those who are interested in Theoretical Computer Science and have basic knowledge in this field.
The workshop is organized by the HSE Laboratory of Theoretical Computer Science.
The workshop language is English.
The talks will be given by HSE professors as well as invited speakers.
Workshop program
Alexander Shen (Montpellier University)
Often some existence result can be proven by showing that objects that do not have the required property, can be compressed (and not all objects can!). We will try to illustrate this type of arguments with several examples -- both classical ones (e.g., a toy proof of the existence of infinitely many primes, law of large numbers) and more recent ones (some versions of Lovasz local lemma or related results).
Sergei O. Kuznetsov (Higher School of Economics)
A natural problem setting in machine learning is shown to be equivalent to the problem of dualizing a monotone boolean function. The most classical form of dualization setting is converting a DNF to CNF. The complexity of a solution depends on particular machine learning setting, which defines the type of the structure where dualization takes place. Several intractability and tractability results are discussed.
Sam Buss (University of California, San Diego)
The class TFNP of total NP search problems consists of multivalued functions (total relations) with polynomial time recognizable graphs. In the complexity theoretic setting, the totality (existence) is usually established via a combinatorial principle, but it can also be established in a fragment of bounded arithmetic. This talk will give an introduction to these classes, from both points of view (complexity theoretic and bounded arithmetic). We will also discuss two recent results about the Tucker problem and about the Frege Proof Consistency search problem.
Nikolay Vereshchagin (Higher School of Economics)
Let f_p be an optimal Goedel numbering of the family of computable functions (in Schnorr's sense), where p ranges over binary strings. Assume that a list of strings L(p) is computable from p and for all p contains a f-program for f_p whose length is at most eps bits larger that the length of shortest f-programs for f_p. We show that for infinitely many p the list L(p) must have exponential in (|p|-eps) strings. Here eps is an arbitrary function of p.
Irina A. Lomazova (Higher School of Economics)
The modern computational paradigm shifts from traditional centralized computing on workstations, servers, or groups of servers, to distributed, decentralized, loosely coupled computing (cloud, ubiquitous, etc.). Correctness and safeness of distributed systems is a matter of utmost importance, and formal methods are used for modeling and analysis of such systems.
In this talk we review some automata-based models of concurrent systems and discuss the balance between expressibility of modeling languages and decidability of behavioral properties.
Sergey Yekhanin (Microsoft Research)
Historically, most large distributed storage systems (e.g., Hotmail) have been using replication to provide reliability against machine failures. Today however as the amount of stored data reaches multiple Zetabytes keeping few copies of data around is prohibitively expensive. Therefore more and more systems are adopting erasure coding in place of replication. Coding for distributed storage has some unique challenges and trade-offs. In this talk we review the state of the art in erasure codes for distributed storage.
Jakob Nordström (KTH Royal Institute of Technology)
Although determining satisfiability of Boolean formulas is an NP-complete problem, and is hence believed to require exponential time in the worst case, algorithmic developments over the last 15-20 years have led to so-called SAT solvers that successfully handle real-world formulas with millions of variables. It is still quite poorly understood when and how such solvers work, however.
Proof complexity studies formal methods for reasoning about Boolean formulas, and provides one of the few tools available for theoretical analysis of SAT solver performance. This talk is intended as an informal and accessible survey of proof complexity for non-experts, focusing on some comparatively weak proof systems of particular interest in the context of SAT solving. We will review resolution, polynomial calculus, and cutting planes (related to conflict-driven clause learning, Gröbner basis computations, and pseudo-Boolean solvers, respectively) and some proof complexity measures that have been studied for these proof systems. This will then allow us to discuss if and how these complexity measures could provide insights into the potential and limitations of current state-of-the-art SAT solvers, and how concerns related to applied SAT solving can give rise to interesting complexity-theoretic questions. Along the way, we highlight a number of current research challenges.
Ilan Newman (University of Haifa)
For a graph on n vertices, and an integer D, let the D-local view of G=(V,E) be the collection (multiset) of the unlabelled n balls of distance D around the vertices.
The main question that motivates this study is: what can be said about G knowing only its D-local view for some constant D.
For constant bounded degree planar (or more generally hyperfinite) graphs, Newman-Sohler [2011] following a long sequence of work, show that for any ε>0, there is a D such that the D-local view of the graph determines the graph up to the deletion / insertion of at most εn edges. This in turn, implies that every property of planar (hyperfinite) graphs can be tested (in the sense of property testing, by constantly many queries.
What happens in non-bounded degree planar graphs? The answer is currently still open. However, we show, following Yoshida's results on Forests, that the above phenomenon still holds for outerplanar graphs. The implication to testing is deteriorated, though. Testing now requires O(poly(log n)) queries.
I will describe the ideas behind the two results, the later which is a joint work with Jasine Babu and Areej Khoury.
Amir Shpilka (Tel Aviv University)
Algebraic complexity studies the complexity of computing polynomials by arithmetic circuits - i.e. circuits that use the arithmetic operations +,*. Arithmetic circuits form a very elegant model of computation in which the (analog of the) P vs. NP problem may be easier to attack. In recent years algebraic complexity has gained a lot of interest and some breakthrough results were obtained. In this talk we will mention those breakthrough results and discuss some of the recent developments. In particular we will mention results regarding depth reduction, lower bounds and algorithms for polynomial identity testing.
Madhu Sudan (Harvard University)
Property Testing studies the design and analysis of algorithms that Test if some (massive) data satisfies some global Property without looking at all the data, or inferring the parameters that explain how the data satifies the property. It was initiated by accidental discoveries, by Blum, Luby and Rubinfeld, and by Babai, Fortnow and Lund, showing that some complex properties could be tested remarkably efficiently. In the nearly quarter century since these discoveries, the scope of Property Testing has expanded broadly - it covers properties of algebraic, graph-theoretic, statistical, and functional nature; and the resulting techniques have connected the field to combinatorics, additive number theory, harmonic analysis, algebraic geometry, while having applications in complexity theory, combinatorial optimization and even extremal graph theory.
In this talk I will look back at some of this history attempting to describe some of the diversity of the results and impact; and try to present a personal perspective, via "Invariance", that explains some of the reason for the diversity, and tries to extract some coherent picture among this diversity.