Collective Decision Making via Automated Reasoning

Collective decision-making tasks, such as voting, matching, and resource allocation, are frequently encountered in multi-agent scenarios where a consensus is sought for based on the-often conflictingpreferences of individual agents. Deciding if a consensus can be reached and finding such consensus give rise to computationally hard decision and optimization problems, characterized by NPcompleteness or even beyond-NP complexity. This complexity poses significant challenges for developing practical exact algorithms. At the same time, advances in automated logical reasoning techniques, such as Boolean satisfiability solvers, their extensions to higherlevel constraints, and optimization have proven successful for capturing and solving a wide range of computationally hard real-world problems. My doctoral research harnesses automated logical reasoning for developing novel types of practical, exact algorithms for computational social choice scenarios.