DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.22

Definition-Based Dependency Schemes

Authors: David Kattermann, Clemens Hofstadler, and Martina Seidl

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

Abstract

A variable in a quantified Boolean formula (QBFs) is defined, if its value is uniquely determined by some other variables. Such definitions are widely exploited in various techniques for QBF solving. In this work, we formalize the concept of using definitions for reducing variable dependencies by introducing a novel dependency scheme and investigate its proof-theoretic impact. Our analysis shows that a definition-based dependency scheme is able to detect independencies other established dependency schemes cannot and that this can lead to exponentially shorter refutations. We further demonstrate that our scheme can be combined with any other scheme and that such a combined use can exponentially outperform using either scheme alone. Moreover, we study the dynamic application of our definition-based dependency scheme, which leads to another exponential speedup compared to the static application. Finally, we analyze the computational complexity of our dependency scheme and introduce a family of tractable variants.

Cite as

David Kattermann, Clemens Hofstadler, and Martina Seidl. Definition-Based Dependency Schemes. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kattermann_et_al:LIPIcs.SAT.2026.22,
  author =	{Kattermann, David and Hofstadler, Clemens and Seidl, Martina},
  title =	{{Definition-Based Dependency Schemes}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{22:1--22:18},
  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.22},
  URN =		{urn:nbn:de:0030-drops-263285},
  doi =		{10.4230/LIPIcs.SAT.2026.22},
  annote =	{Keywords: Quantified Boolean formulas, Dependency schemes, Proof calculi}
}

Search Results

Documents authored by Kattermann, David

Definition-Based Dependency Schemes

Abstract

Cite as

Thanks for your feedback!

Could not send message