TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Tomas Peitl

Univ.Ass. Dr.techn.

Tomas Peitl

Role

Contact

2024W

2025S

 

  • 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
  • Davis and Putnam Meet Henkin: Solving DQBF with Resolution / Blinkhorn, J., Peitl, T., & Slivovsky, F. (2021). Davis and Putnam Meet Henkin: Solving DQBF with Resolution. In Theory and Applications of Satisfiability Testing – SAT 2021 (pp. 30–46). LNCS / Springer. https://doi.org/10.1007/978-3-030-80223-3_4
  • Finding the Hardest Formulas for Resolution (Extended Abstract) / Peitl, T., & Szeider, S. (2021). Finding the Hardest Formulas for Resolution (Extended Abstract). In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada, Canada. https://doi.org/10.24963/ijcai.2021/657
  • Finding the Hardest Formulas for Resolution / Peitl, T., & Szeider, S. (2020). Finding the Hardest Formulas for Resolution. In Principles and Practice of Constraint Programming 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7–11, 2020, Proceedings (pp. 514–530). LNCS. https://doi.org/10.1007/978-3-030-58475-7_30
  • Fixed-Parameter Tractability of Dependency QBF with Structural Parameters / Ganian, R., Peitl, T., Slivovsky, F., & Szeider, S. (2020). Fixed-Parameter Tractability of Dependency QBF with Structural Parameters. In Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning. 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece. https://doi.org/10.24963/kr.2020/40
  • 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)