Algorithms and Complexity Group
  • People
  • Research
  • Courses
  • Talks
  • Jobs
  • Contact

Friedrich Slivovsky

» Dipl.-Ing. Dr. techn.

Address:
Friedrich Slivovsky
Technische Universität Wien
Institute of Logic and Computation
Favoritenstraße 9–11, E192-01
1040 Wien
Austria

Email: fslivovsky@ac.tuwien.ac.at
Web: http://www.ac.tuwien.ac.at/people/fslivovsky/

2015-04-16-fslivovsky-IMG_4337

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.

40 results
2024
[40]eSLIM: Circuit Minimization with SAT Based Local Improvement
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
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 23:1–23:14, 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[bibtex] [doi]
[39]Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 7978–7986, 2024, AAAI Press.
[bibtex] [pdf] [doi]
2023
[38]Circuit Minimization with QBF-Based Exact Synthesis
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
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, Yiling Chen, Jennifer Neville, eds.), pages 4087–4094, 2023, AAAI Press.
[bibtex] [pdf] [doi]
[37]Circuit Minimization with Exact Synthesis: From QBF Back to SAT
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Proceedings of the 32nd International Workshop on Logic & Synthesis (IWLS), 2023.
[bibtex]
[36]Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF
Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak
Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2023.
[bibtex] [pdf] [doi]
2022
[35]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]
[34]Pedant: A Certifying DQBF Solver
Franz-Xaver Reichl, Friedrich Slivovsky
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 20:1–20:10, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
[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]
  • Doris Brazda
  • Maria Bresich
  • Jiehua Chen
  • Alexis de Colnet
  • Thomas Depian
  • Sara Di Bartolomeo
  • Alexander Dobler
  • Jan Dreier
  • Martin Durand
  • Simon Dominik Fink
  • Alexander Firbas
  • Robert Ganian
  • Christian Hatschka
  • Phuc Hung Hoang
  • Marc Huber
  • Enrico Iurlano
  • Liana Khazaliya
  • Markus Kirchweger
  • Viktoria Korchemna
  • Martin Kronegger
  • Fionn Aidan Mc Inerney
  • Martin Nöllenburg
  • Tomáš Peitl
  • Vaidyanathan P. R.
  • Günther Raidl
  • Franz Xaver Reichl
  • Mathis Rocton
  • Andre Schidler
  • Sofia Simola
  • Frank Sommer
  • Manuel Sorge
  • Johannes Strasser
  • Stefan Szeider
  • Laurenz Tomandl
  • Johannes Varga
  • Florentina Voboril
  • Markus Wallinger
  • Simon Wietheger
  • Hai Xia
  • Tianwei Zhang
TU Wien Informatics
Offenlegung (§25 MedienG) Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. – Disclaimer – Datenschutzerklärung
Log in requires cookies.