Proof Logging for MaxSAT – The Past, The Present and The Future

Published on ● Video Link: https://www.youtube.com/watch?v=yFoo9Wbwplw



Category:
Vlog
Duration: 28:21
108 views
2


Jeremias 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.







Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Satisfiability: Theory Practice and Beyond
Jeremias Berg