Skip to main content
What types of page to search?

Popular pages: Undergraduate Postgraduate PhD Accommodation Research International students

Alternatively use our A-Z index.

Dr Friedrich Slivovsky


Trustworthy Computing
Part of
School of Computer Science and Informatics
Faculty of Science and Engineering

Contact

F.Slivovsky@liverpool.ac.uk

Research outputs

What type of research output do you want to show?

2026

Model Counting for Dependency Quantified Boolean Formulas

Fung, L. -H., Cheng, C., Jiang, J. -H. R., Slivovsky, F., & Tan, T. (2026). Model Counting for Dependency Quantified Boolean Formulas. In Proceedings of the AAAI Conference on Artificial Intelligence Vol. 40 (pp. 14234-14242). Association for the Advancement of Artificial Intelligence (AAAI). doi:10.1609/aaai.v40i17.38437

DOI
10.1609/aaai.v40i17.38437
Conference Paper

2025

2024

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

Chew, L., De Colnet, A., Slivovsky, F., & Szeider, S. (2024). Hardness of Random Reordered Encodings of Parity for Resolution and CDCL. In Proceedings of the AAAI Conference on Artificial Intelligence Vol. 38 (pp. 7978-7986). Association for the Advancement of Artificial Intelligence (AAAI). doi:10.1609/aaai.v38i8.28635

DOI
10.1609/aaai.v38i8.28635
Conference Paper

TOWARDS UNIFORM CERTIFICATION IN QBF

Chew, L., & Slivovsky, F. (2024). TOWARDS UNIFORM CERTIFICATION IN QBF. LOGICAL METHODS IN COMPUTER SCIENCE, 20(1). doi:10.46298/LMCS-20(1:14)2024

DOI
10.46298/LMCS-20(1:14)2024
Journal article

2023

Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF

Fichte, J. K., Ganian, R., Hecher, M., Slivovsky, F., & Ordyniak, S. (2023). Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. In 2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS. doi:10.1109/LICS56636.2023.10175675

DOI
10.1109/LICS56636.2023.10175675
Conference Paper

Circuit Minimization with QBF-Based Exact Synthesis

Reichl, F. -X., Slivovsky, F., & Szeider, S. (2023). Circuit Minimization with QBF-Based Exact Synthesis. THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 4, 4087-4094. Retrieved from https://www.webofscience.com/

Journal article

2022

Sum-of-Products with Default Values: Algorithms and Complexity Results

Ganian, R., Kim, E. J., Slivovsky, F., & Szeider, S. (2022). Sum-of-Products with Default Values: Algorithms and Complexity Results. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 73, 535-552. Retrieved from https://www.webofscience.com/

Journal article

Towards Uniform Certification in QBF

Chew, L., & Slivovsky, F. (2022). Towards Uniform Certification in QBF. In 39TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE, STACS 2022 Vol. 219. doi:10.4230/LIPIcs.STACS.2022.22

DOI
10.4230/LIPIcs.STACS.2022.22
Conference Paper

2021

Engineering an Efficient Boolean Functional Synthesis Engine

Golia, P., Slivovsky, F., Roy, S., & Meel, K. S. (2021). Engineering an Efficient Boolean Functional Synthesis Engine. In 2021 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN (ICCAD). doi:10.1109/ICCAD51958.2021.9643583

DOI
10.1109/ICCAD51958.2021.9643583
Conference Paper

Certified DQBF Solving by Definition Extraction

Reichl, F. -X., Slivovsky, F., & Szeider, S. (2021). Certified DQBF Solving by Definition Extraction. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 Vol. 12831 (pp. 499-517). doi:10.1007/978-3-030-80223-3_34

DOI
10.1007/978-3-030-80223-3_34
Conference Paper

Davis and Putnam Meet Henkin: Solving DQBF with Resolution

Blinkhorn, J., Peitl, T., & Slivovsky, F. (2021). Davis and Putnam Meet Henkin: Solving DQBF with Resolution. In Unknown Book (Vol. 12831, pp. 30-46). doi:10.1007/978-3-030-80223-3_4

DOI
10.1007/978-3-030-80223-3_4
Chapter

Proof Complexity of Symbolic QBF Reasoning

Mengel, S., & Slivovsky, F. (2021). Proof Complexity of Symbolic QBF Reasoning. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 Vol. 12831 (pp. 399-416). doi:10.1007/978-3-030-80223-3_28

DOI
10.1007/978-3-030-80223-3_28
Conference Paper

2020

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters

Ganian, R., Peitl, T., Slivovsky, F., & Szeider, S. (2020). Fixed-Parameter Tractability of Dependency QBF with Structural Parameters. In KR2020: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING (pp. 392-402). Retrieved from https://www.webofscience.com/

Conference Paper

A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth

Slivovsky, F., & Szeider, S. (2020). A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2020 Vol. 12178 (pp. 267-276). doi:10.1007/978-3-030-51825-7_19

DOI
10.1007/978-3-030-51825-7_19
Conference Paper

Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing

Slivovsky, F. (2020). Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing. In COMPUTER AIDED VERIFICATION (CAV 2020), PT I Vol. 12224 (pp. 508-528). doi:10.1007/978-3-030-53288-8_24

DOI
10.1007/978-3-030-53288-8_24
Conference Paper

Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness

Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2020 Vol. 12178 (pp. 429-446). doi:10.1007/978-3-030-51825-7_30

DOI
10.1007/978-3-030-51825-7_30
Conference Paper

Short Q-Resolution Proofs with Homomorphisms

Shukla, A., Slivovsky, F., & Szeider, S. (2020). Short Q-Resolution Proofs with Homomorphisms. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2020 Vol. 12178 (pp. 412-428). doi:10.1007/978-3-030-51825-7_29

DOI
10.1007/978-3-030-51825-7_29
Conference Paper

2019

Qute in the QBF Evaluation 2018

Peitl, T., Slivovsky, F., & Szeider, S. (2019). Qute in the QBF Evaluation 2018. Journal on Satisfiability, Boolean Modeling and Computation, 11(1), 261-272. doi:10.3233/sat190124

DOI
10.3233/sat190124
Journal article

Combining Resolution-Path Dependencies with Dependency Learning

Peitl, T., Slivovsky, F., & Szeider, S. (2019). Combining Resolution-Path Dependencies with Dependency Learning. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2019 Vol. 11628 (pp. 306-318). doi:10.1007/978-3-030-24258-9_22

DOI
10.1007/978-3-030-24258-9_22
Conference Paper

Dependency Learning for QBF

Peitl, T., Slivovsky, F., & Szeider, S. (2019). Dependency Learning for QBF. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 65, 181-208. doi:10.1613/jair.1.11529

DOI
10.1613/jair.1.11529
Journal article

Long-Distance Q-Resolution with Dependency Schemes

Peitl, T., Slivovsky, F., & Szeider, S. (2019). Long-Distance Q-Resolution with Dependency Schemes. JOURNAL OF AUTOMATED REASONING, 63(1), 127-155. doi:10.1007/s10817-018-9467-3

DOI
10.1007/s10817-018-9467-3
Journal article

Proof Complexity of Fragments of Long-Distance Q-Resolution

Peitl, T., Slivovsky, F., & Szeider, S. (2019). Proof Complexity of Fragments of Long-Distance Q-Resolution. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2019 Vol. 11628 (pp. 319-335). doi:10.1007/978-3-030-24258-9_23

DOI
10.1007/978-3-030-24258-9_23
Conference Paper

2018

Sum-of-Products with Default Values: Algorithms and Complexity Results

Ganian, R., Kim, E. J., Slivovsky, F., & Szeider, S. (2018). Sum-of-Products with Default Values: Algorithms and Complexity Results. In 2018 IEEE 30TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI) (pp. 733-737). doi:10.1109/ICTAI.2018.00115

DOI
10.1109/ICTAI.2018.00115
Conference Paper

Polynomial-Time Validation of QCDCL Certificates

Peitl, T., Slivovsky, F., & Szeider, S. (2018). Polynomial-Time Validation of QCDCL Certificates. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018 Vol. 10929 (pp. 253-269). doi:10.1007/978-3-319-94144-8_16

DOI
10.1007/978-3-319-94144-8_16
Conference Paper

Portfolio-Based Algorithm Selection for Circuit QBFs

Hoos, H. H., Peitl, T., Slivovsky, F., & Szeider, S. (2018). Portfolio-Based Algorithm Selection for Circuit QBFs. In PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING Vol. 11008 (pp. 195-209). doi:10.1007/978-3-319-98334-9_13

DOI
10.1007/978-3-319-98334-9_13
Conference Paper

2017

Dependency Learning for QBF

Peitl, T., Slivovsky, F., & Szeider, S. (2017). Dependency Learning for QBF. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING (SAT 2017) Vol. 10491 (pp. 298-313). doi:10.1007/978-3-319-66263-3_19

DOI
10.1007/978-3-319-66263-3_19
Conference Paper

On Compiling Structured CNFs to OBDDs

Bova, S., & Slivovsky, F. (2017). On Compiling Structured CNFs to OBDDs. THEORY OF COMPUTING SYSTEMS, 61(2), 637-655. doi:10.1007/s00224-016-9715-z

DOI
10.1007/s00224-016-9715-z
Journal article

2016

Model Counting for CNF Formulas of Bounded Modular Treewidth

Paulusma, D., Slivovsky, F., & Szeider, S. (2016). Model Counting for CNF Formulas of Bounded Modular Treewidth. ALGORITHMICA, 76(1), 168-194. doi:10.1007/s00453-015-0030-x

DOI
10.1007/s00453-015-0030-x
Journal article

Quantifier Reordering for QBF

Slivovsky, F., & Szeider, S. (2016). Quantifier Reordering for QBF. JOURNAL OF AUTOMATED REASONING, 56(4), 459-477. doi:10.1007/s10817-015-9353-1

DOI
10.1007/s10817-015-9353-1
Journal article

Meta-kernelization with structural parameters

Ganian, R., Slivovsky, F., & Szeider, S. (2016). Meta-kernelization with structural parameters. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 82(2), 333-346. doi:10.1016/j.jcss.2015.08.003

DOI
10.1016/j.jcss.2015.08.003
Journal article

Long Distance Q-Resolution with Dependency Schemes

Peitl, T., Slivovsky, F., & Szeider, S. (2016). Long Distance Q-Resolution with Dependency Schemes. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016 Vol. 9710 (pp. 500-518). doi:10.1007/978-3-319-40970-2_31

DOI
10.1007/978-3-319-40970-2_31
Conference Paper

Soundness of Q-resolution with dependency schemes

Slivovsky, F., & Szeider, S. (2016). Soundness of Q-resolution with dependency schemes. THEORETICAL COMPUTER SCIENCE, 612, 83-101. doi:10.1016/j.tcs.2015.10.020

DOI
10.1016/j.tcs.2015.10.020
Journal article

2015

On Compiling CNFs into Structured Deterministic DNNFs

Bova, S., Capelli, F., Mengel, S., & Slivovsky, F. (2015). On Compiling CNFs into Structured Deterministic DNNFs. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015 Vol. 9340 (pp. 199-214). doi:10.1007/978-3-319-24318-4_15

DOI
10.1007/978-3-319-24318-4_15
Conference Paper

2014

Variable Dependencies and Q-Resolution

Slivovsky, F., & Szeider, S. (2014). Variable Dependencies and Q-Resolution. In THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2014 Vol. 8561 (pp. 269-284). Retrieved from https://www.webofscience.com/

Conference Paper

2013

Meta-kernelization with Structural Parameters

Ganian, R., Slivovsky, F., & Szeider, S. (2013). Meta-kernelization with Structural Parameters. In MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013 Vol. 8087 (pp. 457-468). Retrieved from https://www.webofscience.com/

Conference Paper

Model Counting for Formulas of Bounded Clique-Width

Slivovsky, F., & Szeider, S. (2013). Model Counting for Formulas of Bounded Clique-Width. In ALGORITHMS AND COMPUTATION Vol. 8283 (pp. 677-687). Retrieved from https://www.webofscience.com/

Conference Paper