Skip to main content

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

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