Search Results

Documents authored by Kasche, Lea

Document
DOI: 10.4230/LIPIcs.SAT.2026.3
Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions

Authors: S. Akshay, Olaf Beyersdorff, Supratik Chakraborty, Lea Kasche, Meena Mahajan, and Luc Nicolas Spachmann

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.
Cite as

S. Akshay, Olaf Beyersdorff, Supratik Chakraborty, Lea Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.SAT.2026.3,
  author =	{Akshay, S. and Beyersdorff, Olaf and Chakraborty, Supratik and Kasche, Lea and Mahajan, Meena and Spachmann, Luc Nicolas},
  title =	{{Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.3},
  URN =		{urn:nbn:de:0030-drops-263096},
  doi =		{10.4230/LIPIcs.SAT.2026.3},
  annote =	{Keywords: Quantified Boolean Formulas, Skolem and Herbrand functions, Automated synthesis, Knowledge compilation, Proof systems and complexity}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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