Classes of Hard Formulas for QBF Resolution

EasyChair Preprint no. 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: lower bounds, proof complexity, QBF, resolution

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

  year = {EasyChair, 2022}}