Publications: Tomas Peitl
2026
| [1] | Graph Choosability via SAT: Beyond the Nullstellensatz Fortieth AAAI Conference on Artificial Intelligence, Thirty-Eighth Conference on Innovative Applications of Artificial Intelligence, Sixteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2026, Singapore, January 20-27, 2026 (Sven Koenig, Chad Jenkins, Matthew E. Taylor, eds.), pages 14269–14277, 2026, AAAI Press. |
| [2] | Smart Cubing for Graph Search: A Comparative Study 32nd International Conference on Principles and Practice of Constraint Programming, CP 2026, July 20–23, 2026, Lisbon, Portugal, volume 379 of LIPIcs, pages 33:1–33:19, 2026, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: Preprint: CoRR abs/2501.17201, https://arxiv.org/abs/2501.17201 |
| [3] | Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking 29th International Conference on Theory and Applications of Satisfiability Testing, SAT 2026, Lisbon, Portugal, July 20-23, 2026 (Alexey Ignatiev, Stefan Szeider, eds.), volume 377 of LIPIcs, pages 11:1–11:20, 2026, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
2025
| [1] | Better Extension Variables in DQBF via Independence 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025 (Jeremias Berg, Jakob Nordström, eds.), volume 341 of LIPIcs, pages 11:1–11:24, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [2] | Breaking Symmetries in Quantified Graph Search: A Comparative Study AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA (Toby Walsh, Julie Shah, Zico Kolter, eds.), pages 11246–11254, 2025, AAAI Press. |
2024
| [1] | Hard QBFs for Merge Resolution ACM Trans. Comput. Theory, volume 16, number 2, pages 6:1–6:24, 2024. |
| [2] | QCDCL with cube learning or pure literal elimination - What is best? Artif. Intell., volume 336, pages 104194, 2024. |
| [3] | Should Decisions in QCDCL Follow Prefix Order? J. Autom. Reason., volume 68, number 1, pages 5, 2024. |
| [4] | Small unsatisfiable k-CNFs with bounded literal occurrence 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. |
2023
| [1] | Are Hitting Formulas Hard for Resolution? Discr. Appl. Math., volume 337, pages 173–184, 2023. |
| [2] | A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture 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. |
| [3] | Co-Certificate Learning with SAT Modulo Symmetries 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 |
2022
| [1] | Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution ACM Transactions on Computational Logic, sep 2022, Association for Computing Machinery. |
| [2] | QCDCL with Cube Learning or Pure Literal Elimination - What is Best? 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 |
| [3] | Should Decisions in QCDCL Follow Prefix Order? 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. |
2021
| [1] | Finding the Hardest Formulas for Resolution Journal of Artificial Intelligence Research, volume 72, pages 69–97, 2021. Note: Conference Award Track, best paper CP 2020 |
| [2] | Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths Electron. Colloquium Comput. Complex., pages 135, 2021. |
| [3] | Davis and Putnam Meet Henkin: Solving DQBF with Resolution 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. |
| [4] | Finding the Hardest Formulas for Resolution (Extended Abstract) 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 |
| [5] | Davis and Putnam Meet Henkin: Solving DQBF with Resolution 2021, Technical report AC-TR-21-012, Algorithms and Complexity Group, TU Wien. |
2020
| [1] | Finding the Hardest Formulas for Resolution 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 |
| [2] | Fixed-Parameter Tractability of Dependency QBF with Structural Parameters 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. |
| [3] | Hard QBFs for Merge Resolution 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. |
| [4] | Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths 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. |
| [5] | Finding the Hardest Formulas for Resolution 2020, Technical report AC-TR-20-008, Algorithms and Complexity Group, TU Wien. |
| [6] | Fixed-Parameter Tractability of Dependency QBF with Structural Parameters 2020, Technical report AC-TR-20-011, Algorithms and Complexity Group, TU Wien. |
2019
| [1] | Dependency Learning for QBF Journal of Artificial Intelligence Research, volume 65, pages 180–208, 2019. |
| [2] | Long-Distance Q-Resolution with Dependency Schemes Journal of Automated Reasoning, volume 63, number 1, pages 127–155, 2019. |
| [3] | Combining Resolution-Path Dependencies with Dependency Learning 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. |
| [4] | Proof Complexity of Fragments of Long-Distance Q-resolution 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. |
| [5] | Combining Resolution-Path Dependencies with Dependency Learning 2019, Technical report AC-TR-19-005, Algorithms and Complexity Group, TU Wien. |
| [6] | Proof Complexity of Fragments of Long-Distance Q-resolution 2019, Technical report AC-TR-19-004, Algorithms and Complexity Group, TU Wien. |
2018
| [1] | Polynomial-Time Validation of QCDCL Certificates 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. |
| [2] | Portfolio-Based Algorithm Selection for Circuit QBFs 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. |
| [3] | Portfolio-Based Algorithm Selection for Circuit QBFs QBF Workshop, 2018. |
| [4] | Polynomial-Time Validation of QCDCL Certificates 2018, Technical report AC-TR-18-003, Algorithms and Complexity Group, TU Wien. |
| [5] | Portfolio Solvers for QDIMACS and QCIR 2018. Note: QBF Evaluation at SAT |
| [6] | Portfolio-Based Algorithm Selection for Circuit QBFs 2018, Technical report AC-TR-18-004, Algorithms and Complexity Group, TU Wien. |
| [7] | QBF Encodings of Chess Problems 2018, Technical report AC-TR-18-013, Algorithms and Complexity Group, TU Wien. |
2017
| [1] | Long-Distance Q-Resolution with Dependency Schemes 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. |
| [2] | Dependency Learning for QBF 2017, Technical report AC-TR-17-011, Algorithms and Complexity Group, TU Wien. |
2016
| [1] | Long Distance Q-Resolution with Dependency Schemes 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. |
AC Admin
Website maintainer