Advances in Maximum Satisfiability

September 04, 1:45 pm - 5:00 pm (CEST)

Speakers: Jeremias Berg, Matti Järvisalo, Ruben Martins

Tutorial website:

Agenda: Advances in Maximum Satisfiability

In this tutorial, we will introduce MaxSAT, give an overview of the different techniques that have been developed for solving MaxSAT, focusing on recent advances and covering both complete and incomplete MaxSAT solving, and explain via case studies how MaxSAT has been used to solve problems from different areas of AI. We will also outline major current research directions in MaxSAT. After this tutorial, you should be better equipped to assess whether or not MaxSAT would be useful in your work and better able to use modern MaxSAT solvers in your work.

The tutorial is targeted towards both researchers working on related areas in automated reasoning, knowledge representation, and optimization, as well as more generally towards a wide range of the ECAI audience who could benefit from obtaining further knowledge of recent progress and state-of-the-art in MaxSAT solving and in applying MaxSAT to solve hard optimization problems arising from various AI and industrial problem domains. The tutorial assumes no background knowledge beyond what a new graduate student in computer science would possess.

Jeremias Berg (webpage) is Post-Doctoral Researcher at University of Helsinki, Finland. His research focuses especially on constraint optimization and maximum satisfiability, covering both theoretical and algorithmic aspects as well as applications. Dr. Berg has to-date circa 20 peer-reviewed papers published at venues such as AIJ, IJCAI, AAAI, ECAI, CP, and SAT. He has also contributed to the development of several state-of-the-art MaxSAT solvers and preprocessors, and is the primary developer of the Loandra solver which ranked on top in the incomplete track of MaxSAT Evaluation 2019. His PhD thesis on MaxSAT received the 2018 Doctoral Dissertation Award by University of Helsinki.

Matti Järvisalo (webpage) is Associate Professor of Computer Science at University of Helsinki, Finland, where he leads the Constraint Reasoning and Optimization group. His research interests span several areas in artificial intelligence, including automated reasoning, optimization, knowledge representation and graphical models. Beyond theoretical and algorithmic advances, his group has been successful in developing state-of-the-art solvers e.g. for Boolean satisfiability (SAT), maximum satisfiability (MaxSAT), formal argumentation, answer set programming, and their applications in structure learning and causal discovery. With more than 100 publications to date, Dr. Järvisalo has received various best paper awards and other international recognitions for his contributions, including the 2019 IJCAI-JAIR Best Paper Award and an IJCAI 2016 Early Career Spotlight, as well as further best paper awards at ECAI, CP, KR, ICLP and PGM. He was PC Chair for SAT 2013 and is PC Chair of IJCAI-PRICAI 2020 Demo Track as well as Chair of the Finnish AI Society (EurAI member society of Finland). Furthermore, Dr. Järvisalo has been involved in organizing the renown SAT solver competitions and MaxSAT Evaluations for many years.

Ruben Martins (webpage) is Systems Scientist at Carnegie Mellon University, USA. His interests lie in the intersection of constraint programming and synthesis, analysis and verification of programs. His recent research focuses on using programming synthesis to improve programmer’s productivity and to automate data science-related tasks such as data querying, imputation, consolidation, and tidying. Dr. Martins has more than 40 peer-reviewed papers published in top-tier venues, including, POPL, PLDI, FSE, SAT, CP, with a distinguished paper award at PLDI 2018 for his work on program synthesis. He has developed several award-winning constraint solvers and is the main developer of the Open-WBO MaxSAT solver that has ranked on top in several MaxSAT Evaluations. Since 2017, Dr. Martins organizes of the annual MaxSAT Evaluation where state-of-the-art MaxSAT solvers are independently evaluated.