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 Nov 2021 I'm a postdoc back here in the AC group, funded by the return phase of my FWF Erwin Schrödinger Fellowship.
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

QBF solver Qute ,which implements QCDCL with dependency learning and the reflexive resolution-path dependency scheme D^rrs.
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

25 results

2024
[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] [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 The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy (Meena Mahajan, Friedrich Slivovsky, eds.), 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex]
[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]