In the talk, we consider the propositional proof system Resolution over Parities (Res(⊕)), in which the unsatisfiability of a Boolean formula is established by analyzing the parity of sums of variables, that is, through case analysis. This proof system extends classical Resolution by allowing reasoning modulo 2, thereby providing a more expressive framework for capturing parity-based inference. Understanding the strengths and limitations of Res(⊕) is an important step toward clarifying the role of parity in propositional proofs and SAT solving.A central open problem is to construct formulas that do not admit short (polynomial-size) refutations in this system. For many years, such hard instances were known only for the tree-like version of Res(⊕), which forbids the simultaneous analysis of multiple cases.In this talk, I will provide an overview of recent progress beyond tree-like restrictions, establishing exponential lower bounds for bounded-depth Res(⊕), where the depth grows superlinearly. I will also highlight the main lower-bound techniques, including random walks with restarts and lifting with stifling gadgets. No prior background in proof complexity will be assumed.

Short Bio: Dmitry Itsykson is a non-faculty researcher at Ben-Gurion University of the Negev (BGU). He received his PhD from St. Petersburg State University in 2009 and his Habilitation in 2022 from the St. Petersburg Department of Steklov Mathematical Institute of the Russian Academy of Sciences (PDMI). He has been a member of PDMI since 2009, where he holds the rank of Leading Researcher, and has been on leave since joining BGU in 2022.He held part-time Associate Professor positions at St. Petersburg Academic University (2010–2019) and St. Petersburg State University (2018–2022). His research interests are in computational complexity theory, with a focus on propositional proof complexity, average-case complexity, and lower bounds for Boolean satisfiability (SAT) algorithms.