To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q and QU, and only one specific QBF family to separate Q and QU.

Here we provide a general method to construct hard formulas for Q and QU. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Sigma_2^b formulas without constant winning strategies).
This leads to a host of new hard formulas, including new classes of hard random QBFs.

We further present generic constructions for formulas separating Q and QU, and for separating Q and LDQ.

Corrected Definition of LDQ-Res

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q and QU, and only one specific QBF family to separate Q and QU.

Here we provide a general method to construct hard formulas for Q and QU. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Sigma_2^b formulas without constant winning strategies).
This leads to a host of new hard formulas, including new classes of hard random QBFs.

We further present generic constructions for formulas separating Q and QU, and for separating Q and LDQ.