Friedrich Slivovsky

Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

2022

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

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2022

Quantified CDCL with Universal Resolution.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

Pedant: A Certifying DQBF Solver.

[BibT_eX]

[DOI]

Franz-Xaver Reichl

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

2021

Towards Uniform Certification in QBF.

[BibT_eX]

[DOI]

Leroy Chew

Electron. Colloquium Comput. Complex., 2021

Certified DQBF Solving by Definition Extraction.

[BibT_eX]

[DOI]

Franz-Xaver Reichl

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Proof Complexity of Symbolic QBF Reasoning.

[BibT_eX]

[DOI]

Stefan Mengel

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Davis and Putnam Meet Henkin: Solving DQBF with Resolution.

[BibT_eX]

[DOI]

Joshua Blinkhorn

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Engineering an Efficient Boolean Functional Synthesis Engine.

[BibT_eX]

[DOI]

Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2021

2020

A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Short Q-Resolution Proofs with Homomorphisms.

[BibT_eX]

[DOI]

Ankit Shukla

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

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

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

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

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Qute in the QBF Evaluation 2018.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2019

Long-Distance Q-Resolution with Dependency Schemes.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Dependency Learning for QBF.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2019

Proof Complexity of Fragments of Long-Distance Q-Resolution.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Combining Resolution-Path Dependencies with Dependency Learning.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

2018

Polynomial-Time Validation of QCDCL Certificates.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Portfolio-Based Algorithm Selection for Circuit QBFs.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2018

2017

On Compiling Structured CNFs to OBDDs.

[BibT_eX]

[DOI]

Simone Bova

Theory Comput. Syst., 2017

2016

Soundness of Q-resolution with dependency schemes.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2016

Meta-kernelization with structural parameters.

[BibT_eX]

[DOI]

Robert Ganian

J. Comput. Syst. Sci., 2016

Quantifier Reordering for QBF.

[BibT_eX]

[DOI]

J. Autom. Reason., 2016

Model Counting for CNF Formulas of Bounded Modular Treewidth.

[BibT_eX]

[DOI]

Daniël Paulusma

Algorithmica, 2016

Knowledge Compilation Meets Communication Complexity.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

2015

On Compiling CNFs into Structured Deterministic DNNFs.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

2014

Expander CNFs have Exponential DNNF Size.

[BibT_eX]

[DOI]

CoRR, 2014

Variable Dependencies and Q-Resolution.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

2013

Model Counting for Formulas of Bounded Clique-Width.

[BibT_eX]

[DOI]

Proceedings of the Algorithms and Computation - 24th International Symposium, 2013

2012

Computing Resolution-Path Dependencies in Linear Time , .

[BibT_eX]

[DOI]