1 Search Results for "Schleitzer, Agnes"

Document
DOI: 10.4230/LIPIcs.SAT.2022.5
Classes of Hard Formulas for QBF Resolution

Authors: Agnes Schleitzer and Olaf Beyersdorff

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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 (Σ₂^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 LD-Q-Res.
Cite as

Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schleitzer_et_al:LIPIcs.SAT.2022.5,
  author =	{Schleitzer, Agnes and Beyersdorff, Olaf},
  title =	{{Classes of Hard Formulas for QBF Resolution}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.5},
  URN =		{urn:nbn:de:0030-drops-166792},
  doi =		{10.4230/LIPIcs.SAT.2022.5},
  annote =	{Keywords: QBF, proof complexity, resolution, separations}
}
  • Refine by Author
  • 1 Beyersdorff, Olaf
  • 1 Schleitzer, Agnes

  • Refine by Classification
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 1 QBF
  • 1 proof complexity
  • 1 resolution
  • 1 separations

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact