Talks
Below you find a list of talks I gave at various conferences and workshops. Sets of slides in PDF are available for download.
In reverse chronological ordering:
- Evaluating QBF Solvers: Quantifier Alternations Matter, CP'2018, Lille, France.
- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property, CiE 2018, Kiel, Germany; slightly extended version of IJCAR 2018 talk; related paper at IJCAR 2018.
- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property, IJCAR 2018, part of FLoC, Oxford, UK.
- Submissions to QBFEVAL'18, QBF Workshop 2018, affiliated to SAT 2018, part of FLoC, Oxford, UK.
- An Introduction to QBF Solving, The Second Indian SAT+SMT School, Mysuru, India.
- Evaluating QBF Solvers: Quantifier Alternations Matter, AVM'2017, Visegrad, Hungary.
- DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL , CADE'2017, Gothenburg, Sweden.
- Parallel QBF Solving: State of the Art Techniques and Future Perspectives , PCR'2017, Gothenburg, Sweden.
- An Overview of QBF Reasoning Techniques, SAT and Interactions, Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik.
- Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges, IJCAI-16, New York City, USA.
- Q-Resolution with Generalized Axioms, SAT'2016, Bordeaux, France.
- Submissions to QBFEVAL'16, QBF'2016, Bordeaux, France.
- Advances in QBF Reasoning, SAT/SMT/AR Summer School 2016, Lisbon, Portugal.
- Automated Benchmarking of Incremental SAT and QBF Solvers, LPAR 2015, Suva, Fiji.
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination, LPAR 2015, Suva, Fiji.
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. PUMA/RiSE Workshop 2015, Bad Griesbach, Germany.
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API, SAT'2015, Austin, Texas, USA.
- Conformant Planning as a Case Study of Incremental QBF Solving, AISC 2014, Sevilla, Spain.
- Incremental QBF Solving, CP 2014, Lyon, France.
- Incremental QBF Solving by DepQBF, ICMS 2014, Seoul, South Korea.
- MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing, SAT'2014, Vienna, Austria.
- Incremental QBF Solving, AVM'2014, Frejus, France.
- Inside Search-Based QBF Solvers and DepQBF in Practice, at the ReRiSE'14 Winter School, Johannes Kepler University, Linz, Austria.
- Search-based QBF Solving: Basics, Recent Trends and Challenges. JST ERATO Minato Discrete Strucure Manipulation System Project Seminar, Hokkaido University, Sapporo, Japan. October 2013.
- The QBF Gallery 2013, SAT'13, Helsinki, Finnland.
- The QBF Gallery 2013, QBF Workshop 2013, Helsinki, Finnland.
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation, SAT'13, Helsinki, Finnland.
- QBF Certificates: Challenges and Future Research Directions. PUMA/RiSE Workshop 2012, Goldegg, Salzburg, Austria.
- Blocked Clause Elimination for QBF, CADE'11, Wroclaw, Poland
- Failed Literal Detection for QBF, SAT'11, Ann Arbor, Michigan, USA.
- Preprocessing QBF: Failed Literals and Quantified Blocked Clause Elimination , Deduction at Scale Seminar, Ringberg Castle, Tegernsee, Germany.
- Practical Aspects of Dependency Schemes in QBF Solving, AVM'10, Lugano, Switzerland
- Integrating Dependency Schemes in Search-Based QBF Solvers (Talk) (Poster), SAT'10, Edinburgh, Scotland, UK
- DepQBF: A Dependency-Aware QBF Solver (System Description), POS'10, Edinburgh, Scotland, UK.
- A Compact Representation for Syntactic Dependencies in QBFs, SAT'09, Swansea, Wales, UK.
- Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, MEMICS'08, Znojmo, Czech Republic
- Nenofex: Expanding NNF for QBF Solving, SAT'08, Guangzhou, P. R. China.