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

Room: HB0418 (how to get there)
Phone: +43(1)58801–192128
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).

Publications

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

26 results
2020
[26]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]
[25]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]
[24]Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
, , ,
Principles of Knowledge Representation and Reasoning: Proceedings of the Seventeenth International Conference, KR 2020, pages 1898–1904, 2020.
Note: to appear
[bibtex] [pdf]
2019
[23]Dependency Learning for QBF
, ,
Journal 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]