Assignment #1.

Assignment #2.

1. For every $k>0$ there exists a $\Sigma_1^b(\alpha)$ formula $A$ such that $T_2^k(\alpha)\vdash A$ whereas $S_2^k(\alpha)\not\vdash A$ (see e.g. [18, Problem 6]; this source also contains a discussion of candidate $A$s).
2. For a fixed formula $A(x)$ (not necessarily bounded), define the hierarchy $\Sigma_k^b(A),\Pi_k^b(A)$ similarly to $\Sigma_k^b,\Pi_k^b$ but allowing one extra clause: every formula of the form $A(t)$ ($t$ any term) belongs to $\Sigma_0^b(A)\cup \Pi_0^b(A)$. The theories $S_2^k(A), T_2^k(A)$ are defined respectively. Does there exist a specific formula $A$ such that $S_2(A)$ is not finitely axiomatizable (or at least such that $S_2^1(A)\neq T_2^1(A)$)?
   This problem has developed from a question asked in the class. An affirmative answer clearly implies that $S_2(\alpha)$ is not finitely axiomatizable, and an intended approach to this problem would be to try to take as $A$ an arithmetic definition of an oracle separating levels of the polynomial hierarchy.
3. Does $Res(2)$ have Feasible Interpolation Property (for the negative answer you can use any reasonable complexity assumption)?
4. The Existential Interpolation Property for a proof system $f$ means that whenever $A(x)\lor B(y)$ has an $f$-proof of size $s$ then either $A(x)$ or $B(y)$ has an $f$-proof of size polynomial in $s$.
   Does the (Extended) Frege proof system possess EIP (again, modulo any reasonable complexity assumption in case of negative anwer)?
5. Is the resolution proof system quasi-automatizable (again, modulo assumptions)? (See e.g. [22].)
6. Let $\Delta$ be any fixed constant. Prove that with probability $1-o(1)$ a random CNF that has $n$ variables and $\Delta n$ clauses does not posses an $F_2$ (depth-2 Frege) refutation of polynomial size.
7. Does $onto-FPHP^\infty_n$ have a polynomial size bounded-depth Frege proof? ([17, Problem 2]; quasi-polynomial bounds are known.)
8. Does $onto-FPHP^\infty_n$ have a quasi-polynomial size $Res(t)$ proof for any constant $t$? ([17, Problems 3,4]; this is true if $t$ is allowed to grow polylogarithhmically in $n$).
9. We know that the minimal size of a resolution refutation of $onto-FPHP^\infty_n$ behaves as $\exp(n^{\epsilon})$, where $\epsilon\in [1/3,1/2]$. Determine the right value of $\epsilon$. ([17, Problem 5].)
10. Prove superpolynomial lower bounds for the system $F_d[p]$ ($p$ a prime), that is bounded-depth Frege augmented with counting connectives $MOD_p$ [18, Problem 10].
11. Find a "direct" proof of superpolynomial lower bounds for the Cutting Planes proof system.
12. Prove superpolynomial lower bounds for the DAG version of the Lovasz-Schrijver proof system $LS$.
13. Prove superlogarithmic lower bounds on the refutation rank for the system $LS_{\ast}$ that extends Lovasz-Schrijver by allowing the full power of the rule $f\geq 0, g\geq 0 \Longrightarrow fg\geq 0$, $f,g$ arbitrary linear forms. Precise definitions can be found in [27]; this paper also proves an $\Omega(\log n)$ bound.
14. Prove that there exist Nisan generators stretching $n$ bits to $2^{n^\epsilon}$ bits that are hard for Resolution. All definitions can be found in [33] (you can use any of the encodings described there), and it solves this problem for Resolution width. The best we can do at the moment in terms of Resolution size is $n^{3-\epsilon}$ bits [34].

One good starting point might be the survey paper [1] by Nate Segerlind. It is (to the best of my knowledge) the most recent writing on the subject, it contains a comprehensive list of literature, and it includes recommendations for further reading, specifically indicating the topics where other surveys offer a different perspective.

The only drawback of the survey [2] by Paul Beame and Toni Pitassi is that it is a little bit outdated. Due to natural limitations, lecture notes [3] by Paul Beame are not intended to be comprehensive. But if a topic is covered there, this is usually also one of the best expositions.

Research on Bounded Arithmetic heavily uses standard machinery from mathematical logic (Gentzen-style calculus, cut elimination, Herbrand theorem etc.), while much of the propositional proof complexity is based upon combinatorial and algebraic techniques parallel to those employed in the circuit complexity and similar disciplines. It is not totally inconceivable that a certain part of the audience has developed a much better taste to the techniques of the second (combinatorial) kind. And, as a courtesy to these listeners, after a word (well, actually a few words) of introduction on January 6, and before immersing into the logical formalism for a few weeks, we will do preview of a sort. Namely, we will prove right away one basic result from the propositional part of the course known as width-size tradeoff for resolution (with applications). Our exposition will follow, more or less closely, the original paper [4]; this material is also covered in [1,3].

Several lectures in the second part will be devoted to outreach activity, that is, important by-products of research in the propositional proof complexity. We will certainly cover applications to:

1. integrality gaps of various LP/SDP relaxation procedures for integral programming (see [5,6] and extended follow-up literature);
2. learning theory [7].