| Publication | Date of Publication | Type |
|---|
| Structure-aware lower bounds and broadening the horizon of tractability for QBF | 2026-02-27 | Paper |
| Strategy extraction by interpolation | 2026-02-03 | Paper |
| ESLIM: Circuit minimization with SAT based local improvement | 2026-02-03 | Paper |
| Pedant: a certifying DQBF solver | 2024-07-12 | Paper |
| Quantified CDCL with universal resolution | 2024-07-12 | Paper |
| Towards uniform certification in QBF | 2024-04-23 | Paper |
Towards Uniform Certification in QBF
Logical Methods in Computer Science | 2024-03-11 | Paper |
| Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF | 2023-04-26 | Paper |
Sum-of-Products with Default Values: Algorithms and Complexity Results
Journal of Artificial Intelligence Research | 2022-05-16 | Paper |
Proof complexity of symbolic QBF reasoning
(available as arXiv preprint) | 2022-03-22 | Paper |
| Davis and Putnam meet Henkin: solving DQBF with resolution | 2022-03-22 | Paper |
Certified DQBF solving by definition extraction
(available as arXiv preprint) | 2022-03-22 | Paper |
| Multi-linear strategy extraction for QBF expansion proofs via local soundness | 2021-04-07 | Paper |
| Short Q-resolution proofs with homomorphisms | 2021-04-07 | Paper |
| A faster algorithm for propositional model counting parameterized by incidence treewidth | 2021-04-07 | Paper |
| Interpolation-based semantic gate extraction and its applications to QBF preprocessing | 2021-02-04 | Paper |
| Proof complexity of fragments of long-distance Q-resolution | 2020-05-20 | Paper |
| Combining resolution-path dependencies with dependency learning | 2020-05-20 | Paper |
Dependency Learning for QBF
Journal of Artificial Intelligence Research | 2019-07-12 | Paper |
Long-distance Q-resolution with dependency schemes
Journal of Automated Reasoning | 2019-05-31 | Paper |
| Polynomial-time validation of QCDCL certificates | 2018-08-10 | Paper |
| Dependency learning for QBF | 2017-11-15 | Paper |
On compiling structured CNFs to OBDDs
Theory of Computing Systems | 2017-10-20 | Paper |
| Model counting for CNF formulas of bounded modular treewidth | 2017-01-30 | Paper |
Model counting for CNF formulas of bounded modular treewidth
Algorithmica | 2016-11-01 | Paper |
Long distance Q-resolution with dependency schemes
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Quantifier reordering for QBF
Journal of Automated Reasoning | 2016-05-26 | Paper |
Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
Theoretical Computer Science | 2015-12-15 | Paper |
Meta-kernelization with structural parameters
Journal of Computer and System Sciences | 2015-12-11 | Paper |
On compiling CNFs into structured deterministic DNNFs
Lecture Notes in Computer Science | 2015-11-20 | Paper |
On compiling structured CNFs to OBDDs
Lecture Notes in Computer Science | 2015-10-20 | Paper |
Variable dependencies and Q-resolution
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Model counting for formulas of bounded clique-width
Algorithms and Computation | 2014-01-14 | Paper |
Meta-kernelization with structural parameters
Mathematical Foundations of Computer Science 2013 | 2013-09-20 | Paper |
Computing Resolution-Path Dependencies in Linear Time ,
Theory and Applications of Satisfiability Testing – SAT 2012 | 2013-08-12 | Paper |
| Making it more explicit | 2013-04-24 | Paper |
