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
, ,
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
, , ,
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
, ,
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
, ,
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
, , , ,
LICS, pages 1–14, 2023.
[bibtex] [pdf] [doi]
2022
[35]Sum-of-Products with Default Values: Algorithms and Complexity Results
, , ,
Journal of Artificial Intelligence Research, volume 33, pages 535–552, 2022.
[bibtex] [pdf]
[34]Pedant: A Certifying DQBF Solver
,
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
,
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
, ,
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
,
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
, , ,
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
, ,
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
,
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

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
, ,
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
, , ,
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
, , ,
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
, ,
Journal of Artificial Intelligence Research, volume 65, pages 180–208, 2019.
[bibtex] [pdf] [doi]
[22]Long-Distance Q-Resolution with Dependency Schemes
, ,
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
, ,
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
, ,
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
, ,
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
, , ,
QBF Workshop, 2018.
[bibtex]
[17]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.
[bibtex] [pdf] [doi]
[16]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, Éric Grégoire, Miltiadis Alamaniotis, eds.), pages 733–737, 2018, IEEE.
[bibtex] [pdf] [doi]
[15]Portfolio Solvers for QDIMACS and QCIR
, , ,
2018.
Note: QBF Evaluation at SAT
[bibtex]
2017
[14]Dependency learning for QBF
, ,
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
,
Journal of Automated Reasoning, volume 56, number 4, pages 459–477, 2016.
[bibtex] [pdf] [doi]
[12]Soundness of Q-resolution with dependency schemes
,
Theoretical Computer Science, volume 612, pages 83–101, 2016.
[bibtex] [pdf] [doi]
[11]Model Counting for CNF Formulas of Bounded Modular Treewidth
, ,
Algorithmica, volume 76, number 1, pages 168–194, 2016.
[bibtex] [pdf] [doi]
[10]Meta-Kernelization with Structural Parameters
, ,
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
, ,
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
, , ,
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
,
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
, , ,
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
,
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
,
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
, ,
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
, ,
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
,
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]