Friedrich Slivovsky

Recent Publications

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy and Sriraam Natarajan), pages 7978-7986, 2024, AAAI Press.
Improved Circuit Minimization with Exact Synthesis
2024, Technical report AC-TR-24-001, Algorithms and Complexity Group, TU Wien.
Circuit Minimization with QBF-Based Exact Synthesis
Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023 (Brian Williams and Yiling Chen and Jennifer Neville), pages 4087-4094, 2023, AAAI Press.
Certified DQBF Solving by Definition Extraction
2021, Technical report AC-TR-21-010, Algorithms and Complexity Group, TU Wien.
Davis and Putnam Meet Henkin: Solving DQBF with Resolution
2021, Technical report AC-TR-21-012, Algorithms and Complexity Group, TU Wien.
Proof Complexity of Symbolic QBF Reasoning
2021, Technical report AC-TR-21-011, Algorithms and Complexity Group, TU Wien.
A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
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 267-276, 2020, Springer Verlag.
Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
Computer Aided Verification - 32nd International Conference, CAV 2020 (Shuvendu K. Lahiri and Chao Wang), volume 12224 of Lecture Notes in Computer Science, pages 508-528, 2020, Springer Verlag.
Short Q-Resolution Proofs with Homomorphisms
2020, Technical report AC-TR-20-007, Algorithms and Complexity Group, TU Wien.
Short Q-Resolution Proofs with Homomorphisms
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 412-428, 2020, Springer Verlag.
Combining Resolution-Path Dependencies with Dependency Learning
2019, Technical report AC-TR-19-005, Algorithms and Complexity Group, TU Wien.
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 and Inês Lynce), volume 11628 of Lecture Notes in Computer Science, pages 306-318, 2019, Springer Verlag.
Dependency Learning for QBF
Journal of Artificial Intelligence Research, volume 65, pages 180-208, 2019.
Long-Distance Q-Resolution with Dependency Schemes
Journal of Automated Reasoning, volume 63, number 1, pages 127-155, 2019.
Proof Complexity of Fragments of Long-Distance Q-resolution
2019, Technical report AC-TR-19-004, Algorithms and Complexity Group, TU Wien.
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 and Inês Lynce), volume 11628 of Lecture Notes in Computer Science, pages 319-335, 2019, Springer Verlag.
Polynomial-Time Validation of QCDCL Certificates
2018, Technical report AC-TR-18-003, Algorithms and Complexity Group, TU Wien.
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 and Christoph M. Wintersteiger), volume 10929 of Lecture Notes in Computer Science, pages 253-269, 2018, Springer Verlag.
Portfolio-Based Algorithm Selection for Circuit QBFs
2018, Technical report AC-TR-18-004, Algorithms and Complexity Group, TU Wien.
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), volume 11008 of Lecture Notes in Computer Science, pages 195-209, 2018, Springer Verlag.
Sum-of-Products with Default Values: Algorithms and Complexity Results
Proceedings of ICTAI 2018, the 30th IEEE International Conference on Tools with Artificial Intelligence (Lefteri H. Tsoukalas and Éric Grégoire and Miltiadis Alamaniotis), pages 733-737, 2018, IEEE.
Dependency Learning for QBF
2017, Technical report AC-TR-17-011, Algorithms and Complexity Group, TU Wien.
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 and Toby Walsh), volume 10491 of Lecture Notes in Computer Science, pages 298-313, 2017, Springer Verlag.
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 and Daniel Le Berre), volume 9710 of Lecture Notes in Computer Science, pages 500-518, 2016, Springer Verlag.
Meta-Kernelization with Structural Parameters
Journal of Computer and System Sciences, volume 82, number 2, pages 333-346, 2016.
Computing Resolution-Path Dependencies in Linear Time
Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings (Alessandro Cimatti and Roberto Sebastiani), volume 7317 of Lecture Notes in Computer Science, pages 58-71, 2012, Springer Verlag.