Classes of Hard Formulas for QBF Resolution

EasyChair Preprint 8633

Abstract

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res. Here we provide a general method to construct hard formulas for Q-Res and QU-Res. 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-Res and QU-Res, and for separating Q-Res and long-distance-Q-Res.

Keyphrases: QBF, lower bounds, proof complexity, resolution

@booklet{EasyChair:8633,
  author    = {Agnes Schleitzer and Olaf Beyersdorff},
  title     = {Classes of Hard Formulas for QBF Resolution},
  howpublished = {EasyChair Preprint 8633},
  year      = {EasyChair, 2022}}