swe flag På svenska
School of
Computer Science
and Communication
KTH / CSC / Theory Group / Jakob Nordström / Complexity meetings

Complexity meetings

The complexity meetings are a(n even) less formal analogue of the Theory reading group. The main differences are:

  • Complexity meetings are not announced publicly (i.e., in the CSC and Department of Mathematics calendars). However, we have a mailing list which you are free to join — just send an e-mail to jakobn at kth dot se.
  • In the complexity meetings, we typically start earlier in the day and go on for longer, say from 10:15 to 14:00 or so.
  • The presentations are more technical, and are most often related to topics where we are conducting research ourselves or want to start doing so.
  • There is no listener-friendly one-hour general seminar — instead we start with the technical presentation right away. Also, we mostly assume that listeners are generally familiar with the relevant terminology in the area, although it is perfectly OK to ask for quick recapitulations of any forgotten definitions.
  • Notification of attendance in advance is mandatory for those who want lunch. Spontaneous visitors are still very welcome, but there will be no extra food.

Complexity meetings spring 2017

  • Thursday Jun 1 at 12:00 (note the time!) in 1537, Lindstedtsvägen 3
    Lower bounds for cutting planes refutations of random CNFs
    (Robert Robere, University of Toronto)

    The cutting planes proof system is a well-known and fairly strong propositional proof system which manipulates integer linear inequalities. Despite many years of work, the only lower bound technique capable of proving superpolynomial length lower bounds on cutting planes refutations is feasible interpolation, introduced by Pudlák. Feasible interpolation only applies to tautologies of a certain restricted form, meaning that for many standard tautologies we do not have strong length lower bounds for cutting planes.

    In this work we introduce a new technique for proving lower bounds on cutting planes refutations. To be precise, our new technique shows an equivalence between

    1. proofs of any tautology F in the proof system RCC (which is stronger than cutting planes), and
    2. real monotone circuits computing a monotone boolean function related to F.

    Furthermore, we are able to apply this technique to prove lower bounds on the size of cutting planes refutations of random CNF formulas.

    This talk is based on joint work with Noah Fleming, Denis Pankratov and Toniann Pitassi. The results in this work have been discovered independently by Pavel Hrubeš and Pavel Pudlák.

  • Tuesday May 16 at 10:15 in 4523
    An interactive journey through combinatorial optimization: resilient solutions, multiple objectives, and logic-based approaches for timetabling
    (Emir Demirović, Technische Universität Wien)

    In this presentation, a range of combinatorial optimization topics will be covered, where the audience will dictate the flow according to their interest. Therefore, it is meant to be an interactive presentation. The topics are as follows:

    1. Solving the general high school timetabling (XHSTT) problem using logic-based approaches: maxSAT, SMT-bitvector theory, and a hybrid algorithm which combines maxSAT with large neighborhood search (metaheuristic algorithm). These approaches are state-of-the-art for XHSTT, outperforming the competition on numerous benchmarks.
    2. Computing the "representative" subset of all Pareto optimal solutions for multi-objective optimization problems is known to be ΣP2-hard. We will see a shift in complexity to NP-hardness when considering an approximation using the notion of egalitarian solutions, and discuss algorithms for its computation.
    3. For practical applications, it is important to compute solutions that remain "stable" after unexpected changes to the problem happen (e.g. new constraints are added post-solving). We will formally define the problem for set covering and set partitioning, prove ΣP3- and ΣP2-hardness (respectively), and analyze algorithms for computing such "resilient" solutions.

  • Wednesday May 3 at 10:15 in 4423
    Low-degree spectral algorithms are at least as strong as the sum-of-squares hierarchy for planted problems
    (Sam Hopkins, Cornell University)

    We study planted problemsfinding hidden structures in random noisy inputsthrough the lens of the sum-of-squares semidefinite programming hierarchy (SoS). This family of powerful semidefinite programs has recently yielded many new algorithms for planted problems, often achieving the best known polynomial-time guarantees in terms of accuracy of recovered solutions and robustness to noise. One theme in recent work is the design of spectral algorithms which match the guarantees of SoS algorithms for planted problems. Classical spectral algorithms are often unable to accomplish this: the twist in these new spectral algorithms is the use of spectral structure of matrices whose entries are low-degree polynomials of the input variables.

    We prove that for a wide class of planted problems, including refuting random constraint satisfaction problems, tensor and sparse PCA, densest-k-subgraph, community detection in stochastic block models, planted clique, and others, eigenvalues of degree-d matrix polynomials are as powerful as SoS semidefinite programs of size roughly n d . For such problems it is therefore always possible to match the guarantees of SoS without solving a large semidefinite program.

    The proof uses ideas from Fourier analysis and showcases a novel use of the powerful random restrictions technique. In this whiteboard talk we will try to cover as many of the main ideas from the proof as possible.

    Joint work with Pravesh Kothari, Aaron Potechin, Prasad Raghavendra, Tselil Schramm, and David Steurer.

  • Tuesday Mar 28 at 10:15 in 4523
    An improved small restriction switching lemma by Razborov
    (Ilario Bonacina, Theory Group, KTH)

    In this seminar we will give an exposition of some parts of Razborov's recent Annals paper "Pseudorandom generators hard for k-DNF resolution and polynomial calculus". In particular, we will focus on the small restriction switching lemma, a key ingredient of that paper. We will not cover the main application of this result, that is the fact that resolution over (log log n)-DNF formulas does not have efficient proofs of NP \nsubseteq P/poly. We will see a less a technically challenging application: the weak pigeonhole principle with 2n pigeons and n holes is hard for Resolution over (c log n / log log n)-DNF formulas.

Complexity meetings autumn 2016

During the autumn of 2016 we have mostly been busy with the course DD2442 Seminars on Theoretical Computer Science: Proof Complexity, which has served as a long series of more or less informal proof complexity seminars.

  • Monday Dec 12 at 10:00 (sharp) in 4523
    Refuting the dense linear order principle in resolution requires large width
    (Susanna F. de Rezende, Theory Group, KTH)

    The paper "A combinatorial characterization of resolution width" by Atserias and Dalmau is mainly known for proving that width is a lower bound on space in resolution. This is, however, only one of the two applications they present in the paper of their combinatorial characterization of width. The other application is to show that any resolution refutation of the dense linear order (DLO) principle has large width. The DLO principle is of special interest since it is an example of a formula that requires large width but has small resolution proofs.

    In this informal meeting we will present Atserias-Dalmau's combinatorial characterization of resolution width and the application to the DLO principle. The significance of this result is not so much the width lower bound itself, but rather the techniques that are involved.

Complexity meetings spring 2016

The complexity meetings webpage was not quite kept up to date during the spring of 2016 for various reasons… In the best of worlds it will be updated later with the talks that were given during the semester.

In addition, a larger than usual part of the TCS group was away in May-July, so the Complexity meetings were on hold during that time.

Complexity meetings autumn 2015

  • Monday Dec 7 at 12:00 in 4523
    Semisimple polynomial calculus lower bounds
    (Mladen Mikša, Theory Group, KTH)

    In 2001, Alekhnovich and Razborov proved the first lower bound in polynomial calculus that works for fields of arbitrary characteristic. Their proof was based on constructing a special linear operator that distinguishes between polynomials derivable in low degree and the goal polynomial 1, thus establishing that we cannot derive the contradiction 1 = 0 in low degree. While a groundbreaking proof, the structure of their linear operator remains hard to understand and applying it to other formulas is still a challenge. However, last year Yuval Filmus made a step towards a better understanding of these bounds by giving an alternative proof of the same result. In this new proof, rather than constructing a linear operator, Filmus directly describes the set of low degree polynomials that belong to the kernel of the operator, which polynomials he calls semisimple. Thus, in this new proof we are able to see exactly which polynomials are derivable in low degree.

    In this talk, I will present a modified version of this alternative proof of degree lower bounds by Yuval Filmus.

  • Thursday Oct 1 at 11:15 in 1635
    Pseudorandom generators in proof complexity
    (Mladen Mikša, Theory Group, KTH)

    How can we efficiently generate a long string of random bits if we are provided with an inefficient source of randomness that takes a long time to generate a random bit? The answer to this question was proposed by Yao in '82 by introducing the concept of a pseudorandom generator, one of the most important concepts in theoretical computer science. The pseudorandom generator is a function that takes a string of n bits and stretches it to a string of m >> n bits such that no bounded computer can distinguish between the probabilistic distribution produced by the generator and a truly random distribution on m bits. Here, the bounded computer is as an arbitrary logical circuit from some class of small circuits C.

    Another view of bounded computation is provided by proof complexity, where we are interested in what can be proved efficiently by a prover whose computational ability is bounded by some circuit class C. With this view in mind we can ask what are good pseudorandom generators with respect to different provers? In this talk we look at two proof systems: resolution and polynomial calculus. For these proof systems we show that proving that a pseudorandom generator is not an onto-function requires exponential proofs for certain types of generators that stretch n to ~n^2 random bits.

    This talk is based on the paper "Pseudorandom generators in propositional proof complexity" by Alekhnovich, Ben-Sasson, Razborov, and Wigderson.

Complexity meetings spring 2015

  • Thursday Jul 9 at 13:15 in 4523
    Hardness of Hypergraph Coloring
    (Sangxia Huang, KTH and EPFL)

    In hypergraph coloring, we are given a hypergraph, and the goal is to find a vertex coloring such that all hyperedges contain at least two colors. The focus of this talk is the computational complexity of finding a hypergraph coloring that minimizes the number of colors used. I will first survey the algorithmic and hardness results of the problem, and then present my recent result showing quasi-NP-hardness of coloring 2-colorable-8-uniform hypergraphs with 2^{(log N)^{1/4-o(1)}} colors. Our result is based on techniques developed recently in [Dinur, Guruswami '13], [Guruswami, Håstad, Harsha, Srinivasan, Varma '14] and [Khot, Saket '14].

  • Monday Jun 8 at 13:15 in 4523
    The multiparty communication complexity of disjointness
    (Marc Vinyals, Theory Group, KTH)

    Set disjointness is a key problem in communication complexity and it is well understood in the thoroughly studied model where two parties communicate. With more parties involved, one can show an upper bound for disjointness where the communication decreases (roughly) exponentially in the number of parties.

    We will go over the proof that this is nearly optimal when the communication protocol is deterministic and discuss how to use the techniques to simplify an existing, weaker lower bound for the randomized case.

    The talk is based on the paper "Simplified Lower Bounds on the Multiparty Communication Complexity of Disjointness" by Rao and Yehudayoff to appear at CCC '15.

  • Tuesday Apr 7 at 10:15 in 4523
    A combinatorial framework for space lower bounds in proof complexity
    (Ilario Bonacina, Sapienza – Università di Roma)

    Recently new space lower bounds in algebraic proof systems and resolution were proven. Those lower bounds rely on the possibility to build families of assignments with certain combinatorial properties. In this talk we present such frameworks, discuss how they are related, and show how they are used to obtain space lower bounds for total space in Resolution and monomial space in Polynomial Calculus with Resolution.

    This talk is based on joint works with Nicola Galesi and Neil Thapen (ITCS '13, FOCS '14).

  • Monday Feb 9 at 12:00 in 4523
    The space complexity of cutting planes refutations
    (Susanna F. de Rezende, Theory Group, KTH)

    I will present the paper "The space complexity of cutting planes refutations" by Nicola Galesi, Pavel Pudlák and Neil Thapen (eccc.hpi-web.de/report/2014/138). This paper studies the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. The space used by a refutation is measured as the number of inequalities that need to be kept on a blackboard while verifying it.

    The authors prove that any unsatisfiable set of inequalities has a cutting planes refutation in space 5. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal lower bounds are known. Motivated by this result they also consider a restriction of cutting planes, in which all coefficients have size bounded by a constant and show, on one hand, that it is stronger than resolution with respect to space, and on the other, that there is a CNF formula which requires super-constant space to refute in this system.

Complexity meetings autumn 2014

  • Monday Nov 24 at 10:30 in 4523
    Lower bounds for parity and the switching lemma
    (Johan Håstad, Theory Group, KTH)

    We study the model of constant depth circuits containing unbounded fanin and-gates and or-gates. It was proved a long time ago (1986) that any circuit of depth d that computes parity of n inputs must be of size exp(Ω(n(1/(d-1))).

    This was proved by the use of the switching lemma. This lemma says that if you have a depth-2 circuit which is an and-of-ors and is of small bottom fanin then, by fixing a suitable fraction of the input variables in a random way, you can, with high probability, convert the circuit to an or-of-ands maintaining small bottom fanin.

    A more recent result (2014) says that best correlation of depth-d, size-S circuit and parity of n inputs is exp(-Ω(n/(log S)(d-1)). This requires an extension of the switching lemma.

    In this seminar we will prove the switching lemma and give the application from 1986. Time permitting we will also discuss the more recent extension.

  • Monday Nov 17 at 11:15 in the "research lounge" outside 4523
    Lower bounds for k-DNF resolution on random 3-CNFs: The sequel
    (Marc Vinyals, Theory Group, KTH)

    Last autumn we studied k-DNF resolution, an extension of resolution that works with k-DNF formulas instead of clauses. This proof sytem is exponentially more powerful than resolution yet weak enough so that one can prove interesting lower bounds.

    We already saw a switching lemma by Segerlind et al. and how to use it to prove lower bounds on refutation length for various formula families. However, for the lower bound for random 3-CNF formulas by Alekhnovich we did not quite manage to cover the technical details in the proofs.

    In this talk we will quickly recap the basics of k-DNF resolution and the switching lemma, and then show the lower bound for random 3-CNFs in full detail.

  • Wednesday Sep 24 at 10:15 in 1625
    Sherali-Adams rank lower bounds for the pigeonhole and least number principles
    (Massimo Lauria, Theory Group, KTH)

    This talk will consider the Sherali-Adams (SA) proof system for integer linear programming and how it can be used to refute propositional formulas. We will show how tight lower bounds on rank can be established for both the pigeonhole principle and least number principle. If time permits, we will show how the existence of a resolution refutation of width w and size s implies a SA refutation of rank w + 1 and comparable size.

    This talk will be based on the paper "Tight Rank Lower Bounds for the Sherali-Adams Proof System" by Stefan Dantchev, Barnaby Martin, and Mark Rhodes (www.sciencedirect.com/science/article/pii/S0304397509000127).

  • Friday Sep 5 at 10:15 in 1625
    Degree lower bounds in polynomial calculus: The sequel
    (Mladen Mikša, Theory Group, KTH)

    We continue our excursion into the mysteries of "Lower bounds for polynomial calculus: non-binomial case" by Alekhnovich and Razborov (people.cs.uchicago.edu/~razborov/files/misha.pdf).

  • Monday Sep 1 at 10:15 in 1537
    Degree lower bounds in polynomial calculus
    (Mladen Mikša, Theory Group, KTH)

    Given a set of polynomials a natural question to ask is whether they share a common zero. Convincing us that they share a zero is easy and can be done by just presenting the appropriate assignment to the variables. On the other hand, if polynomials do not share a common zero we need a proof of this claim in some formal proof system. In this talk we focus on the polynomial calculus proof system.

    Once we have a proof system fixed, we can ask how complicated the proof needs to be. While there are different ways of measuring the complexity of a polynomial calculus proof, one useful measure, which is also related to other measures, is the degree of the largest monomial occurring in the proof.

    In this talk I will show that for polynomials satisfying certain properties any polynomial calculus proof that the polynomials do not share a common zero requires large degree. The presentation is based on the paper "Lower bounds for polynomial calculus: non-binomial case" by Alekhnovich and Razborov (people.cs.uchicago.edu/~razborov/files/misha.pdf).

  • Thursday Aug 21 at 10:15 in 4523
    Rounds in communication complexity
    (Marc Vinyals, Theory Group, KTH)

    Alice and Bob need to compute the solution to a problem jointly but are far apart, so that the communication cost dwarfs all other concerns. The standard communication complexity setting analyzes this problem by proving upper and lower bounds on how many bits Alice and Bob will need to exchange.

    However, if Alice and Bob are far apart messages also take time to arrive, and so a more refined analysis should also take the number of messages exchanged into account. In this presentation, I will talk about communication with bounds on the number of rounds and show that for the so-called pointer jumping problem restricting the number of rounds increases the required amount of communication exponentially. The presentation will mostly follow the paper "Rounds in Communication Complexity Revisited" by Nisan and Wigderson (dx.doi.org/10.1137/0222016).

Complexity meetings spring 2014

  • Friday Mar 21 at 10:15 in 4523
    Strong ETH holds (almost) for resolution: An exposition
    (Ilario Bonacina, Sapienza – Università di Roma,
    Navid Talebanfard, Aarhus University)

    The Strong Exponential Time Hypothesis (SETH) states that k-SAT gets harder and harder as k grows and that the running time of the best k-SAT algorithm approaches that of exhaustive search. In this presentation we give an exposition of a recent result of Beck and Impagliazzo (STOC '13) showing that general resolution is almost consistent with SETH, that is, there are unsatisfiable k-CNFs for which any general resolution refutation has size (3/2)^(1 - \epsilon_k)n, where espilon_k approaches 0 as k goes to infinity.

  • Tuesday Mar 11 at 10:15 in 4523
    Lower bounds for width-restricted clause learning
    (Jan Johannsen, Ludwig-Maximilians-Universität München)

    Clause learning is a technique that is crucial for the success of contemporary SAT solving algorithms. We show lower bounds for clause learning SAT algorithms when the width of learned clauses is restricted. These algorithms require time 2Ω(n/log n) to refute the pigeonhole principle clauses PHPn when learning only clauses of width n/2. They also require time 2Ω(n) to refute the ordering principle clauses Ordn when learning only clauses of width n/4. In general, for unsatisfiable input formulas of small width, lower bounds for width-restricted clause learning follow from resolution lower bounds. All lower bounds obtained are of the same order of magnitude as known lower bounds for DPLL algorithms without clause learning, i.e., for tree-like resolution.

  • Friday Feb 21 at 14:30 in 4523
    The graph pigeonhole principle is hard for polynomial calculus
    (Mladen Mikša, Theory Group, KTH)

    I will talk about the paper Lower Bounds for Polynomial Calculus: Non-Binomial Case by Alekhnovich and Razborov. Using a slight modification of their original proof, I will show a polynomial calculus degree lower bound for the graph pigeonhole principle on 3-regular expanders (with one right vertex removed).

  • Friday Feb 7 at 10:15 in 4523
    Total space in resolution
    (Ilario Bonacina, Sapienza Universitá di Roma)

    I will talk about some ongoing work with Nicola Galesi and Neil Thapen. A resolution refutation of some unsatisfiable CNF F can be presented on a blackboard with limited space. At each step the blackboard contains a set of clauses. Initially it is empty and at each step we can either: (1) write down a clause from F, (2) infer new clauses from the ones already on the blackboard, (3) erase clauses in order to save space. The refutation ends when we reach the empty clause.

    The size of a blackboard is measured as the total number of variables (with repetitions) that we can possibly write on it. The Total Space of a refutation is the minimal size of a blackboard needed to present in this way. We show an Omega(n^2) total space lower bound for random kCNFs where n is the number of variables. This is optimal (up to a constant factor) and the result goes through a quite general theorem that can be used to produce total space lower bounds for other families of formulas.

Complexity meetings autumn 2013

  • Tuesday Dec 10 at 10:15 in 4523
    Monotone lower bounds via Fourier analysis
    (Siu Man Chan, Princeton University)

    We will discuss lower bounds on combinatorial models of computation under monotone restrictions, using the Fourier analysis techniques introduced by Potechin. We prove tight size bounds on monotone switching networks for the NP-complete problem of k-clique, and for an explicit monotone problem by connecting the P-complete problem of generation with reversible pebble games. This gives alternative proofs of the separations of m-NC from m-P and of m-NC^i from m-NC^{i+1} , different from Raz-McKenzie (Combinatorica '99).

  • Wednesday Dec 4 at 10:15 in 1625
    Linear rank Lasserre lower bounds for k-XOR and k-SAT
    (Massimo Lauria, Theory Group, KTH)

    In 2001, Dima Grigoriev showed that a particular kind of unsatisfiable linear equations (mod 2) cannot be refuted even by the most powerful integer programming relaxation techniques studied in theory literature. Later Schoenebeck independently rediscovered this result in 2008 and extended to more general families of k-CSP. We will see that it follows as a corollary that for several CSP problems the approximation given by a linear level Lasserre relaxation is not better than the one given by the trivial random algorithm.

    The talk is based on the following papers:

    • Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity (Grigoriev, 2001).
    • Linear level Lasserre lower bounds for certain k-CSPs (Schoenebeck, 2008).

  • Thursday Nov 21 at 12:00 noon in 1537
    Lower bounds for k-DNF resolution on random 3-CNFs
    (Marc Vinyals, Theory Group, KTH)

    We continue our study of k-DNF resolution, an extension of resolution that works with k-DNF formulas instead of clauses, which is exponentially more powerful than resolution yet weak enough so that one can prove interesting lower bounds.

    Segerlind et al. developed a switching lemma and used it to prove lower bounds on refutation length for various formula families. One of these families were random CNF formulas of bounded width, but the width had to be large enough as a function of k for their techniques to apply. In a follow-up work, Alekhnovich refined their arguments and proved exponential length lower bounds for random CNFs of minimal width 3 (2-CNFs are always easy).

    We will give an exposition of Alekhnovich's result as presented in the paper Lower Bounds for k-DNF Resolution on Random 3-CNFs (dx.doi.org/10.1007/s00037-011-0026-0).

  • Monday Nov 11 at 10:15 in 4523
    Complexity of Positivstellensatz proofs for the knapsack
    (Massimo Lauria, Theory Group, KTH)

    Positivstellensatz Calculus (Grigoriev & Vorobjov 2001; Grigoriev 2001) is a inference system that reasons about polynomial inequalities over the reals. Its importance stems from the fact that many approximation algorithms for combinatorial optimization can be viewed as proofs in this inference system. The runtime of such algorithms is correlated to the degree of the polynomials involved in the corresponding proofs.

    In this talk we will show degree lower bounds for a Positivstellensatz Calculus proof of the claim that some knapsack problem has no solution. We will also show that the use of inequality (instead of just equations) reduces the degree of the proof on some instances.

    This presentation is based on the paper Complexity of Positivstellensatz proofs for the knapsack by Dima Grigoriev (link.springer.com/article/10.1007%2Fs00037-001-8192-0).

  • Monday Oct 7 at 12:00 noon in 4523
    On fitting too many pigeons into too few holes — the sequel
    (Mladen Mikša, Theory Group, KTH)

    In a breakthrough result, Haken (1985) showed that it is exponentially hard for the resolution proof system to prove that n+1 pigeons don't fit into n holes. However, what happens when the number of pigeons increases? Since it becomes increasingly obvious that not every pigeon can get a different hole, perhaps one can find shorter proofs as the number of pigeons goes to infinity? This notorious open problem was finally resolved by Raz (2001), who established that even for infinitely many pigeons one still needs proofs of exponential length. Raz's result was subsequently simplified and strengthened by Razborov in a sequence of three papers.

    In this complexity meeting we will return to Razborov's proof, which we discussed once already during the spring term. Somehow we ran out of steam a bit by the time we got to the low-level technical details, but this time nothing will stop us! We will once more go over Razborov's proof in all its wonderful mysteriousness, and will hopefully have time to ponder the remaining open questions that Razborov raises. If time (and energy) permits, we will also look into a generalization of Razborov's proof to the strongest version of the pigeonhole principle.

    This talk will be self-contained and everyone should be able to follow it even if they did not attend the previous talk (during the spring). However, as complexity meetings go, this will be a less friendly talk in that we will go over the basics fairly quickly, and so some familiarity with the definitions of resolution and the pigeonhole principle is probably helpful (though not strictly necessary).

Complexity meetings spring 2013

  • Monday May 27 at 13:15 in 1537
    Random CNFs are hard for polynomial calculus
    (Marc Vinyals, Theory Group, KTH)

    In the next to last meeting we studied [BGIP01], where a linear lower bound on degree (and therefore an exponential lower bound on size) was proven for refuting a specific family of formulas in polynomial calculus. A couple of follow-up questions one can ask are "Is it the case that most formulas are this hard?" and "If so, can we use the same techniques to prove it?" The answer to the first question is "yes" (in the sense that a randomly sampled CNF formula is very likely to be hard), and the answer to the second is "mostly."

    I will talk about the paper Random CNFs are hard for Polynomial Calculus by Ben-Sasson and Impagliazzo (journal version in 2010 based on a conference version in 2001), which proves a linear lower bound on the degree of refuting random CNFs for most flavours of polynomial calculus. We will reduce the SAT problem from satisfiability of random linear equations and use the particular structure of these equations to prove a lower bound.

  • Monday May 20 at 10:15 in 1537
    Lower bounds for the polynomial calculus and the Groebner basis algorithm
    (Massimo Lauria, Theory Group, KTH)

    This seminar will cover (parts of) the paper Lower Bounds for the Polynomial Calculus and the Groebner Basis Algorithm by Russell Impagliazzo, Pavel Pudlak, and Jiri Sgall. We will study the polynomial calculus proof system. In particular, we are going to show a degree lower bound of n/2 for refutations of the (functional) pigeonhole principle encoded as a set of polynomials of degree at most 2. We will also show a matching upper bounds for fields with large enough characteristic. A similar lower bound will be proved for the subset sum, but only for polynomial calculus over the field of reals.

  • Thursday May 2 at 10:15 in 4523
    Linear gaps between degrees for the polynomial calculus modulo distinct primes
    (Marc Vinyals, Theory Group, KTH)

    I will talk about the paper Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes by Buss, Grigoriev, Impagliazzo, and Pitassi (2001).

    We will see exponential lower bounds on proof size in polynomial calculus for Tseitin formulas (such formulas encode the handshaking lemma, i.e., that the sum of all vertex degrees in a graph is even). The lower bound is established by showing that any such proof must have high degree, and then appealing to a general theorem saying that strong lower bounds on proof degree imply strong lower bounds on proof size. [We will probably cover this general theorem in a separate meeting later in May.]

    A useful idea when proving degree lower bounds is to make a linear transformation from {0,1} to {-1,1}. In this latter setting polynomials encoding Tseitin formulas have a very simply structure. This simple structure is preserved by the polynomial calculus derivations, making it easier to prove lower bounds.

  • Monday Apr 29 at 10:15 in 4523
    Using the Groebner basis algorithm to find proofs of unsatisfiability
    (Massimo Lauria, Theory Group, KTH)

    I will review the paper Using the Groebner basis algorithm to find proofs of unsatisfiability by Clegg, Edmonds, and Impagliazzo (1996), explaining how standard algebraic manipulations of polynomials can be used to prove that a CNF formula is unsatisfiable.

    This is interesting because when it is possible to do the manipulations using only low-degree polynomials, then there is an efficient and systematic way to find a proof. For example, we can find constant-degree proofs in polynomial time; and for any formula that has some polynomial size proof we can find some (perhaps other) proof in subexponential time.

    The algorithm and its proof of correctness are the most technical part of the talk, so I will give a brief intro to the concept of Groebner bases (but no more than what is strictly necessary to present the algorithm).

  • Wednesday Apr 24 at 10:15 in 1625
    Survey of linear threshold functions
    (Li-Yang Tan, Columbia University)

    I will survey a few fundamental results about linear thresholds functions (LTFs) over {0,1}^n, including:

    • Total influence and Peres' noise sensitivity bound.
    • Chow's theorem and efficient reconstruction from Chow parameters.
    • Integer-weight representations: Muroga-Toda-Takasu, Johan's lower bound, low-weight approximators.
    • The invariance principle and regularity lemmas for LTFs.
    • Lots of open problems along the way.

Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2017-05-18