Algorithms and Complexity Group
  • People
  • Research
  • Courses
  • Talks
  • Jobs
  • Contact

Tomáš Peitl

Address:
Tomáš Peitl
Technische Universität Wien
Institute of Logic and Computation
Favoritenstraße 9–11, E192-01
1040 Wien
Austria

Room: HB0418
Phone: +43(1)58801–192128
Email: peitl@ac.tuwien.ac.at
Web: http://www.ac.tuwien.ac.at/people/peitl/

Research Interests

  • QBF, DQBF, SAT, Proof Complexity, Complexity Theory, Graph Theory
  • Anything from theory through solver development to applications goes.

Current and previous positions

  • Since Sep 2023 I'm a University assistant and I additionally teach Algorithms and Data Structures, Algorithmics, and Structural Decompositions and Aglorithms
  • Between Nov 2021-Aug 23 I was a postdoc in the AC group, funded by the return phase of my FWF Erwin Schrödinger Fellowship and other FWF grants.
  • Between Nov 2019 and Oct 2021 I was a postdoc in the group of Olaf Beyersdorff at Friedrich Schiller University in Jena, Germany, funded by an FWF Erwin Schrödinger Fellowship.
  • Until October 2019 I was a PhD student funded by the FWF project P27721 and partially by Doctoral College Logical Methods in Computer Science, and I was also a project assistant in the Algorithms and Complexity Group. I started my PhD studies in September 2015 under the supervision of Prof. Dr. Stefan Szeider, and I succesfully defended my thesis on October 14th 2019.

Education

  • 2015-2019 PhD in Computer Science (TU Wien, PhD thesis; with a research stay with Holger Hoos at the University of British Columbia, Vancouver, Canada)
  • 2013-2015 master's in Mathematics (Comenius University, Bratislava Slovakia, with an Erasmus stay at the University of Primorska, Koper, Slovenia)
  • 2010-2013 bachelor's in Mathematics (Comenius University, Bratislava, Slovakia)

Software

  • The isomorph-free constrained graph-generation package SAT Modulo Symmetries
  • QBF solver Qute ,which implements QCDCL with dependency learning and the reflexive resolution-path dependency scheme Drrs.
  • short.py, a SAT-based tool to compute shortest proofs of minimally unsatisfiable formulas.
  • The long-distance Q-resolution strategy extractor qrp2rup will be available soon. Please send me an email if you're interested in using it before it's properly published.

Publications

See also my DBLP.

29 results
2025
[29]Breaking Symmetries in Quantified Graph Search: A Comparative Study
Mikoláš Janota, Markus Kirchweger, Tomáš Peitl, Stefan Szeider
AAAI 2025: The 39th Annual AAAI Conference on Artificial Intelligence, 2025.
Note: to appear
[bibtex]
2024
[28]Should Decisions in QCDCL Follow Prefix Order?
Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff
J. Autom. Reason., volume 68, number 1, pages 5, 2024.
[bibtex] [pdf] [doi]
[27]QCDCL with cube learning or pure literal elimination - What is best?
Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff
Artif. Intell., volume 336, pages 104194, 2024.
[bibtex] [pdf] [doi]
[26]Hard QBFs for Merge Resolution
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood
ACM Trans. Comput. Theory, volume 16, number 2, pages 6:1–6:24, 2024.
[bibtex] [pdf] [doi]
[25]Small unsatisfiable k-CNFs with bounded literal occurrence
Tianwei Zhang, Tomáš Peitl, Stefan Szeider
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (Supratik Chakraborty, Jie-Hong Roland Jiang, eds.), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1–31:22, 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
2023
[24]Are Hitting Formulas Hard for Resolution?
Tomáš Peitl, Stefan Szeider
Discr. Appl. Math., volume 337, pages 173–184, 2023.
[bibtex] [doi]
[23]A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture
Markus Kirchweger, Tomáš Peitl, Stefan Szeider
26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy (Meena Mahajan, Friedrich Slivovsky, eds.), volume 271 of LIPIcs, pages 13:1–13:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
[22]Co-Certificate Learning with SAT Modulo Symmetries
Markus Kirchweger, Tomáš Peitl, Stefan Szeider
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 1944–1953, 2023, ijcai.org.
Note: Main Track
[bibtex] [pdf] [doi]
2022
[21]Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl
ACM Transactions on Computational Logic, September 2022, Association for Computing Machinery.
[bibtex] [pdf] [doi]
[20]QCDCL with Cube Learning or Pure Literal Elimination - What is Best?
Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022 (Luc De Raedt, ed.), pages 1781–1787, 2022, ijcai.org.
Note: Distinguished Paper Award
[bibtex] [pdf] [doi]
[19]Should Decisions in QCDCL Follow Prefix Order?
Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff
25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Kuldeep S. Meel, Ofer Strichman, eds.), volume 236 of LIPIcs, pages 11:1–11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
2021
[18]Finding the Hardest Formulas for Resolution
Tomáš Peitl, Stefan Szeider
Journal of Artificial Intelligence Research, volume 72, pages 69–97, 2021.
Note: Conference Award Track, best paper CP 2020
[bibtex] [doi]
[17]Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths
Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl
Electron. Colloquium Comput. Complex., pages 135, 2021.
[bibtex] [pdf]
[16]Finding the Hardest Formulas for Resolution (Extended Abstract)
Tomáš Peitl, Stefan Szeider
Proceeding of IJCAI-21, the 30th International Joint Conference on Artificial Intelligence (Zhi-Hua Zhou, ed.), pages 4814–4818, 2021.
Note: Sister Conferences Best Papers
[bibtex] [doi]
[15]Davis and Putnam Meet Henkin: Solving DQBF with Resolution
Joshua Blinkhorn, Tomáš Peitl, Friedrich Slivovsky
Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Chu-Min Li, Felip Manyà, eds.), volume 12831 of Lecture Notes in Computer Science, pages 30–46, 2021, Springer Verlag.
[bibtex] [pdf] [doi]
2020
[14]Finding the Hardest Formulas for Resolution
Tomáš Peitl, Stefan Szeider
Proceedings of CP 2020, the 26th International Conference on Principles and Practice of Constraint Programming (Helmut Simonis, ed.), volume 12333 of Lecture Notes in Computer Science, pages 514–530, 2020, Springer Verlag.
Note: Best Paper Award
[bibtex] [pdf]
[13]Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
Robert Ganian, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 (Diego Calvanese, Esra Erdem, Michael Thielscher, eds.), pages 392–402, 2020.
[bibtex] [pdf]
[12]Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths
Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl
Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 394–411, 2020, Springer Verlag.
[bibtex] [pdf]
[11]Hard QBFs for Merge Resolution
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood
40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference) (Nitin Saxena, Sunil Simon, eds.), volume 182 of LIPIcs, pages 12:1–12:15, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
2019
[10]Dependency Learning for QBF
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Journal of Artificial Intelligence Research, volume 65, pages 180–208, 2019.
[bibtex] [pdf] [doi]
[9]Long-Distance Q-Resolution with Dependency Schemes
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Journal of Automated Reasoning, volume 63, number 1, pages 127–155, 2019.
[bibtex] [pdf] [doi]
[8]Proof Complexity of Fragments of Long-Distance Q-resolution
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2019, the 22nd International Conference on Theory and Applications of Satisfiability Testing, July 7–12, 2019, Lisbon, Portugal (Mikoláš Janota, Inês Lynce, eds.), volume 11628 of Lecture Notes in Computer Science, pages 319–335, 2019, Springer Verlag.
[bibtex] [pdf] [doi]
[7]Combining Resolution-Path Dependencies with Dependency Learning
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2019, the 22nd International Conference on Theory and Applications of Satisfiability Testing, July 7–12, 2019, Lisbon, Portugal (Mikoláš Janota, Inês Lynce, eds.), volume 11628 of Lecture Notes in Computer Science, pages 306–318, 2019, Springer Verlag.
[bibtex] [pdf] [doi]
2018
[6]Polynomial-Time Validation of QCDCL Certificates
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of SAT 2018, the 21st International Conference on Theory and Applications of Satisfiability Testing, Part of FLoC 2018, July 9–12, 2018, Oxford, UK (Olaf Beyersdorff, Christoph M. Wintersteiger, eds.), volume 10929 of Lecture Notes in Computer Science, pages 253–269, 2018, Springer Verlag.
[bibtex] [pdf] [doi]
[5]Portfolio-Based Algorithm Selection for Circuit QBFs
Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
QBF Workshop, 2018.
[bibtex]
[4]Portfolio-Based Algorithm Selection for Circuit QBFs
Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Proceedings of CP 2018, the 24rd International Conference on Principles and Practice of Constraint Programming (John N. Hooker, ed.), volume 11008 of Lecture Notes in Computer Science, pages 195–209, 2018, Springer Verlag.
[bibtex] [pdf] [doi]
[3]Portfolio Solvers for QDIMACS and QCIR
Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2018.
Note: QBF Evaluation at SAT
[bibtex]
2017
[2]Dependency learning for QBF
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings (Serge Gaspers, Toby Walsh, eds.), volume 10491 of Lecture Notes in Computer Science, pages 298–313, 2017, Springer Verlag.
[bibtex] [pdf] [doi]
2016
[1]Long Distance Q-Resolution with Dependency Schemes
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Nadia Creignou, Daniel Le Berre, eds.), volume 9710 of Lecture Notes in Computer Science, pages 500–518, 2016, Springer Verlag.
[bibtex] [pdf] [doi]
  • Doris Brazda
  • Maria Bresich
  • Jiehua Chen
  • Alexis de Colnet
  • Thomas Depian
  • Sara Di Bartolomeo
  • Alexander Dobler
  • Jan Dreier
  • Martin Durand
  • Simon Dominik Fink
  • Alexander Firbas
  • Robert Ganian
  • Christian Hatschka
  • Phuc Hung Hoang
  • Marc Huber
  • Enrico Iurlano
  • Liana Khazaliya
  • Markus Kirchweger
  • Viktoria Korchemna
  • Martin Kronegger
  • Fionn Aidan Mc Inerney
  • Martin Nöllenburg
  • Tomáš Peitl
  • Vaidyanathan P. R.
  • Günther Raidl
  • Franz Xaver Reichl
  • Mathis Rocton
  • Andre Schidler
  • Sofia Simola
  • Frank Sommer
  • Manuel Sorge
  • Johannes Strasser
  • Stefan Szeider
  • Laurenz Tomandl
  • Johannes Varga
  • Florentina Voboril
  • Markus Wallinger
  • Simon Wietheger
  • Hai Xia
  • Tianwei Zhang
TU Wien Informatics
Offenlegung (§25 MedienG) Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. – Disclaimer – Datenschutzerklärung
Log in requires cookies.