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}
}

Artifact

Software

DOI: 10.4230/artifacts.23376

TalisMan

Authors: Clemens Hofstadler and Daniela Kaufmann

Abstract

Cite as

Clemens Hofstadler, Daniela Kaufmann. TalisMan (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23376,
   title = {{TalisMan}}, 
   author = {Hofstadler, Clemens and Kaufmann, Daniela},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20;origin=https://github.com/d-kfmnn/talisman;visit=swh:1:snp:d83634ac4675c6c2a76a146bbea12568e3c642a1;anchor=swh:1:rev:be8187df3d18d3530bd175136d6865269cbc21e2}{\texttt{swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20}} (visited on 2025-08-08)},
   url = {https://github.com/d-kfmnn/talisman/tree/be8187d},
   doi = {10.4230/artifacts.23376},
}

Document

DOI: 10.4230/LIPIcs.CP.2025.14

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification

Authors: Clemens Hofstadler and Daniela Kaufmann

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract

Formal verification of arithmetic circuits using computer algebra has been shown to be highly successful. The circuit is encoded as a system of polynomials, which automatically generates a lexicographic Gröbner basis. Correctness is then verified by computing the polynomial remainder of the specification. To optimize the remainder computation, prior work extracts linear polynomials. However, this required recomputing a Gröbner basis with respect to a degree-compatible order. In this paper, we show that this computationally expensive step is unnecessary and propose a novel hybrid verification approach that combines an FGLM-style linearization technique with a guess-and-prove method using SAT solving to derive the linear relations directly from lexicographic Gröbner bases. We enhance our approach using caching techniques and propagating vanishing monomials. Our experimental results demonstrate that our method significantly outperforms previous linearization techniques.

Cite as

Clemens Hofstadler and Daniela Kaufmann. Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hofstadler_et_al:LIPIcs.CP.2025.14,
  author =	{Hofstadler, Clemens and Kaufmann, Daniela},
  title =	{{Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{14:1--14:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.14},
  URN =		{urn:nbn:de:0030-drops-238752},
  doi =		{10.4230/LIPIcs.CP.2025.14},
  annote =	{Keywords: Computer Algebra, FGLM, And-Inverter Graphs, Hardware Verification}
}

Search Results

Documents authored by Hofstadler, Clemens

Definition-Based Dependency Schemes

Abstract

Cite as

TalisMan

Abstract

Cite as

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message