BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1423
DTSTAMP:20240509T082219Z
SUMMARY:Resolution is NP hard to automate
DESCRIPTION:Speaker: Sreejata Kishor Bhattacharya (TIFR)\n\nAbstract: \nA
proof system P is called automatizable if there is an algorithm A that\, g
iven input a statement phi\, runs in time poly(s) and outputs a P-proof of
phi of size at most poly(s)\, where s is the size of the shortest P-proof
of phi. It had been a long-standing open problem to determine if resoluti
on is automatizable. In a breakthrough result\, Atserias and Muller showed
that automating resolution is NP hard. They construct a polynomial time c
omputable transformation A that\, on input a CNF phi\, outputs an unsatisf
iable CNF A(phi) such that:(i) If phi is satisfiable\, A(phi) has polynomi
al sized resolution refutations(ii) If phi is not satisfiable\, A(phi) doe
s not have any subexponential sized resolution refutationWe shall describe
this construction.\n
URL:https://www.tcs.tifr.res.in/web/events/1423
DTSTART;TZID=Asia/Kolkata:20240510T160000
DTEND;TZID=Asia/Kolkata:20240510T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR