publications

2024

  1. Towards Uniform Certification in QBF
    Leroy Chew and Friedrich Slivovsky
    Log. Methods Comput. Sci., 2024
  2. Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
    Leroy Chew, Alexis Colnet, Friedrich Slivovsky, and Stefan Szeider
    In AAAI 2024 , 2024
  3. eSLIM: Circuit Minimization with SAT Based Local Improvement
    Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2024 , 2024
  4. Strategy Extraction by Interpolation
    Friedrich Slivovsky
    In SAT 2024 , 2024

2023

  1. Circuit Minimization with QBF-Based Exact Synthesis
    Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider
    In AAAI 2023 , 2023
  2. Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF
    Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, and Sebastian Ordyniak
    In LICS 2023 , 2023

2022

  1. Sum-of-Products with Default Values: Algorithms and Complexity Results
    Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, and Stefan Szeider
    JAIR, 2022
  2. Pedant: A Certifying DQBF Solver
    Franz-Xaver Reichl and Friedrich Slivovsky
    In SAT 2022 , 2022
  3. Quantified CDCL with Universal Resolution
    Friedrich Slivovsky
    In SAT 2022 , 2022
  4. Towards Uniform Certification in QBF
    Leroy Chew and Friedrich Slivovsky
    In STACS 2023 , 2022

2021

  1. Engineering an Efficient Boolean Functional Synthesis Engine
    Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, and Kuldeep S. Meel
    In ICCAD 2021 , 2021
  2. Davis and Putnam Meet Henkin: Solving DQBF with Resolution
    Joshua Blinkhorn, Tomás Peitl, and Friedrich Slivovsky
    In SAT 2021 , 2021
  3. Proof Complexity of Symbolic QBF Reasoning
    Stefan Mengel and Friedrich Slivovsky
    In SAT 2021 , 2021
  4. Certified DQBF Solving by Definition Extraction
    Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2021 , 2021

2020

  1. Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
    Friedrich Slivovsky
    In CAV 2020 , 2020
  2. Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
    Robert Ganian, Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In KR 2020 , 2020
  3. A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
    Friedrich Slivovsky and Stefan Szeider
    In SAT 2020 , 2020
  4. Short Q-Resolution Proofs with Homomorphisms
    Ankit Shukla, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2020 , 2020
  5. Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
    Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, and Florian Zuleger
    In SAT 2020 , 2020

2019

  1. Dependency Learning for QBF
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    JAIR, 2019
  2. Long-Distance Q-Resolution with Dependency Schemes
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    Journal of Automated Reasoning, 2019
  3. Qute in the QBF Evaluation 2018
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    J. Satisf. Boolean Model. Comput., 2019
  4. Combining Resolution-Path Dependencies with Dependency Learning
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2019 , 2019
  5. Proof Complexity of Fragments of Long-Distance Q-Resolution
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2019 , 2019

2018

  1. Portfolio-Based Algorithm Selection for Circuit QBFs
    Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In CP 2018 , 2018
  2. Sum-of-Products with Default Values: Algorithms and Complexity Results
    Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, and Stefan Szeider
    In ICTAI 2018 , 2018
  3. Polynomial-Time Validation of QCDCL Certificates
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2018 , 2018

2017

  1. On Compiling Structured CNFs to OBDDs
    Simone Bova and Friedrich Slivovsky
    Theory Comput. Syst., 2017
  2. Dependency Learning for QBF
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2017 , 2017

2016

  1. Model Counting for CNF Formulas of Bounded Modular Treewidth
    Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider
    Algorithmica, 2016
  2. Quantifier Reordering for QBF
    Friedrich Slivovsky and Stefan Szeider
    Journal of Automated Reasoning, 2016
  3. Meta-kernelization with structural parameters
    Robert Ganian, Friedrich Slivovsky, and Stefan Szeider
    JCSS, 2016
  4. Soundness of Q-resolution with dependency schemes
    Friedrich Slivovsky and Stefan Szeider
    Theoretical Computer Science, 2016
  5. Knowledge Compilation Meets Communication Complexity
    Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky
    In IJCAI 2016 , 2016
  6. Long Distance Q-Resolution with Dependency Schemes
    Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider
    In SAT 2016 , 2016

2015

  1. On Compiling Structured CNFs to OBDDs
    Simone Bova and Friedrich Slivovsky
    In CSR 2015 , 2015
  2. On Compiling CNFs into Structured Deterministic DNNFs
    Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky
    In SAT 2015 , 2015

2014

  1. Variable Dependencies and Q-Resolution
    Friedrich Slivovsky and Stefan Szeider
    In SAT 2014 , 2014

2013

  1. Model Counting for Formulas of Bounded Clique-Width
    Friedrich Slivovsky and Stefan Szeider
    In ISAAC 2013 , 2013
  2. Meta-kernelization with Structural Parameters
    Robert Ganian, Friedrich Slivovsky, and Stefan Szeider
    In MFCS 2013 , 2013
  3. Model Counting for CNF Formulas of Bounded Modular Treewidth
    Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider
    In STACS 2013 , 2013

2012

  1. Computing Resolution-Path Dependencies in Linear Time ,
    Friedrich Slivovsky and Stefan Szeider
    In SAT 2012 , 2012