Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Olaf Beyersdorff:

TR20-005 | 17th January 2020
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege ... more >>>

TR19-057 | 6th April 2019
Olaf Beyersdorff, Joshua Blinkhorn

Proof Complexity of Symmetry Learning in QBF

For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs.

Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we ... more >>>

ISSN 1433-8092 | Imprint