Abstract
In the last few decades, the Boolean optimization paradigm of maximum satisfiability (MaxSAT) has matured into an effective and thriving optimization paradigm. However, in contrast to SAT solving---on which much of modern MaxSAT solving relies---there has been significantly less development in tools and methods for proof logging MaxSAT solvers.
In this talk I give a brief overview of modern algorithms and heuristics for MaxSAT solving. I will focus especially on the motivation for and central challenges in developing proof logging for MaxSAT. I will also discuss the existing work on the topic and highlight some interesting future research directions.