| ||||
| ||||
![]() Title:Classes of Hard Formulas for QBF Resolution Conference:SAT-22 Tags:lower bounds, proof complexity, QBF and resolution 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. Classes of Hard Formulas for QBF Resolution ![]() Classes of Hard Formulas for QBF Resolution | ||||
Copyright © 2002 – 2025 EasyChair |