There are many open problems in Discrete Mathematics, including Extremal Graph Theory, Ramsey Theory, and Design Theory, where one is interested in finding smallest examples or counterexamples to conjectures. Since the search space grows quickly with the size of the objects, advanced symmetry-breaking methods are essential. This project combines symmetry-breaking with SAT-based methods.

Relevant literature:
[1] Michael Codish, Alice Miller, Patrick Prosser, Peter J. Stuckey: Constraints for symmetry breaking in graph representation. Constraints, an Int. J. 24(1): 1-24 (2019).
[2] Tomás Peitl, Stefan Szeider: Finding the Hardest Formulas for Resolution. Journal Artificial Intelligence Research, volume 72, pages 69–97, 2021.
[3] Markus Kirchweger, Stefan Szeider: SAT Modulo Symmetries for Graph Generation. CP 2021: 34:1-34:16.

This project aims to utilize recent SAT-solving progress to tackle problems that arise in Computational Social Choice, such as the aggregation of preferences of multiple agents or the prevention of rigged elections. The work includes theoretical investigations combined with experimental evaluation on real-world data.

Relevant literature:
[1] Ulle Endriss: Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. AAAI 2020: 1918-1925.
[2] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

This project analyzes subsymbolic machine learning models, such as neural networks, with symbolic tools like SAT solvers. The aim is to replace opaque models with explainable and verifiable models, easily checked for bias.

Relevant literature:
[1] Alexey Ignatiev, Nina Narodytska, João Marques-Silva: Abduction-Based Explanations for Machine Learning Models. AAAI 2019: 1511-1519.
[2] Christoph Molnar: Interpretable machine learning. A Guide for Making Black Box Models Explainable, 2019.
[3] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.
[4] Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider: Learning fast-inference Bayesian networks. Proceedings of NeurIPS 2021, the Thirty-fifth Conference on Neural Information Processing Systems, 2021.

Many computational problems that arise in Artificial Intelligence and Combinatorial Optimization are intractable. Nevertheless, efficient, practical algorithms have been developed that exploit the hidden structure of problem instances that arise from real-world applications. This project aims at utilizing recent progress in Machine Learning to speed up such solving algorithms.
Relevant literature:
[1] Yoshua Bengio, Andrea Lodi, Antoine Prouvost: Machine learning for combinatorial optimization: A methodological tour d’horizon. Eur. J. Oper. Res. 290(2): 405-421 (2021)
[2] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Learning Rate Based Branching Heuristic for SAT Solvers. SAT 2016: 123-140
[3] Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider: Portfolio-Based Algorithm Selection for Circuit QBFs. CP 2018: 195-209