PhD Position on Innovative Applications of SAT Techniques

There is an opening for a PhD position on innovative applications of SAT techniques (that includes, SAT, MaxSAT, (D)QBF, and related techniques), with theoretical and experimental objectives.

The position is within the new PhD program LogiCS@TUWien (cofounded by the European Commission), are for 4 years each, and come with an attractive full-time salary including all Austrian's social security benefits, and traveling allowance.

Successful applicants will work under the supervision of Prof. Stefan Szeider on one of the research topics:

Topic 10: Computer Search in Discrete Mathematics (click for more information)
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.

Topic 11: Formal Methods in Computational Social Choice (click for more information)

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.

Topic 12: SAT-Based Methods for Explainable Artificial Intelligence (click for more information)

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.

 

Application Instructions:

  1. Interested applicants can find instructions on how to apply here.
  2. The application deadline is May 8, 2022 (extended)
  3. Informal inquiries are welcome and should be directed to Stefan Szeider sz@ac.tuwien.ac.at