Hard Theorems

'Cause when the proof gets tough… the tough get provin' (…proof complexity lower bounds!)

Sums-of-squares integer programming relaxation: Lecture 8

Lecture 8: Sum of squares lower bound for k-SAT and k-XOR. Part 2/2.

Scribe: Mohamed Abdalmoaty


This whole lecture is devote to show that if a k-XOR formula \phi requires degree D refutations in Binomial Calculus (BC), then it requires degree D/2 Positivstellensatz Calculus refutations (\mathsf{PC}_>).

In the last lecture we already showed that for a random k-XOR formula the required degree D is large, therefore this part will conclude the proof of the lower bound for the degree of \mathsf{PC}_> refutations of random $k$-XORs.

Link: [Lecture notes 08]


Sums-of-squares integer programming relaxation: Lecture 7

Lecture 7: Sum of squares lower bound for k-SAT and k-XOR. Part 1/2.

Scribe: Ilario Bonacina


In this lecture we define the Positivstellensatz Calculus proof system and we show a lower bound for the degree needed to refute random k-XOR formulas. We define the Positivstellensatz Calculus, its subystem Binomial Calculus and prove a lower bound for the degree of random k-XOR formulas in Binomial Calculus. The proof of why this result leads to a lower bound for Positivstellensatz is in the next lecture.

Link: [Lecture notes 07]

Sums-of-squares integer programming relaxation: Lecture 6

Lecture 6: Max-Cut approximation as a Lasserre rounding.

Scribe: Marc Vinyals


We show how to give a good approximation for the max-cut problem using only low levels of the Lasserre hierarchy. This implies a separation between Sherali-Adams and Lasserre hierarchies. Additionally we introduce basic Fourier analysis in the boolean setting.

Link: [Lecture notes 06]

Sums-of-squares integer programming relaxation: Lecture 5

Lecture 5: Properties of the Lasserre Relaxation.

Scribe: Sangxia Huang


In this lecture, we study the properties of the solution vectors of the Lasserre relaxation. We start with some basic properties of the solutions, and then continue to show that the solution vectors give us a family of locally consistent distributions over feasible integral local solutions. At the end of the lecture, we see an example of this property in graph coloring.

Link: [Lecture notes 05]

Sums-of-squares integer programming relaxation: Lecture 4

Lecture 4: Semidefinite program relaxations of integer programs.

Scribe: Mariette Annergren


We continue the discussion on how to improve the initial relaxation made of an integer program. Here, we focus on semidefinite program (SDP) relaxations, and we introduce Lovász-Schrijver relaxation with semidefinite programming, and the Positivstellensatz, Positivstellensatz Calculus and sums-of-squares (SOS) proof systems.

Link: [Lecture notes 04]

The call for paper of MFCS 2015 is out!

The deadline is on April 22, 2015.

From the webpage http://mfcs2015.di.unimi.it/

The series of MFCS symposia, organized since 1972, has a long and well-established tradition. The MFCS symposia encourage high-quality research in all branches of theoretical computer science. Their broad scope provides an opportunity to bring together researchers who do not usually meet at specialized conferences. Quality papers presenting original research on theoretical aspects of computer science are solicited.

CCC 2015 accepted papers.

There will be a great Proof Complexity session at CCC2015.

  • Non-commutative formulas and Frege lower bounds: a new characterization of propositional proofs. Fu Li (Tsinghua University), Iddo Tzameret (Royal Holloway, University of London), Zhengyu Wang (Harvard University)
  • The space complexity of cutting planes refutations. Nicola Galesi (Sapienza University of Rome), Pavel Pudlák (Czech Academy of Sciences), Neil Thapen (Czech Academy of Sciences)
  • The functional pigeonhole principle requires polynomial calculus proofs of exponential size. Mladen Miksa (KTH Royal Institute of Technology), Jakob Nordstrom (KTH Royal Institute of Technology)
  • Tight size-degree lower bounds for sums-of-squares proofs. Massimo Lauria (KTH Royal Institute of Technology) Jakob Nordström (KTH Royal Institute of Technology)

See you all in Portland. If you come for STOC, no reason to miss CCC 2015!

CCC 2015 accepted papers.

Sums-of-squares integer programming relaxation: Lecture 3

Lecture 3: Improving linear relaxations of integer programs.

Scribe: Mariette Annergren


We discuss methods to improve the linear relaxations of integer programs.

They are systematic ways to find tighter and tighter polytopes containing the convex hull of the integer solutions. The main idea is to lift, that is, to augment the linear program to a higher dimensional space and then to project it down to the original space to obtain a polytope that is smaller than the one we started with. We shall see two different ways to do lift and project: namely the Lovász-Schrijver and Sherali-Adams hierarchies.

Link: [Lecture notes 03]

Highlight inverse search in Emacs + AUCTeX

I always lose track of the cursor when I use inverse search on LaTeX documents. This small hack will mitigate the pain.

One cool addition to Emacs, if you write papers using LaTeX1, is the powerful AUCTeX software. Among tons of useful features it gives the possibility to jump from any point in your LaTeX code to the corresponding point in the PDF document (this is called “forward search” in the lingo). If you have a proper PDF viewer (e.g. Evince on Linux or Skim on MacOSX) the target location will be highlighted.


But what about the opposite? If your setup is correct it is possible to click on the preview document, and Emacs will jump to the corresponding point in the appropriate LaTeX file.

If you are like me, you like low contrast themes a big Emacs windows (frames in Emacs parlance), so it is easy to lose track of the cursor, which can end up anywhere. With the following piece of code every time you use inverse search, the target location in the LaTex file will be highlighted as well.

(defadvice TeX-source-correlate-sync-source (after ad-TeX-correlate-center)
    "Center and highlight point after AUCTeX inverse-search."
    (pulse-momentary-highlight-one-line (point)))

Here’s the result.


This is of course useless if you use global-hl-line-mode, but I find quite annoying. The actual highlight style is due to the pulse.el package (included in recents GNU/Emacs versions).



which you should do, whatever some misinformed researchers say. At least if you are in Math, CS or Physics.

Sums-of-squares integer programming relaxation: Lecture 2

Lecture 2: Semidefinite programming and relaxations.

Scribe: Massimo Lauria


Semidefinite programs are a valuable tools in approximation algorithms and in combinatorial optimization, since semidefinite relaxations are usually stronger than linear ones. In this lecture we describe what is a semidefinite program.

Link: [Lecture notes 02]