Accepted Papers
- Martin Kronegger, Andreas Pfandler and Reinhard Pichler: Conformant Planning as a Benchmark for QBF-Solvers (slides)
- Uwe Egly and Magdalena Widl: Solution extraction from long-distance resolution proofs (slides)
- Mikolas Janota and Joao Marques-Silva: forall-Exp+Res Does not P-Simulate Q-resolution (slides)
- Friedrich Slivovsky and Stefan Szeider: Variable Dependencies and Q-Resolution (slides)
- William Klieber, Mikolas Janota, Joao Marques-Silva and Edmund Clarke: Extending DPLL-Based QBF Solvers to Handle Free Variables (slides)
- Allen Van Gelder: Certificate Extraction from Variable Elimination QBF Preprocessors (slides)
- Charles Jordan and Lukasz Kaiser: Benchmarks from Reduction Finding (slides)
- Florian Lonsing, Martina Seidl, Allen Van Gelder: Report on the QBF Gallery 2013 (slides)
Schedule
The workshop takes place on Tuesday July 9 from 09:00 to 12:30.
Length of presentations: max. 15 minutes.
Last update: June 13 2013.
Session 1 (09:00 - 10:30): QBF Solving
- Florian Lonsing, Martina Seidl: welcome address
- Mikolas Janota and Joao Marques-Silva: forall-Exp+Res Does not P-Simulate Q-resolution
- Friedrich Slivovsky and Stefan Szeider: Variable Dependencies and Q-Resolution
- Uwe Egly and Magdalena Widl: Solution extraction from long-distance resolution proofs
- William Klieber, Mikolas Janota, Joao Marques-Silva and Edmund Clarke: Extending DPLL-Based QBF Solvers to Handle Free Variables
- Allen Van Gelder: Certificate Extraction from Variable Elimination QBF Preprocessors
Coffee Break 10:30 - 11:00
Session 2 (11:00 - 12:30): QBF Encodings and QBF Gallery 2013
- Martin Kronegger, Andreas Pfandler and Reinhard Pichler: Conformant Planning as a Benchmark for QBF-Solvers
- Charles Jordan and Lukasz Kaiser: Benchmarks from Reduction Finding
- Allen Van Gelder, Florian Lonsing, Martina Seidl: The QBF Gallery 2013
- Discussions