Publications: Tomas Peitl

2026

Graph Choosability via SAT: Beyond the Nullstellensatz
Markus Kirchweger, Tomás Peitl, David Seka, Stefan Szeider
The 40th Annual AAAI Conference on Artificial Intelligence, AAAI-2026, 2026.
Note: To appear
[details]

2025

Better Extension Variables in DQBF via Independence
Leroy Chew and Tomás Peitl
28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025 (Jeremias Berg and Jakob Nordström), volume 341 of LIPIcs, pages 11:1-11:24, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[pdf] [doi] [details]

2024

Hard QBFs for Merge Resolution
Olaf Beyersdorff and Joshua Blinkhorn and Meena Mahajan and Tomáš Peitl and Gaurav Sood
ACM Trans. Comput. Theory, volume 16, number 2, pages 6:1-6:24, 2024.
[pdf] [doi] [details]

QCDCL with cube learning or pure literal elimination - What is best?
Benjamin Böhm and Tomáš Peitl and Olaf Beyersdorff
Artif. Intell., volume 336, pages 104194, 2024.
[pdf] [doi] [details]

Should Decisions in QCDCL Follow Prefix Order?
Benjamin Böhm and Tomáš Peitl and Olaf Beyersdorff
J. Autom. Reason., volume 68, number 1, pages 5, 2024.
[pdf] [doi] [details]

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) (Chakraborty, Supratik and Jiang, Jie-Hong Roland), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:22, 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[doi] [details]

2023

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
[pdf] [doi] [details]

2022

Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
Beyersdorff, Olaf, Blinkhorn, Joshua, Mahajan, Meena, Peitl, Tomáš
ACM Transactions on Computational Logic, sep 2022, Association for Computing Machinery.
[doi] [details]

Should Decisions in QCDCL Follow Prefix Order?
Benjamin Böhm and Tomáš Peitl and Olaf Beyersdorff
25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Kuldeep S. Meel and Ofer Strichman), volume 236 of LIPIcs, pages 11:1-11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[pdf] [doi] [details]

QCDCL with Cube Learning or Pure Literal Elimination - What is Best?
Benjamin Böhm and Tomáš Peitl and Olaf Beyersdorff
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022 (Luc De Raedt), pages 1781-1787, 2022, ijcai.org.
Note: Distinguished Paper Award
[pdf] [doi] [details]

2021

Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths
Olaf Beyersdorff and Joshua Blinkhorn and Tomáš Peitl
Electron. Colloquium Comput. Complex., pages 135, 2021.
[pdf] [details]

Davis and Putnam Meet Henkin: Solving DQBF with Resolution
Joshua Blinkhorn, Tomáš Peitl, Friedrich Slivovsky
2021, Technical report AC-TR-21-012, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

Davis and Putnam Meet Henkin: Solving DQBF with Resolution
Joshua Blinkhorn and Tomáš Peitl and Friedrich Slivovsky
Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings (Chu-Min Li and Felip Manyà), volume 12831 of Lecture Notes in Computer Science, pages 30-46, 2021, Springer.
[pdf] [doi] [details]

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
[doi] [details]

2020

Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths
Olaf Beyersdorff and Joshua Blinkhorn and Tomáš Peitl
Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina and Martina Seidl), volume 12178 of Lecture Notes in Computer Science, pages 394-411, 2020, Springer Verlag.
[pdf] [details]

Hard QBFs for Merge Resolution
Olaf Beyersdorff and Joshua Blinkhorn and Meena Mahajan and Tomáš Peitl and 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 and Sunil Simon), volume 182 of LIPIcs, pages 12:1-12:15, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[pdf] [doi] [details]

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
Robert Ganian, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2020, Technical report AC-TR-20-011, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

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), volume 12333 of Lecture Notes in Computer Science, pages 514-530, 2020, Springer Verlag.
Note: Best Paper Award
[details]

Finding the Hardest Formulas for Resolution
Tomáš Peitl, Stefan Szeider
2020, Technical report AC-TR-20-008, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

2019

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.
[pdf] [doi] [details]

Dependency Learning for QBF
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Journal of Artificial Intelligence Research, volume 65, pages 180-208, 2019.
[pdf] [doi] [details]

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 and Inês Lynce), volume 11628 of Lecture Notes in Computer Science, pages 306-318, 2019, Springer Verlag.
[doi] [details]

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 and Inês Lynce), volume 11628 of Lecture Notes in Computer Science, pages 319-335, 2019, Springer Verlag.
[doi] [details]

Proof Complexity of Fragments of Long-Distance Q-resolution
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2019, Technical report AC-TR-19-004, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

Combining Resolution-Path Dependencies with Dependency Learning
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2019, Technical report AC-TR-19-005, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

2018

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), volume 11008 of Lecture Notes in Computer Science, pages 195-209, 2018, Springer Verlag.
[doi] [details]

Portfolio-Based Algorithm Selection for Circuit QBFs
Hoos, Holger H., Peitl, Tomáš, Slivovsky, Friedrich, Szeider, Stefan
QBF Workshop, 2018.
[details]

Portfolio Solvers for QDIMACS and QCIR
Hoos, Holger H., Peitl, Tomáš and Slivovsky, Friedrich, Szeider, Stefan
2018.
Note: QBF Evaluation at SAT
[details]

Portfolio-Based Algorithm Selection for Circuit QBFs
Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2018, Technical report AC-TR-18-004, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

QBF Encodings of Chess Problems
Tomáš Peitl
2018, Technical report AC-TR-18-013, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

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 and Christoph M. Wintersteiger), volume 10929 of Lecture Notes in Computer Science, pages 253-269, 2018, Springer Verlag.
[pdf] [doi] [details]

Polynomial-Time Validation of QCDCL Certificates
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2018, Technical report AC-TR-18-003, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

2017

Long-Distance Q-Resolution with Dependency Schemes
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 and Toby Walsh), volume 10491 of Lecture Notes in Computer Science, pages 298-313, 2017, Springer Verlag.
[pdf] [doi] [details]

Dependency Learning for QBF
Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
2017, Technical report AC-TR-17-011, Algorithms and Complexity Group, TU Wien.
[pdf] [details]

2016

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 and Daniel Le Berre), volume 9710 of Lecture Notes in Computer Science, pages 500-518, 2016, Springer Verlag.
[pdf] [doi] [details]