Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR22-036 | 10th March 2022 14:38

Classes of Hard Formulas for QBF Resolution

RSS-Feed




TR22-036
Authors: Agnes Schleitzer, Olaf Beyersdorff
Publication: 10th March 2022 15:16
Downloads: 88
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint