Search Results

Documents authored by Kasche, Kaspar

Document
DOI: 10.4230/DagRep.14.10.22
SAT and Interactions (Dagstuhl Seminar 24421)

Authors: Olaf Beyersdorff, Laura Kovács, Meena Mahajan, Martina Seidl, and Kaspar Kasche

Published in: Dagstuhl Reports, Volume 14, Issue 10 (2025)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar "SAT and Interactions" (24421). The seminar brought together theoreticians and practitioners from the areas of proof complexity, SAT and QBF solving, and first-order theorem proving, who discussed recent developments in their fields and embarked on an interdisciplinary exchange of ideas and techniques between these neighbouring subfields of SAT.
Cite as

Olaf Beyersdorff, Laura Kovács, Meena Mahajan, Martina Seidl, and Kaspar Kasche. SAT and Interactions (Dagstuhl Seminar 24421). In Dagstuhl Reports, Volume 14, Issue 10, pp. 22-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.14.10.22,
  author =	{Beyersdorff, Olaf and Kov\'{a}cs, Laura and Mahajan, Meena and Seidl, Martina and Kasche, Kaspar},
  title =	{{SAT and Interactions (Dagstuhl Seminar 24421)}},
  pages =	{22--38},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{14},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Kov\'{a}cs, Laura and Mahajan, Meena and Seidl, Martina and Kasche, Kaspar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.10.22},
  URN =		{urn:nbn:de:0030-drops-230243},
  doi =		{10.4230/DagRep.14.10.22},
  annote =	{Keywords: SAT, QBF, proof complexity, solving, first-order logic, automated theorem proving}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.27
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree

Authors: Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.
Cite as

Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann. Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.MFCS.2024.27,
  author =	{Beyersdorff, Olaf and Hoffmann, Tim and Kasche, Kaspar and Spachmann, Luc Nicolas},
  title =	{{Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.27},
  URN =		{urn:nbn:de:0030-drops-205834},
  doi =		{10.4230/LIPIcs.MFCS.2024.27},
  annote =	{Keywords: proof complexity, QBF, polynomial calculus, circuits, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.5
The Relative Strength of #SAT Proof Systems

Authors: Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.
Cite as

Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2024.5,
  author =	{Beyersdorff, Olaf and Fichte, Johannes K. and Hecher, Markus and Hoffmann, Tim and Kasche, Kaspar},
  title =	{{The Relative Strength of #SAT Proof Systems}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.5},
  URN =		{urn:nbn:de:0030-drops-205276},
  doi =		{10.4230/LIPIcs.SAT.2024.5},
  annote =	{Keywords: Model Counting, #SAT, Proof Complexity, Proof Systems, Lower Bounds, Knowledge Compilation}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact