Tata Institute of Fundamental Research

Proof Complexity of MaxSAT Resolution

STCS Student Seminar
Speaker: Gaurav Sood (Institute of Mathematical Sciences Chennai, Tamil Nadu)
Organiser: Prerona Chatterjee
Date: Thursday, 25 Jun 2020, 14:30 to 15:30
Venue:

(Scan to add to calendar)
Abstract:  Zoom details:
Meeting ID: 613 566 8340
Password: 183102
Abstract: Boolean satisfiability (SAT) is the quintessential NP-complete problem. It has given rise to many areas of research within theoretical computer science, one of them being proof complexity. Given a proof system for SAT, we ask questions of the following form: is there a short proof that an unsatisfiable formula is unsatisfiable?

MaxSAT is the related problem of determining the maximum number of satisfiable clauses, and like SAT, it has its own proof systems. In this talk, we will study a proof system for MaxSAT proposed by Bonet et al. in 2007, and compare it with proof systems for SAT. This is joint work with Yuval Filmus, Meena Mahajan and Marc Vinyals.