2024W

• Algorithmics / 186.814 / VU
• Bachelor Thesis in Computer Science / 186.819 / PR

2025S

• Algorithms and Data Structures / 186.866 / VU
• Seminar on Algorithms / 186.182 / SE
• Structural Decompositions and Algorithms / 186.856 / VU

• From QBF to DQBF: Theory together with Practice
  2021 – 2022 / Austrian Science Fund (FWF)
  Publications: 154458 / 193563

• Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths / Beyersdorff, O., Blinkhorn, J. L., & Peitl, T. (2024). Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths. ACM Transactions on Computation Theory, 16(4), Article 22. https://doi.org/10.1145/3689345
  Download: Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths (530 KB)
• QCDCL with cube learning or pure literal elimination – What is best? / Böhm, B., Peitl, T., & Beyersdorff, O. (2024). QCDCL with cube learning or pure literal elimination – What is best? Artificial Intelligence, 336, Article 104194. https://doi.org/10.1016/j.artint.2024.104194
  Download: QCDCL with cube learning or pure literal elimination – What is best? (2.34 MB)
• Should Decisions in QCDCL Follow Prefix Order? / Böhm, B., Peitl, T., & Beyersdorff, O. (2024). Should Decisions in QCDCL Follow Prefix Order? Journal of Automated Reasoning, 68(1), Article 5. https://doi.org/10.1007/s10817-024-09694-6
• Are hitting formulas hard for resolution? / Peitl, T., & Szeider, S. (2023). Are hitting formulas hard for resolution? Discrete Applied Mathematics, 337, 173–184. https://doi.org/10.1016/j.dam.2023.05.003
  Download: PDF (732 KB)
  Project: REVEAL-AI (2020–2024)
• A SAT Solver's Opinion on the Erdos-Faber-Lovász Conjecture / Kirchweger, M., Peitl, T., & Szeider, S. (2023). A SAT Solver’s Opinion on the Erdos-Faber-Lovász Conjecture. In M. Mahajan (Ed.), 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) (pp. 1–17). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.13
  Download: PDF (651 KB)
  Projects: REVEAL-AI (2020–2024) / SLIM (2019–2024)
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution / Beyersdorff, O., Blinkhorn, J., Mahajan, M., & Peitl, T. (2023). Hardness Characterisations and Size-width Lower Bounds for QBF Resolution. ACM Transactions on Computational Logic, 24(2), Article 10. https://doi.org/10.34726/3603
  Download: Posted for your personal use. Not for redistribution. (631 KB)
  Project: From QBF to DQBF: Theory together with Practice (2021–2022)
• Hard QBFs for merge resolution / Beyersdorff, O., Blinkhorn, J., Mahajan, M., Peitl, T., & Sood, G. (2023). Hard QBFs for merge resolution. ACM Transactions on Computation Theory. https://doi.org/10.1145/3638263
  Project: From QBF to DQBF: Theory together with Practice (2021–2022)
• Co-Certificate Learning with SAT Modulo Symmetries / Kirchweger, M., Peitl, T., & Szeider, S. (2023). Co-Certificate Learning with SAT Modulo Symmetries. In E. Elkind (Ed.), Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence (IJCAI-23) (pp. 1944–1953). International Joint Conferences on Artificial Intelligence. https://doi.org/10.24963/ijcai.2023/216
• Proof Complexity of Fragments of Long-Distance Q-Resolution / Peitl, T., Slivovsky, F., & Szeider, S. (2019). Proof Complexity of Fragments of Long-Distance Q-Resolution. In Theory and Applications of Satisfiability Testing – SAT 2019 (pp. 319–335). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-030-24258-9_23
• Combining Resolution-Path Dependencies with Dependency Learning / Peitl, T., Slivovsky, F., & Szeider, S. (2019). Combining Resolution-Path Dependencies with Dependency Learning. In Theory and Applications of Satisfiability Testing – SAT 2019 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings. Int. Conference on Theory and Applications of Satisfiability Testing, Trento, Italy. LNCS. https://doi.org/10.1007/978-3-030-24258-9_22
• Advanced dependency analysis for QBF / Peitl, T. (2019). Advanced dependency analysis for QBF [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.71708
  Download: PDF (3.47 MB)
• Long-Distance Q-Resolution with Dependency Schemes / Peitl, T., Slivovsky, F., & Szeider, S. (2019). Long-Distance Q-Resolution with Dependency Schemes. Journal of Automated Reasoning, 63(1), 127–155. https://doi.org/10.1007/s10817-018-9467-3
• Dependency Learning for QBF / Peitl, T., Slivovsky, F., & Szeider, S. (2019). Dependency Learning for QBF. Journal of Artificial Intelligence Research, 65, 181–208. https://doi.org/10.1613/jair.1.11529
• Portfolio-Based Algorithm Selection for Circuit QBFs / Hoos, H. H., Peitl, T., Slivovsky, F., & Szeider, S. (2018). Portfolio-Based Algorithm Selection for Circuit QBFs. In Principles and Practice of Constraint Programming 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings (pp. 195–209). Springer-Verlag. https://doi.org/10.1007/978-3-319-98334-9_13
• Polynomial-Time Validation of QCDCL Certificates / Peitl, T., Slivovsky, F., & Szeider, S. (2018). Polynomial-Time Validation of QCDCL Certificates. In O. Beyersdorff & C. M. Wintersteiger (Eds.), Theory and Applications of Satisfiability Testing – SAT 2018 (pp. 253–269). Springer-Verlag, Lecture Notes in Artificial Intelligence 8268. https://doi.org/10.1007/978-3-319-94144-8_16
• Dependency Learning for QBF / Peitl, T., Slivovsky, F., & Szeider, S. (2017). Dependency Learning for QBF. In S. Gaspers & T. Walsh (Eds.), Theory and Applications of Satisfiability Testing – SAT 2017 : 20th International Conference, Melbourne, VIC, Australia, August 28 – September 1, 2017, Proceedings. Cham. https://doi.org/10.1007/978-3-319-66263-3_19
  Download: PDF (359 KB)
• Long Distance Q-Resolution with Dependency Schemes / Peitl, T., Slivovsky, F., & Szeider, S. (2016). Long Distance Q-Resolution with Dependency Schemes. In N. Creignou & D. Le Berre (Eds.), Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (pp. 500–518). Cham. https://doi.org/10.1007/978-3-319-40970-2_31
  Download: PDF (1.21 MB)