Friedrich Slivovsky

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 42

Top Topics

Knowledge Compilation

Top Venues

J. Artif. Intell. Res.

J. Autom. Reason.

Publications

Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL. AAAI (2024)
Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL. CoRR (2024)
Leroy Chew, Friedrich Slivovsky
Towards Uniform Certification in QBF. Log. Methods Comput. Sci. 20 (1) (2024)
Friedrich Slivovsky
Strategy Extraction by Interpolation. SAT (2024)
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
eSLIM: Circuit Minimization with SAT Based Local Improvement. SAT (2024)
Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. LICS (2023)
Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. CoRR (2023)
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Circuit Minimization with QBF-Based Exact Synthesis. AAAI (2023)
Leroy Chew, Friedrich Slivovsky
Towards Uniform Certification in QBF. CoRR (2022)
Leroy Chew, Friedrich Slivovsky
Towards Uniform Certification in QBF. STACS (2022)
Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider
Sum-of-Products with Default Values: Algorithms and Complexity Results. J. Artif. Intell. Res. 73 (2022)
Franz-Xaver Reichl, Friedrich Slivovsky
Pedant: A Certifying DQBF Solver. SAT (2022)
Friedrich Slivovsky
Quantified CDCL with Universal Resolution. SAT (2022)
Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel
Engineering an Efficient Boolean Functional Synthesis Engine. CoRR (2021)
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Certified DQBF Solving by Definition Extraction. SAT (2021)
Stefan Mengel, Friedrich Slivovsky
Proof Complexity of Symbolic QBF Reasoning. SAT (2021)
Stefan Mengel, Friedrich Slivovsky
Proof Complexity of Symbolic QBF Reasoning. CoRR (2021)
Leroy Chew, Friedrich Slivovsky
Towards Uniform Certification in QBF. Electron. Colloquium Comput. Complex. 28 (2021)
Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel
Engineering an Efficient Boolean Functional Synthesis Engine. ICCAD (2021)
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Certified DQBF Solving by Definition Extraction. CoRR (2021)
Joshua Blinkhorn, Tomás Peitl, Friedrich Slivovsky
Davis and Putnam Meet Henkin: Solving DQBF with Resolution. SAT (2021)
Friedrich Slivovsky, Stefan Szeider
A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth. SAT (2020)
Ankit Shukla, Friedrich Slivovsky, Stefan Szeider
Short Q-Resolution Proofs with Homomorphisms. SAT (2020)
Robert Ganian, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Fixed-Parameter Tractability of Dependency QBF with Structural Parameters. KR (2020)
Friedrich Slivovsky
Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing. CAV (1) (2020)
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. SAT (2020)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Combining Resolution-Path Dependencies with Dependency Learning. SAT (2019)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Long-Distance Q-Resolution with Dependency Schemes. J. Autom. Reason. 63 (1) (2019)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Qute in the QBF Evaluation 2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Proof Complexity of Fragments of Long-Distance Q-Resolution. SAT (2019)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Dependency Learning for QBF. J. Artif. Intell. Res. 65 (2019)
Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Portfolio-Based Algorithm Selection for Circuit QBFs. CP (2018)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Polynomial-Time Validation of QCDCL Certificates. SAT (2018)
Robert Ganian, Eun Jung Kim, Friedrich Slivovsky, Stefan Szeider
Sum-of-Products with Default Values: Algorithms and Complexity Results. ICTAI (2018)
Simone Bova, Friedrich Slivovsky
On Compiling Structured CNFs to OBDDs. Theory Comput. Syst. 61 (2) (2017)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Dependency Learning for QBF. SAT (2017)
Friedrich Slivovsky, Stefan Szeider
Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612 (2016)
Daniël Paulusma, Friedrich Slivovsky, Stefan Szeider
Model Counting for CNF Formulas of Bounded Modular Treewidth. Algorithmica 76 (1) (2016)
Robert Ganian, Friedrich Slivovsky, Stefan Szeider
Meta-kernelization with structural parameters. J. Comput. Syst. Sci. 82 (2) (2016)
Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky
Knowledge Compilation Meets Communication Complexity. IJCAI (2016)
Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
Long Distance Q-Resolution with Dependency Schemes. SAT (2016)
Friedrich Slivovsky, Stefan Szeider
Quantifier Reordering for QBF. J. Autom. Reason. 56 (4) (2016)
Simone Bova, Friedrich Slivovsky
On Compiling Structured CNFs to OBDDs. CSR (2015)
Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky
On Compiling CNFs into Structured Deterministic DNNFs. SAT (2015)
Friedrich Slivovsky, Stefan Szeider
Model Counting for Formulas of Bounded Clique-Width. CoRR (2014)
Friedrich Slivovsky, Stefan Szeider
Variable Dependencies and Q-Resolution. SAT (2014)
Simone Bova, Friedrich Slivovsky
On Compiling Structured CNFs to OBDDs. CoRR (2014)
Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky
Expander CNFs have Exponential DNNF Size. CoRR (2014)
Friedrich Slivovsky, Stefan Szeider
Model Counting for Formulas of Bounded Clique-Width. ISAAC (2013)
Robert Ganian, Friedrich Slivovsky, Stefan Szeider
Meta-kernelization with Structural Parameters. MFCS (2013)
Robert Ganian, Friedrich Slivovsky, Stefan Szeider
Meta-Kernelization with Structural Parameters CoRR (2013)
Daniël Paulusma, Friedrich Slivovsky, Stefan Szeider
Model Counting for CNF Formulas of Bounded Modular Treewidth. STACS (2013)
Friedrich Slivovsky, Stefan Szeider
Computing Resolution-Path Dependencies in Linear Time CoRR (2012)
Friedrich Slivovsky, Stefan Szeider
Computing Resolution-Path Dependencies in Linear Time , . SAT (2012)