Arbetsspråket i Teorigruppen är engelska och därför finns denna sida bara
i engelsk version.
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 email 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 listenerfriendly onehour 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 BenSasson, Alexander A.
Razborov and Avi Wigderson.
Wednesday Jun 12 at 13:15 in 4423, Lindstedtsvägen 5
On MIPstyle cutting plane generation for pseudoBoolean 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 pseudoBoolean
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 kCNF 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 NPHard
(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
NPhard. In the parlance of proof complexity, resolution is
not automatizable unless P = NP. Indeed, we show it is NPhard
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
quasipolynomial 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
Sizedegree tradeoffs for sumsofsquares 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 degreek
polynomial constraints on n Boolean variables has a
SumsofSquares (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 BenSasson–Wigderson sizewidth relation for
resolution. We then show how the proof of the sizedegree
tradeoff 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 zerogap duality theorem
which follow from very general results in the theory of
ordered vector spaces. Assuming this theorem, we will prove
the sizedegree tradeoff for SOS. Finally, we will present
some applications of this tradeoff 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 NPcomplete problem, has enjoyed
a significant boom in the past decades. With the invention of
conflictdriven clauselearning (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 BenSasson
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 ontoFPHP
(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 followup 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
ontoFPHP 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 nonexpert 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/9783319941448_7
Nadel A., Ryvchin V. (2018) Chronological Backtracking.
Abstract: "NonChronological 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
OpenWBO."
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 gatelevel circuits,
such as multipliers, to large bitwidths. We show that the polynomial
calculus provides a framework to define a practical algebraic calculus
(PAC) proof format to capture lowlevel algebraic proofs needed in
scalable gatelevel verification of arithmetic circuits. We apply
these techniques to generate proofs obtained as byproduct of verifying
gatelevel multipliers using stateoftheart 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
twobit 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 ontoFPHP^n_m the functional onto pigeonhole principle from
n pigeons to m holes. In this seminar we show that
ontoFPHP^{n+p^k}_n for n ≥ ((p+2)^kp^k)/2 requires over
Z_p a Nullstellensatz refutation of degree at least 2^k1.
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 cwise 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 gadgetcomposed
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
DAGlike communication X
(Dmitry Sokolov, TCS Group, KTH)

Friday Nov 24 at 13:15
in 4423, Lindstedtsvägen 5
DAGlike 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
highperformance 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 DavisPutnamLogemannLoveland (DPLL) algorithm by exploiting
the structure of the input problem. This includes examining
extensions of Boolean language to cardinality constraints,
pseudoBoolean 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
DAGlike communication VIII
(Dmitry Sokolov, TCS Group, KTH)

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

Friday Oct 27 at 13:15
in 1537, Lindstedtsvägen 3
DAGlike communication VI
(Dmitry Sokolov, TCS Group, KTH)
See below for the general abstract for this seminar miniseries.

Thursday Oct 26 at 13:15
in 4523, Lindstedtsvägen 5
A fast pseudoBoolean constraint solver
(Meysam Aghighi, TCS Group, KTH)
In this seminar we will get a presentation of the paper
"A Fast PseudoBoolean Constraint
Solver" by Chai & Kuehlmann.
This paper discusses how efficient techniques for CNF SAT solving can be
extended to pseudoBoolean constraints (which in this context is a synonym
for 01 linear inequalities with integer coefficients) and describes a
solver that is based on generalized constraint propagation and
conflictbased learning. It is arguably one of the key references in the
pseudoBoolean 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 (AOR88) The paper
obtains a generalization of resolution that involves both
cancellationtype and circulanttype 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 01 Linear Inequalities (AMAI92)
The paper extends resolution to obtain a procedure for finding
all valid cuts of a set of linear inequalities in 01
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
DAGlike communication V
(Dmitry Sokolov, TCS Group, KTH)
See below for the general abstract for this seminar miniseries.

Friday Oct 6 at 13:30
in 1537, Lindstedtsvägen 3
DAGlike 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 BenSasson 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
DAGlike communication III
(Dmitry Sokolov, TCS Group, KTH)
See below for the general abstract for this seminar miniseries.

Friday Sep 22 at 13:15
in 4523, Lindstedtsvägen 5
DAGlike 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 miniseries.

Friday Sep 15 at 13:15
in 4523, Lindstedtsvägen 5
DAGlike communication I
(Dmitry Sokolov, TCS Group, KTH)
This seminar is intended as an overview of what DAGlike
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 miniseries 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 DAGlike communication (instead of
classical one where protocols correspond to trees). We prove
an analogue of the KarchmerWigderson Theorem for this model and
Boolean circuits. We also consider a DAGlike analogue of
realvalued 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:

Relations between protocols, circuits and proofs.

Lower bounds for DAGlike protocols (for monotone circuit complexity):

"Broken Mosquito Screen": bottleneck technique
 "CliqueColoring": approximation technique (with sunflowers)
 "cwise independent set": monotone switching lemma

Connections between canonical search problem in proof complexity and KW relation.
 Lower bound for CPproofs 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 wellknown 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

proofs of any tautology F in the proof system RCC (which is
stronger than cutting planes), and

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
logicbased 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:

Solving the general high school timetabling (XHSTT) problem using
logicbased approaches: maxSAT, SMTbitvector theory, and a hybrid
algorithm which combines maxSAT with large neighborhood search
(metaheuristic algorithm). These approaches are stateoftheart for
XHSTT, outperforming the competition on numerous benchmarks.

Computing the "representative" subset of all Pareto optimal solutions
for multiobjective optimization problems is known to be
Σ^{P}_{2}hard. We will see a shift in complexity to NPhardness when
considering an approximation using the notion of egalitarian
solutions, and discuss algorithms for its computation.

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 postsolving). We will formally define
the problem for set covering and set partitioning, prove Σ^{P}_{3}
and Σ^{P}_{2}hardness (respectively), and analyze algorithms for
computing such "resilient" solutions.

Wednesday May 3 at 10:15 in 4423
Lowdegree spectral algorithms are at least as strong as the
sumofsquares hierarchy for planted problems
(Sam Hopkins, Cornell University)
We study planted problemsfinding hidden structures in random noisy
inputsthrough the lens of the sumofsquares semidefinite programming
hierarchy (SoS). This family of powerful semidefinite programs has
recently yielded many new algorithms for planted problems, often
achieving the best known polynomialtime 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 lowdegree 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,
densestksubgraph, community detection in stochastic block models,
planted clique, and others, eigenvalues of degreed 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 kDNF
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 AtseriasDalmau'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 MayJuly, 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
ontofunction 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, BenSasson, 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 quasiNPhardness of coloring 2colorable8uniform
hypergraphs with 2^{(log N)^{1/4o(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.hpiweb.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 wellstudied 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
superconstant 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 andgates and orgates. 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/(d1))}).
This was proved by the use of the switching lemma.
This lemma says that if you have a depth2 circuit
which is an andofors 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 orofands maintaining small bottom fanin.
A more recent result (2014) says that best correlation of depthd,
sizeS circuit and parity of n inputs is
exp(Ω(n/(log S)^{(d1)}).
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 kDNF resolution on random 3CNFs: The sequel
(Marc Vinyals, Theory Group, KTH)
Last autumn we studied kDNF resolution, an extension of resolution
that works with kDNF 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 3CNF 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 kDNF resolution and
the switching lemma, and then show the lower bound for random 3CNFs in
full detail.

Wednesday Sep 24 at 10:15 in 1625
SheraliAdams rank lower bounds for the pigeonhole and least
number principles
(Massimo Lauria, Theory Group, KTH)
This talk will consider the SheraliAdams (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
SheraliAdams 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: nonbinomial 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: nonbinomial 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 socalled 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 kSAT gets
harder and harder as k grows and that the running time of the best kSAT
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 kCNFs 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 widthrestricted clause learning
(Jan Johannsen, LudwigMaximiliansUniversitä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
PHP_{n}
when learning only clauses of width
n/2.
They also require time
2^{Ω(n)}
to refute the ordering principle clauses
Ord_{n}
when learning only clauses of width
n/4.
In general, for unsatisfiable input formulas of small width, lower bounds for
widthrestricted 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 treelike
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:
NonBinomial 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
3regular 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 NPcomplete problem of kclique, and for an
explicit monotone problem by connecting the Pcomplete problem of
generation with reversible pebble games. This gives alternative proofs
of the separations of mNC from mP and of mNC^i from mNC^{i+1} ,
different from RazMcKenzie (Combinatorica '99).

Wednesday Dec 4 at 10:15 in 1625
Linear rank Lasserre lower bounds for kXOR and kSAT
(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 kCSP. 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 kCSPs (Schoenebeck,
2008).

Thursday Nov 21 at 12:00 noon in 1537
Lower bounds for kDNF resolution on random 3CNFs
(Marc Vinyals, Theory Group, KTH)
We continue our study of kDNF resolution, an extension of resolution
that works with kDNF 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 followup work, Alekhnovich refined their arguments and
proved exponential length lower bounds for random CNFs of minimal
width 3 (2CNFs are always easy).
We will give an exposition of Alekhnovich's result as presented in the
paper Lower Bounds for kDNF Resolution on Random 3CNFs
(dx.doi.org/10.1007/s0003701100260).

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%2Fs0003700181920).

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 lowlevel 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 selfcontained 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 followup 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 BenSasson 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 lowdegree polynomials, then there is an
efficient and systematic way to find a proof. For example, we can find
constantdegree 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
(LiYang 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.
 Integerweight representations: MurogaTodaTakasu, Johan's lower
bound, lowweight approximators.
 The invariance principle and regularity lemmas for LTFs.
 Lots of open problems along the way.
