Proof Complexity of MaxSAT Resolution


Gaurav Sood


Institute of Mathematical Sciences
Chennai, Tamil Nadu


Thursday, 25 June 2020, 14:30 to 15:30


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.