Resolution Width Lifts to Near-Quadratic-Depth Res($\oplus$) Size by Dmitry Itsykson

Value of the Information & Strength of the Argument

The results are of significant value in proof complexity, providing concrete lower bounds that connect resolution width to depth in the setting of parity resolution. The first result offers a clean quadratic size bound, while the main lifting theorem is technically deep, introducing a robust framework based on structured restrictions and closure properties. The proof strategy is well-argued: it progressively builds a distribution over paths, using game-theoretic arguments to ensure that the final node is ’easy to kill’ while any particular semantic consequence is unlikely. The argumentation is rigorous, with careful attention to the definitions of safe matrices, closures, and H-good restrictions. The presentation is concise but self-contained for an expert audience, and the logical flow from the key lemma to the final theorems is clear.

Scientific Rigor, Source Quality, Title Accuracy

The scientific rigor is high: the talk relies on established results (e.g., Ben-Sasson’s width-size relation, Atserias-Dalmau games) without extensive citation within the talk, but the underlying work is presumably peer-reviewed. The only explicit source provided is the program page of the ICTS workshop, which serves as context rather than a direct citation of the paper. The title exactly matches the content: the talk is entirely devoted to proving that resolution width ’lifts’ to near-quadratic depth for Res(⊕). No irrelevant topics are introduced. The lack of external references in the description is a minor limitation, but the technical depth and coherence of the presentation compensate.

The title accurately describes the content: the talk demonstrates that resolution width lifts to near-quadratic depth lower bounds for resolution over parity (Res(⊕)).

8/10

The talk presents rigorous theoretical results with proof sketches, based on a joint paper likely peer-reviewed. The presentation is formal and technically precise, although no external verification is provided.

Markers derived by PSI from the transcript: the creator did not define chapters.

• 00:00Introduction of the talk and joint work, overview of prior results and open questions.
• 02:30Definition of resolution over parity (Res(⊕)) and its parameters: size, width, depth.
• 07:00Statement of the first result: quadratic size lower bound for Res(⊕) refutations of lifted formulas.
• 13:00Statement of the main lifting theorem: depth lower bound in terms of resolution width and size.
• 20:00Proof sketch of the key lemma using H-good restrictions and closure properties.
• 35:00Open questions and concluding remarks.

• ICTS Program: Circuits, Communication, and Proofs — Official workshop page where this invited lecture took place, providing program description and context.