Meeting ID: 613 566 8340
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.