Revision #1 Authors: Olaf Beyersdorff, Agnes Schleitzer

Accepted on: 30th May 2022 06:43

Downloads: 161

Keywords:

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

TR22-036 Authors: Agnes Schleitzer, Olaf Beyersdorff

Publication: 10th March 2022 15:16

Downloads: 403

Keywords:

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.