Proof Logging for MaxSAT – The Past, The Present and The Future
2Jeremias Berg (University of Helsinki)
https://simons.berkeley.edu/talks/jeremias-berg-university-helsinki-2023-04-20
Satisfiability: Theory, Practice, and Beyond
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.