Matti Järvisalo

Solving Harder-than-SAT Computational Social Choice Problems with SAT Solvers

Abstract: Social choice theory considers collective multi-agent decision-making scenarios where agents must reach a group-level consensus. Computational social choice is a modern area of artificial intelligence research that considers social choice mechanisms from the computer science perspective. Of particular interest are applications of computational techniques to provide more stringent analysis of social choice mechanisms (in terms of, e.g., computational complexity and representational aspects) and the development of practical algorithms for computationally hard problems in social choice. Among these directions, practical algorithms remain arguably somewhat underdeveloped. In this talk I will give an overview of our recent work towards closing some of this gap, with a special focus—as time permits—on coalition formation (the formation of coalitions based on preferences of individual agents) and judgment aggregation (capturing e.g. various types of voting mechanisms). In particular, I aim to explain how automated reasoning, and specifically Boolean satisfiability (SAT) solvers, can be harnessed for developing practical exact algorithms for decision and optimization problems studied in COMSOC that are in fact (presumably) harder that SAT, and how complexity analysis can support algorithm design for such problems.**

Bio: Matti Järvisalo is Professor of Computer Science (Algorithms and Machine Learning) 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 and declarative programming, combinatorial optimization, knowledge representation and graphical models, with key contributions especially in theory and practice of Boolean satisfiability (SAT), SAT-based decision, combinatorial optimization and counting procedures, and their applications. His group has been successful in developing state-of-the-art solvers and tools e.g. for SAT, maximum satisfiability (MaxSAT), pseudo-Boolean optimization, formal argumentation, and answer set programming. With over 160 peer-reviewed publications to date, Dr. Järvisalo has received various best paper awards and other international recognitions for his contributions, including the IJCAI-JAIR Best Paper Award and an IJCAI Early Career Spotlight, as well as further best paper recognitions at ECAI, CP, KR, ICLP and PGM. In addition to organizing various workshops and conferences, he was PC Chair for SAT'13, IJCAI-PRICAI'20 Demo Track, KR'23 Applications and Systems Track, and KR'24 In the Wild Track, Chair of the Finnish AI Society (EurAI member society of Finland) 2019-2021, and has served on program committees of over 100 conferences. Today he serves on the editorial boards of Journal of Artificial Intelligence Research, Journal of Automated Reasoning, and Journal of Satisfiability, Boolean Modeling and Computation. Dr. Järvisalo has also been involved in organizing various automated reasoning competitions, including the renown SAT solver competitions and MaxSAT Evaluations for many years.