BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/755
DTSTAMP:20230914T125937Z
SUMMARY:A Generalized Method for Proving Polynomial Calculus Degree Lower B
ounds
DESCRIPTION:Speaker: Jakob Nordstrom (KTH Royal Institute of Technology\nSc
hool of Computer Science and Communication\nSE-100 44 Stockolm\nSweden)\n\
nAbstract: \nWe study the problem of certifying unsatisfiability of formul
as in propositional logic. For proof systems such as resolution and polyno
mial calculus it is known that if the clause-variable incidence graph of a
CNF formula is an expander (i.e.\, is very well-connected)\, then proving
that this formula is unsatisfiable is hard. We further develop techniques
in [Alekhnovich and Razborov '03] to show that if one can "cluster" claus
es and variables in a way that "respects the structure" of the formula in
a certain sense\, then it is sufficient that the incidence graph of this c
lustered version is an expander. We also give a unified view of resolution
and polynomial calculus lower bounds in terms of a 2-player game played o
n this graph\, where the difference between resolution and polynomial calc
ulus is just in which player has to go first. As a corollary\, we prove th
at the functional pigeonhole principle (FPHP) formulas are hard for polyno
mial calculus\, answering an open question in [Razborov '02].\n
URL:https://www.tcs.tifr.res.in/web/events/755
DTSTART;TZID=Asia/Kolkata:20170221T160000
DTEND;TZID=Asia/Kolkata:20170221T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR