Friedrich Slivovsky

» Dipl.-Ing. Dr. techn.

Research interests

• Quantified Boolean Formulas (QBFs)
• Propositional Model Counting (#SAT)
• Knowledge Compilation

Software

• Qute: A dependency learning QBF solver (GitHub).
• Unique: A preprocessor for (D)QBF that computes unique Skolem and Herbrand functions (GitHub).
• Pedant: A certifying DQBF solver (GitHub).

Publications

See also my DBLP entry. My PhD thesis on QBF and #SAT is available here.

36 results

2023
[36]	Circuit Minimization with QBF-Based Exact Synthesis Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, 2023, AAAI Press. Note: to appear [bibtex]
[35]	Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF Johannes K. Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), 2023, Association for Computing Machinery. Note: to appear [bibtex]
2022
[34]	Sum-of-Products with Default Values: Algorithms and Complexity Results Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider Journal of Artificial Intelligence Research, volume 33, pages 535–552, 2022. [bibtex] [pdf]
[33]	Towards Uniform Certification in QBF Leroy Chew, Friedrich Slivovsky 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference) (Petra Berenbrink, Benjamin Monmege, eds.), volume 219 of LIPIcs, pages 22:1–22:23, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
2021
[32]	Certified DQBF Solving by Definition Extraction Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider 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 499–517, 2021, Springer Verlag. [bibtex] [pdf] [doi]
[31]	Proof Complexity of Symbolic QBF Reasoning Stefan Mengel, 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 399–416, 2021, Springer Verlag. [bibtex] [pdf] [doi]
[30]	Engineering an Efficient Boolean Functional Synthesis Engine Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel IEEE/ACM International Conference On Computer Aided Design, ICCAD 2021, Munich, Germany, November 1-4, 2021, pages 1–9, 2021, IEEE. [bibtex] [pdf] [doi]
[29]	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
[28]	A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth Friedrich Slivovsky, Stefan Szeider 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 267–276, 2020, Springer Verlag. [bibtex] [pdf]
[27]	Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing Friedrich Slivovsky Computer Aided Verification - 32nd International Conference, CAV 2020 (Shuvendu K. Lahiri, Chao Wang, eds.), volume 12224 of Lecture Notes in Computer Science, pages 508–528, 2020, Springer Verlag. [bibtex] [pdf]
[26]	Short Q-Resolution Proofs with Homomorphisms Ankit Shukla, Friedrich Slivovsky, Stefan Szeider 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 412–428, 2020, Springer Verlag. [bibtex] [pdf]
[25]	Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 429–446, 2020, Springer Verlag. [bibtex]
[24]	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]
2019
[23]	Dependency Learning for QBF Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider Journal of Artificial Intelligence Research, volume 65, pages 180–208, 2019. [bibtex] [pdf] [doi]
[22]	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]
[21]	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]
[20]	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
[19]	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]
[18]	Portfolio-Based Algorithm Selection for Circuit QBFs Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider QBF Workshop, 2018. [bibtex]
[17]	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]
[16]	Sum-of-Products with Default Values: Algorithms and Complexity Results Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider Proceedings of ICTAI 2018, the 30th IEEE International Conference on Tools with Artificial Intelligence (Lefteri H. Tsoukalas, Éric Grégoire, Miltiadis Alamaniotis, eds.), pages 733–737, 2018, IEEE. [bibtex] [pdf] [doi]
[15]	Portfolio Solvers for QDIMACS and QCIR Holger H. Hoos, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider 2018. Note: QBF Evaluation at SAT [bibtex]
2017
[14]	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
[13]	Quantifier reordering for QBF Friedrich Slivovsky, Stefan Szeider Journal of Automated Reasoning, volume 56, number 4, pages 459–477, 2016. [bibtex] [pdf] [doi]
[12]	Soundness of Q-resolution with dependency schemes Friedrich Slivovsky, Stefan Szeider Theoretical Computer Science, volume 612, pages 83–101, 2016. [bibtex] [pdf] [doi]
[11]	Model Counting for CNF Formulas of Bounded Modular Treewidth Daniël Paulusma, Friedrich Slivovsky, Stefan Szeider Algorithmica, volume 76, number 1, pages 168–194, 2016. [bibtex] [pdf] [doi]
[10]	Meta-Kernelization with Structural Parameters Robert Ganian, Friedrich Slivovsky, Stefan Szeider Journal of Computer and System Sciences, volume 82, number 2, pages 333–346, 2016. [bibtex] [pdf] [doi]
[9]	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]
[8]	Knowledge Compilation Meets Communication Complexity Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI), 9-15 July, 2016, New York, NY, USA, pages 1008–1014, 2016. [bibtex]
2015
[7]	On Compiling Structured CNFs to OBDDs Simone Bova, Friedrich Slivovsky Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, pages 80–93, 2015. [bibtex]
[6]	On Compiling CNFs into Structured Deterministic DNNFs Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, pages 199–214, 2015. [bibtex]
2014
[5]	Variable Dependencies and Q-Resolution Friedrich Slivovsky, Stefan Szeider Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Carsten Sinz, Uwe Egly, eds.), volume 8561 of Lecture Notes in Computer Science, pages 269–284, 2014, Springer Verlag. [bibtex] [doi]
2013
[4]	Model Counting for Formulas of Bounded Clique-Width Friedrich Slivovsky, Stefan Szeider Algorithms and Computation - 24th International Symposium, ISAAC 2013, Hong Kong, China, December 16-18, 2013, Proceedings (Leizhen Cai, Siu-Wing Cheng, Tak Wah Lam, eds.), volume 8283 of Lecture Notes in Computer Science, pages 677-687, 2013, Springer Verlag. [bibtex] [doi]
[3]	Model Counting for CNF Formulas of Bounded Modular Treewidth Daniël Paulusma, Friedrich Slivovsky, Stefan Szeider 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27 - March 2, 2013, Kiel, Germany (Natacha Portier, Thomas Wilke, eds.), volume 20 of LIPIcs, pages 55-66, 2013, Leibniz-Zentrum fuer Informatik. [bibtex] [doi]
[2]	Meta-kernelization with Structural Parameters Robert Ganian, Friedrich Slivovsky, Stefan Szeider Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings (Krishnendu Chatterjee, Jiri Sgall, eds.), volume 8087 of Lecture Notes in Computer Science, pages 457-468, 2013, Springer Verlag. [bibtex] [doi]
2012
[1]	Computing Resolution-Path Dependencies in Linear Time Friedrich Slivovsky, Stefan Szeider Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings (Alessandro Cimatti, Roberto Sebastiani, eds.), volume 7317 of Lecture Notes in Computer Science, pages 58-71, 2012, Springer Verlag. [bibtex] [doi]