All reports by Author Joshua Blinkhorn:

__
TR20-112
| 8th June 2020
__

Joshua Blinkhorn#### Simulating DQBF Preprocessing Techniques with Resolution Asymmetric Tautologies

__
TR20-036
| 9th March 2020
__

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl#### Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths

__
TR20-005
| 17th January 2020
__

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan#### Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

Revisions: 1

__
TR19-057
| 6th April 2019
__

Olaf Beyersdorff, Joshua Blinkhorn#### Proof Complexity of Symmetry Learning in QBF

__
TR18-172
| 11th October 2018
__

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan#### Building Strategies into QBF Proofs

__
TR17-137
| 11th September 2017
__

Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde#### Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

__
TR17-032
| 17th February 2017
__

Olaf Beyersdorff, Joshua Blinkhorn#### Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds

__
TR16-028
| 29th February 2016
__

Olaf Beyersdorff, Joshua Blinkhorn#### Dependency Schemes in QBF Calculi:Semantics and Soundness

Revisions: 1

Joshua Blinkhorn

Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

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 >>>

Olaf Beyersdorff, Joshua Blinkhorn

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 >>>

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver's answer resp. establish soundness of the system. So far ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde

As a natural extension of the SAT problem, different proof systems for quantified Boolean formulas (QBF) have been proposed. Many of these extend a propositional system to handle universal quantifiers.

By formalising the construction of the QBF proof system from a propositional proof system, by the addition of the ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn

We devise a new technique to prove lower bounds for the proof size in resolution-type calculi for quantified Boolean formulas (QBF). The new technique applies to the strong expansion system IR-calc and thereby also to the most studied QBF system Q-Resolution.

Our technique exploits a clear semantic paradigm, showing the ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn

We study the parametrization of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use ... more >>>