swe flag På svenska
School of
Electrical Engineering
and Computer Science
KTH / EECS / TCS / Jakob Nordström / Complexity meetings

I have moved to the Department of Computer Science (DIKU) at the University of Copenhagen and also have a part-time affiliation with the Department of Computer Science at Lund University. For now, my webpages still reside at KTH, and are being updated here, but this should change during 2021.

This also means that the Complexity meetings at KTH are no longer happening.

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 2019

  • Thursday Jun 13 at 10:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Pseudorandom Generators in Propositional Proof Complexity
    (Kilian Risse, TCS group, KTH)

    In this seminar we cover the definitions of pseudorandom generators in proof complexity and give an overview of the results. We then proceed to discuss the proofs for polynomial calculus in more detail. This talk is based on the paper "Pseudorandom Generators in Propositional Proof Complexity" by Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov and Avi Wigderson.

  • Wednesday Jun 12 at 13:15 in 4423, Lindstedtsvägen 5
    On MIP-style cutting plane generation for pseudo-Boolean solving
    (Jo Devriendt, TCS group, KTH)

    In modern mixed integer programming (MIP) solvers, cutting plane generation is a crucial ingredient that has led to tackling many otherwise unsolvable instances [1]. The most important of such generated "cuts" is the "mixed integer rounding" (MIR) cut. In this talk, we will go over what a MIR cut is and how it can be soundly derived from a Linear Programming (LP) solver's search state. We will also dive into the difficulties that arise when generating MIR cuts for the RoundingSat+SoPlex pseudo-Boolean solver, which uses linear inequalities as base constraints, as opposed to the linear equalities used by LP and MIP solvers.

    [1] Achterberg, Tobias & Wunderling, Roland. (2013). Mixed Integer Programming: Analyzing 12 Years of Progress.

  • Wednesday May 29 at 12:00 noon (sharp) in 4423, Lindstedtsvägen 5
    Polynomial calculus space and resolution width
    (Guillaume Lagarde, TCS Group, KTH)

    In this meeting, I will try to present in details a recent paper (Galesi, Kolodziejczyk, Thapen: eccc.weizmann.ac.il/report/2019/052/) that deals mostly with space lower bounds in polynomial calculus resolution. The authors exhibit an interesting connection between two distinct measures, namely, if a k-CNF formula requires width w in resolution then it requires space sqrt(w) in PCR. This result can somehow be seen as the counterpart of Atserias and Dalmau's result saying that width is a lower bound of space in resolution. This main theorem has several applications that we will try to highlight. In particular, it implies new (PCR) space lower bounds on formulas such as the linear ordering principle and the functional pigeonhole principle and it simplifies a proof lower bound for Tseitin formulas.

  • Monday May 20 at 10:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Automating resolution is NP-Hard
    (Dmitry Sokolov, TCS Group, KTH)

    We show that the problem of finding a Resolution refutation that is at most polynomially longer than the shortest one is NP-hard. In the parlance of proof complexity, resolution is not automatizable unless P = NP. Indeed, we show it is NP-hard to distinguish between formulas that have resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that resolution is not automatizable in subexponential time or quasi-polynomial time unless NP is included in SUBEXP or QP, respectively.

    This is a presentation of a recent paper by Albert Atserias and Moritz Müller.

  • Thursday May 16 at 13:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Size-degree trade-offs for sums-of-squares and Positivstellensatz proofs
    (Susanna F. de Rezende, TCS Group, KTH)

    This talk is based on a recent paper by Albert Atserias and Tuomas Hakoniemi showing that that if a system of degree-k polynomial constraints on n Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most s monomials, then it also has one with degree O(sqrt(n log s) + k). Analogous relations are known for weaker proof systems such as resolution and polynomial calculus.

    In this seminar, we will first quickly go over the proof of the Ben-Sasson–Wigderson size-width relation for resolution. We then show how the proof of the size-degree trade-off for SOS follows the general idea of the resolution proof, except that, since SOS is a static proof system, the unrestricting argument requires a lot of work. A key technical tool for this argument to work is a zero-gap duality theorem which follow from very general results in the theory of ordered vector spaces. Assuming this theorem, we will prove the size-degree trade-off for SOS. Finally, we will present some applications of this trade-off to Tseitin, Knapsack, and random CSPs.

  • Tuesday May 14 at 10:15 in 1440, Lindstedtsvägen 3
    SAT solving: The practical parts
    (Mate Soos, National University of Singapore)

    SAT solving, the paradigmatic NP-complete problem, has enjoyed a significant boom in the past decades. With the invention of conflict-driven clause-learning (CDCL) solvers, both the complexity and the types of problems that could be solved by SAT solvers have greatly expanded. In this seminar we will examine the details that allows current SAT solvers to tackle so many different problem types. It turns out that SAT solvers have all the classical issues that plague engineering — having to find a good compromise between sometimes very conflicting requirements — along with all the theoretical questions that still have not been answered. Here we will go into all the interesting engineering compromises having been made in the most popular SAT solvers, some of which may well be of interest in other parts of computer science.

  • Wednesday Apr 10 at 10:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Short proofs are hard to find
    (Dmitry Sokolov, TCS Group, KTH)

    Suppose that we have a short proof that some Boolean formula is unsatisfiable. Is it possible to find this proof in a reasonable time? For various proof systems, we show that under some assumption of a hardness of hitting set problem answer is no. In other words, resolution is not automatizable under GapETH. This is a simplification and improvement of the previous result of Alekhnovich and Razborov.

    The talk is based on a paper by Mertz, Pitassi and Wai.

  • Thursday Apr 4 at 10:15 in 4523, Lindstedtsvägen 5
    Experimental evaluation of integrating LP reasoning in RoundingSat
    (Jo Devriendt, TCS Group, KTH)

    Current generation PB solvers such as RoundingSat might benefit from LP relaxation reasoning to get out of rationally infeasible search states. To illustrate the current state of our investigation into this topic, I'll present a bunch of graphs summarizing three experiments:

    • on adding learnt constraints to the LP relaxation;
    • on postprocessing the Farkas constraint learnt from LP infeasibility;
    • on comparing RoundingSat(+LP), IntSat, Sat4J and SCIP on MIPLIB, PB competition and combinatorial benchmarks.
    This will be an informal talk with ample room for discussion.

  • Tuesday Mar 26 at 10:15 in 1625, Lindstedtsvägen 3
    A tradeoff between length and width in resolution
    (Guillaume Lagarde, TCS Group, KTH)

    In the resolution proof system, a classical result of Ben-Sasson and Wigderson (JACM 2001) exhibits an interesting connection between the minimal length and minimal width of refutations: if a formula in n variables has a refutation of polynomial length, then this formula should also has a refutation of small width, i.e., O(\sqrt(n log n)). A natural question is to know whether we can achieve both small length and small width in the same refutation. In this seminar, I will present a tradeoff result by Neil Thapen (ToC 2016) that answers negatively this question: there is a formula for which the decrease in width comes at the expense of an exponential increase in length.

  • Monday Jan 21 at 14:15 (note the time!) in 1537, Lindstedtsvägen 3
    Extending the resolution size lower bound for the weak FPHP to the weak onto-FPHP
    (Kilian Risse, TCS Group, KTH)

    We consider the weak functional pigeonhole principle formulas (WFPHP), where the number of pigeons is much larger than the number of holes. In this seminar we first give a short overview of Razborov's resolution lower bound for WFPHP formulas. We then move on to Razborov's follow-up paper where he managed to extend this lower bound to weak versions of the onto functional PHP formulas (a.k.a. perfect matching formulas).

    This will be a less friendly seminar than usual in that listeners are assumed to be familiar with with Razborovs WFPHP lower bound paper, so that we can move on quickly to his weak onto-FPHP lower bound paper.

  • Monday Jan 14 at 13:15 in 4523, Lindstedtsvägen 5
    Informal intro to MIP solving for proof complexity practitioners
    (Jo Devriendt, TCS Group, KTH)

    Modern Mixed Integer Programming (MIP) solvers are powerful reasoning engines that are the industry's de facto standard when solving combinatorial problems. The first part of this informal talk provides an overview of the architecture and the key algorithmic ideas of MIP solvers. I focus on their (dis)similiarities to CDCL solvers, and will highlight the way MIP solvers learn cutting planes and clauses. In the second part of the talk I'll go into technical details on request (in as far as a non-expert can). If there is time to fill, I'd like to share some experimental results, or explain a coefficient reduction idea.

Complexity meetings autumn 2018

The complexity meetings were mostly in pause mode during the autumn of 2018 since several TCS group members were attending the semester program Lower Bounds in Computational Complexity at the Simons Institute for the Theory of Computing.

  • Wednesday Dec 12 at 13:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Chronological backtracking
    (Janne Kokkala, TCS Group, KTH)

    I've recently been reading and diving into the details of the paper on chronological backtracking [1] by the winners of this year's SAT competition main track, it seems like a good idea to discuss the paper with the rest of the group. I'll give an informal presentation where I explain the general idea with some examples and then focus on some details which might not be obvious from just reading the paper. Finally if time permits, we can discuss ideas for possible future work.

    [1] link.springer.com/chapter/10.1007/978-3-319-94144-8_7 Nadel A., Ryvchin V. (2018) Chronological Backtracking.

    Abstract: "Non-Chronological Backtracking (NCB) has been implemented in every modern CDCL SAT solver since the original CDCL solver GRASP. NCBs importance has never been questioned. This paper argues that NCB is not always helpful. We show how one can implement the alternative to NCBChronological Backtracking (CB)in a modern SAT solver. We demonstrate that CB improves the performance of the winner of the latest SAT Competition, Maple_LCM_Dist, and the winner of the latest MaxSAT Evaluation Open-WBO."

Complexity meetings spring 2018

  • Wednesday Apr 25 at 10:15 in 4523, Lindstedtsvägen 5
    On lower bound techniques for Nullstellensatz and polynomial calculus
    (Jakob Nordström, TCS Group, KTH)

    This will be a spontaneously organized crash course on the proof systems Nullstellensatz and polynomial calculus. The intention is to have quite an informal and interactive discussion based on some slides and lecture notes. We will be very progressive and apply flipped classroom pedagogy, so participants are highly encouraged (and even expected) to have made a scan through the above material before the meeting to get a sense of what this is all about. During the meeting we will go over everything together and try to make sense of the details.

  • Tuesday Apr 24 at 14:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Algebraic proof generation
    (Daniela Ritirc, Johannes Kepler Universität Linz)

    Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale verification of arithmetic gate-level circuits, such as multipliers, to large bit-widths. We show that the polynomial calculus provides a frame-work to define a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level verification of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked efficiently with independent tools.

  • Wednesday Mar 21 at 13:15 in 4423, Lindstedtsvägen 5
    Polynomial calculus lower bound for the functional pigeonhole principle
    (Kilian Risse, TCS Group, KTH)

    In this seminar we show that any polynomial calculus proof of the functional pigeonhole principle requires degree at least n/2 and also provide a matching upper bound.

    The lower bound for FPHP was first proven by Razborov in his paper titled Lower bounds for the polynomial calculus, which appeared in 1996. The upper bound and the presentationwe will follow is by Impagliazzo, Pudlák, Sgall from their paper titled Lower Bounds for the Polynomial Calculus and the Groebner Basis Algorithm from 1999.

  • Friday Mar 16 at 12 noon in 4523, Lindstedtsvägen 5
    Communication complexity of XOR functions
    (Sagnik Mukhopadhyay, TCS Group, KTH)

    A prevalent trend in communication complexity is to prove communication lower bounds of composed functions in terms of the complexity measures of the functions that take part in composition. In recent times, a number of powerful tools have been invented to this end. One of them, namely the simulation technique, yields lower bound of communication complexity of f \circ g in terms of decision tree complexity of f and communication complexity of g.

    In this talk we look at the class of XOR functions. XOR functions are composed functions of the form f \circ XOR where XOR is a binary two-bit XOR. A naive upper bound for the communication complexity of f \circ XOR is the parity decision tree complexity of f. We show that the parity decision tree complexity of f completely characterizes the communication complexity of f \circ XOR (up to a polynomial factor). More specifically, we prove the following lower bound: the deterministic communication complexity of f \circ XOR is at least pdt(f)^{1/6}, where pdt denotes the parity decision tree complexity.

    This is a result of Hatami, Hosseini and Lovett in their paper titled Structure of protocols for XOR functions, which appeared in FOCS 2016.

  • Friday Mar 9 at 13:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Nullstellensatz over a finite field can be weaker than over the reals.
    (Kilian Risse, TCS Group, KTH)

    Denote by onto-FPHP^n_m the functional onto pigeonhole principle from n pigeons to m holes. In this seminar we show that onto-FPHP^{n+p^k}_n for n ≥ ((p+2)^k-p^k)/2 requires over Z_p a Nullstellensatz refutation of degree at least 2^k-1.

    This is a result of Beame and Riis in their paper titled More on the Relative Strength of Counting Principles from 1996.

Complexity meetings autumn 2017

  • Monday Dec 18 at 10:15 in 4523, Lindstedtsvägen 5
    A monotone switching lemma
    (Dmitry Sokolov, TCS Group, KTH)

    In this talk we consider the best known lower bound on monotone Boolean circuits: 2^{n^{1/3} / log(n)} that was given by Harnik and Raz. The core of technique is a "monotone switching lemma" that is another point of view on Razborov's approximation. We are going to prove this lemma and apply it for function that based on c-wise independent set to obtain the lower bound.

    Based on the paper "Higher lower bounds on monotone size" by D. Harnik and R. Raz.

  • Thursday Dec 14 at 13:15 in 1537, Lindstedtsvägen 3
    Proof logging for SAT solving techniques
    (Stephan Gocht, TCS Group, KTH)

    SAT solvers are used not only to find satisfying assignments to Boolean formulas but also to show that no such assignment exists. To enable verification that an answer "unsatisfiable" is correct, the solver needs to produce a proof that refutes the formula.

    In this talk we will explain the state of the art in proof logging and will show how to generate proofs for various techniques, such as Learned Clauses, Blocked Clause Elimination and Addition, and Extended Resolution. If time allows we will also look into proof logging for symmetry breaking.

    As the focus is on proof logging we will not cover how to figure out when such techniques are useful to apply, but only how to verify that such applications are sound.

  • Friday Dec 8 at 12:00 (note the time!) in 4523, Lindstedtsvägen 5
    From resolution to cutting planes and monotone circuits
    (Dmitry Sokolov, TCS Group, KTH)

    For any unsatisfiable CNF formula F that is hard to refute in the resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols (in particular, as in cutting planes) — or, equivalently, that a monotone function associated with F has large monotone circuit complexity.

    This result is essentially a lifting theorem for "decision dags" and "dag communication protocols."

    Joint work with Ankit Garg, Mika Göös, and Pritish Kamath (Monotone Circuit Lower Bounds from Resolution).

  • Monday Dec 4 at 13:15 in 1537, Lindstedtsvägen 3
    DAG-like communication X
    (Dmitry Sokolov, TCS Group, KTH)

  • Friday Nov 24 at 13:15 in 4423, Lindstedtsvägen 5
    DAG-like communication IX
    (Dmitry Sokolov, TCS Group, KTH)

  • Thursday Nov 23 at 13:15 in 4423, Lindstedtsvägen 5
    Generalizing Boolean Satisfiability I
    (Meysam Aghighi, TCS Group, KTH)

    In this seminar we will discuss the paper "Generalizing Boolean Satisfiability I: Background and Survey of Existing Work" by Dixon, Ginsberg, and Parkes.

    This is the first of three papers that describe ZAP, a satisfiability engine that combines the characteristics of high-performance solvers with a representation that captures the internal structure of the problems. The paper surveys the existing work and previous attempts to improve the performance of Davis-Putnam-Logemann-Loveland (DPLL) algorithm by exploiting the structure of the input problem. This includes examining extensions of Boolean language to cardinality constraints, pseudo-Boolean constraints, symmetry and a limited form of quantification.

  • Wednesday Nov 22 at 13:15 in the "research lounge" outside 4523, Lindstedtsvägen 5
    Resolution lower bounds for mutilated chessboard and Tseitin on the grid
    (Susanna F. de Rezende, TCS Group, KTH)

    Mutilated chessboard was the earliest proposed hard problem for theorem provers. The problem is as follows: given a 2n×2n chessboard with two diagonally opposite squares missing, prove that it cannot be covered by dominoes. The other problem which we address is Tseitin on the grid which is defined as follows. Given an n×n rectangular grid graph with all vertices labeled 0 except for one vertex which is labeled 1, prove that there is no subgraph of the grid such that all nodes labeled 0 have even degree and the node label 1 has odd degree.

    In this talk we will show that resolution requires size 2Ω(n) to solve these problems. The result is obtained by reducing both problems to variants of a tiling problem, and proving a lower bound for these tiling problems via the Pudlák game. The talk is based on the paper "'Planar' tautologies hard for Resolution" by Stefan Dantchev and Søren Riis.

  • Friday Nov 17 at 13:15 in 4423, Lindstedtsvägen 5
    DAG-like communication VIII
    (Dmitry Sokolov, TCS Group, KTH)

  • Thursday Nov 9 at 13:15 in 4423, Lindstedtsvägen 5
    DAG-like communication VII
    (Dmitry Sokolov, TCS Group, KTH)

  • Friday Oct 27 at 13:15 in 1537, Lindstedtsvägen 3
    DAG-like communication VI
    (Dmitry Sokolov, TCS Group, KTH)

    See below for the general abstract for this seminar mini-series.

  • Thursday Oct 26 at 13:15 in 4523, Lindstedtsvägen 5
    A fast pseudo-Boolean constraint solver
    (Meysam Aghighi, TCS Group, KTH)

    In this seminar we will get a presentation of the paper "A Fast Pseudo-Boolean Constraint Solver" by Chai & Kuehlmann. This paper discusses how efficient techniques for CNF SAT solving can be extended to pseudo-Boolean constraints (which in this context is a synonym for 0-1 linear inequalities with integer coefficients) and describes a solver that is based on generalized constraint propagation and conflict-based learning. It is arguably one of the key references in the pseudo-Boolean SAT solving literature.

  • Thursday Oct 19 at 13:15 in 4523, Lindstedtsvägen 5
    Generalized resolution
    (Meysam Aghighi, TCS Group, KTH)

    In this seminar we will go over two papers by Hooker on generalized resolution.

    Very briefly, generalized resolution is what you get when you take linear constraints with integer coefficients and want to do resolution derivations with such constraints. A summary of the two papers is as follows below.

    1. Generalized Resolution and Cutting Planes (AOR-88) The paper obtains a generalization of resolution that involves both cancellation-type and circulant-type sums by enlarging the class of cutting planes to cover clauses that state at least a specified number of literals are true. Then it shows the completeness of this generalization by proving that it generates all prime implications.

    2. Generalized Resolution for 0-1 Linear Inequalities (AMAI-92) The paper extends resolution to obtain a procedure for finding all valid cuts of a set of linear inequalities in 0-1 variables. Resolution generalizes to two cutting plane operations and generate all prime cuts that dominate every other valid cut. The paper then specializes the algorithm to classes of inequalities within which one can easily tell when one inequality dominates another.

  • Friday Oct 13 at 13:30 in 1537, Lindstedtsvägen 3
    DAG-like communication V
    (Dmitry Sokolov, TCS Group, KTH)

    See below for the general abstract for this seminar mini-series.

  • Friday Oct 6 at 13:30 in 1537, Lindstedtsvägen 3
    DAG-like communication IV
    (Dmitry Sokolov, TCS Group, KTH)

  • Monday Oct 2 at 13:15 in 4523, Lindstedtsvägen 5
    A tradeoff between length and width in resolution
    (Joseph Swernofsky, TCS Group, KTH)

    This talk will consist of a 45 minute overview of the content of the title paper, which was written by Neil Thapen. This will include a description of the results and formulas examined, as well as a sketch of the proof. Time and interest permitting, I will follow this with up to another hour of more thorough exposition of the proofs and discussion of open questions.

    Paper abstract: We describe a family of CNF formulas in n variables, with small initial width, which have polynomial length resolution refutations. By a result of Ben-Sasson and Wigderson it follows that they must also have narrow resolution refutations, of width O(sqrt(n logn)). We show that, for our formulas, this decrease in width comes at the expense of an increase in size, and any such narrow refutations must have exponential length.

  • Friday Sep 29 at 14:20 in 4523, Lindstedtsvägen 5
    DAG-like communication III
    (Dmitry Sokolov, TCS Group, KTH)

    See below for the general abstract for this seminar mini-series.

  • Friday Sep 22 at 13:15 in 4523, Lindstedtsvägen 5
    DAG-like communication II
    (Dmitry Sokolov, TCS Group, KTH)

    This second seminar will be concentrated on the connections between DAG communication models and Boolean and real circuits. All required defenitions will be repeated at the begining of the seminar.

    See below for the general abstract for this seminar mini-series.

  • Friday Sep 15 at 13:15 in 4523, Lindstedtsvägen 5
    DAG-like communication I
    (Dmitry Sokolov, TCS Group, KTH)

    This seminar is intended as an overview of what DAG-like communication is and how it can be used to derive strong results in circuit complexity and proof complexity, and will be the first seminar in a mini-series on this topic. Below follows an abstract for this seminar series.

    In 1990 Karchmer and Widgerson considered the following communication problem KW: Alice and Bob know a function f: {0, 1}^n \to {0, 1}, Alice receives a point x \in f^{-1}(1), Bob receives y \in f^{-1}(0), and their goal is to find a position i such that x_i != y_i. Karchmer and Wigderson proved that the minimal size of a Boolean formula for the function f equals the size of the smallest communication protocol for the KW relation. In this talk we consider a model of DAG-like communication (instead of classical one where protocols correspond to trees). We prove an analogue of the Karchmer-Wigderson Theorem for this model and Boolean circuits. We also consider a DAG-like analogue of real-valued and randomized communication protocols.

    The other motivation for this model comes from proof complexity. We simplify and improve Krajicek's interpolation technique that allows us to give lower bounds on huge class of proof systems.

    In the seminars, we expect to partially cover the following results:

    1. Relations between protocols, circuits and proofs.
    2. Lower bounds for DAG-like protocols (for monotone circuit complexity):
      • "Broken Mosquito Screen": bottleneck technique
      • "Clique-Coloring": approximation technique (with sunflowers)
      • "c-wise independent set": monotone switching lemma
    3. Connections between canonical search problem in proof complexity and KW relation.
    4. Lower bound for CP-proofs for ("almost") random CNF.

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 2021-06-24