Publications: Tomas Peitl

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
📄 Details

Better Extension Variables in DQBF via Independence Leroy Chew, Tomás Peitl. 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025
📄 Details

Hard QBFs for Merge Resolution Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood. ACM Trans. Comput. Theory
📄 Details
QCDCL with cube learning or pure literal elimination - What is best? Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff. Artif. Intell.
📄 Details
Should Decisions in QCDCL Follow Prefix Order? Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff. J. Autom. Reason.
📄 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)
📄 Details

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
📄 Details

Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution Beyersdorff, Olaf, Blinkhorn, Joshua, Mahajan, Meena, Peitl, Tomáš. ACM Transactions on Computational Logic
📄 Details
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
📄 Details
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
📄 Details

Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl. Electron. Colloquium Comput. Complex.
📄 Details
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
📄 Details
Finding the Hardest Formulas for Resolution Tomáš Peitl, Stefan Szeider. Journal of Artificial Intelligence Research
📄 Details

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
📄 Details
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)
📄 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
📄 Details

Long-Distance Q-Resolution with Dependency Schemes Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider. Journal of Automated Reasoning
📄 Details
Dependency Learning for QBF Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider. Journal of Artificial Intelligence Research
📄 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
📄 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
📄 Details

Portfolio-Based Algorithm Selection for Circuit QBFs Hoos, Holger H., Peitl, Tomáš, Slivovsky, Friedrich, Szeider, Stefan. Proceedings of CP 2018, the 24rd International Conference on Principles and Practice of Constraint Programming
📄 Details
Portfolio Solvers for QDIMACS and QCIR Hoos, Holger H., Peitl, Tomáš, Slivovsky, Friedrich, Szeider, Stefan.
📄 Details
QBF Encodings of Chess Problems Tomáš Peitl.
📄 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
📄 Details

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
📄 Details
Long-Distance Q-Resolution with Dependency Schemes Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider.
📄 Details

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
📄 Details