BARC talk by Shou Pang

Tuesday, 17 September 2019, Shou Pang, a Graduate Student at the University of Chicago, will give a talk "Large clique is hard on average for resolution ". 

Large clique is hard on average for resolution 

k-CLIQUE is a fundamental NP-hard problem. Its proof-theoretic counterpart is also a fundamental problem in proof complexity, in particular, in form of its average hardness on Erdos-Renyi random graphs. Strong lower bounds are previously known for some proof systems,  such as SOS and regular resolution, but the question remains widely open for systems like resolution. In this talk, we start with a brief  discussion on the CNF-encoding, with emphasis on exploring possible computational hardness, and show a 2^{k^{1-\epsilon}} average lower bound for k in n^(0,1/3). Towards an n^{\Omega(k)} lower bound, which is known in regular resolution, the second part of the talk focuses  on the difference between regular and general resolution. We propose the model of a-irregular resolution, a subsystem of resolution that  syntactically summarizes the power (i.e., separations) of general-over-regular that is known from the literature. Thus lower or upper bound for this model may tell, in a sense, whether there is "novel'' aspect of the regular-general difference that lies in a target CNF. For k- CLIQUE, we show that the n^{\Omega(k)} average lower bound can be extended to this model.

The host is Associate Professor Jakob Nordström and he invites to join afterwards as the formal talk will be followed by more informal, technical discussions in BARC's Creative Room (03-01-02) until 12:30. This is expected ot be quite interactive, perhaps even turning it into more of a discussion than a presentation at times. This second part is entirely optional, and can safely be skipped by everybody who feels that a regular 1-hour talk is sufficient to meet their needs.