BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/347
DTSTAMP:20230914T125920Z
SUMMARY:On the Virtue of Succinct Proofs: Amplifying Communication Complexi
ty Hardness to Time-Space Trade-offs in Proof Complexity
DESCRIPTION:Speaker: Jakob NordstrÃ¶m (KTH Royal Institute of Technology\nS
chool of Computer Science and Communication\nSE-100 44 Stockholm\nSWEDEN)\
n\nAbstract: \nAn active line of research in proof complexity over the las
t decade has been the study of proof space and trade-offs between size and
space. Such questions were originally motivated by practical SAT solving\
, but have also led to the development of new theoretical concepts in proo
f complexity of intrinsic interest and to results establishing nontrivial
relations between space and other proof complexity measures.\nBy now\, the
resolution proof system is fairly well understood in this regard\, as wit
nessed by a long sequence of papers leading up to [Ben-Sasson and Nordstro
m 2008\, 2011] and [Beame\, Beck\, and Impagliazzo 2012]. However\, for ot
her relevant proof systems in the context of SAT solving\, such as polynom
ial calculus (PC) and cutting planes (CP)\, very little has been known.\nI
nspired by [BN08\,BN11]\, we consider CNF encodings of so-called pebble ga
mes played on graphs and the approach of making such pebbling formulas har
der by simple syntactic modifications. We use this paradigm of hardness am
plification to make progress on the relatively longstanding open question
of proving time-space trade-offs for cutting planes and polynomial calculu
s. Specifically\, we exhibit a family of formulas F_n such that:\n- F_n ha
s size Theta(n) and width O(1).\n- F_n has a resolution refutation in leng
th O(n) which generalizes to both CP and PC.\n- For any refutation of F_n
in CP or PCR (an extension of PC) in length L and space s it holds that s
log L is at least (roughly) sqrt[4]{n}.\nA crucial technical ingredient in
our result is a new two-player communication complexity lower bound for c
omposed search problems in terms\nof block sensitivity\, a contribution th
at we believe to be of independent interest.\n
URL:https://www.tcs.tifr.res.in/web/events/347
DTSTART;TZID=Asia/Kolkata:20130313T153000
DTEND;TZID=Asia/Kolkata:20130313T163000
LOCATION:AG-69
END:VEVENT
END:VCALENDAR