Speaker: |
Sreejata Kishor Bhattacharya (TIFR) |

Organiser: |
Varun Ramanathan |

Date: |
Friday, 10 May 2024, 16:00 to 17:00 |

Venue: |
A-201 (STCS Seminar Room) |

(Scan to add to calendar)

A proof system P is called automatizable if there is an algorithm A that, given 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 resolution is automatizable. In a breakthrough result, Atserias and Muller showed that automating resolution is NP hard. They construct a polynomial time computable transformation A that, on input a CNF phi, outputs an unsatisfiable CNF A(phi) such that:

(i) If phi is satisfiable, A(phi) has polynomial sized resolution refutations

(ii) If phi is not satisfiable, A(phi) does not have any subexponential sized resolution refutation

We shall describe this construction.