Search Results

Documents authored by Chakraborty, Supratik

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}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SAT.2024
LIPIcs, Volume 305, SAT 2024, Complete Volume

Authors: Supratik Chakraborty and Jie-Hong Roland Jiang

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

Abstract
LIPIcs, Volume 305, SAT 2024, Complete Volume
Cite as

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1-578, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{chakraborty_et_al:LIPIcs.SAT.2024,
  title =	{{LIPIcs, Volume 305, SAT 2024, Complete Volume}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{1--578},
  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},
  URN =		{urn:nbn:de:0030-drops-205211},
  doi =		{10.4230/LIPIcs.SAT.2024},
  annote =	{Keywords: LIPIcs, Volume 305, SAT 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SAT.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Supratik Chakraborty and Jie-Hong Roland Jiang

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.SAT.2024.0,
  author =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{0:i--0:xviii},
  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.0},
  URN =		{urn:nbn:de:0030-drops-205222},
  doi =		{10.4230/LIPIcs.SAT.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.30
On Synthesizing Computable Skolem Functions for First Order Logic

Authors: Supratik Chakraborty and S. Akshay

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).
Cite as

Supratik Chakraborty and S. Akshay. On Synthesizing Computable Skolem Functions for First Order Logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.MFCS.2022.30,
  author =	{Chakraborty, Supratik and Akshay, S.},
  title =	{{On Synthesizing Computable Skolem Functions for First Order Logic}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.30},
  URN =		{urn:nbn:de:0030-drops-168285},
  doi =		{10.4230/LIPIcs.MFCS.2022.30},
  annote =	{Keywords: Skolem functions, Automated, Synthesis, First order logic, Computability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.40
On Petri Nets with Hierarchical Special Arcs

Authors: S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy of places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of the above four problems for all combinations of hierarchy, inhibitor, reset and transfer arcs, except the termination problem for two combinations. For both these combinations, we show that deciding termination is as hard as deciding the positivity problem on linear recurrence sequences -- a long-standing open problem.
Cite as

S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep. On Petri Nets with Hierarchical Special Arcs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.40,
  author =	{Akshay, S. and Chakraborty, Supratik and Das, Ankush and Jagannath, Vishal and Sandeep, Sai},
  title =	{{On Petri Nets with Hierarchical Special Arcs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{40:1--40:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.40},
  URN =		{urn:nbn:de:0030-drops-78026},
  doi =		{10.4230/LIPIcs.CONCUR.2017.40},
  annote =	{Keywords: Petri Nets, Hierarchy, Reachability, Coverability, Termination, Positivity}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2011
LIPIcs, Volume 13, FSTTCS'11, Complete Volume

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
LIPIcs, Volume 13, FSTTCS'11, Complete Volume
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011,
  title =	{{LIPIcs, Volume 13, FSTTCS'11, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011},
  URN =		{urn:nbn:de:0030-drops-41077},
  doi =		{10.4230/LIPIcs.FSTTCS.2011},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems Specifying and Verifying and Reasoning about Programs}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2011.i
Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. i-xv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011.i,
  author =	{Chakraborty, Supratik and Kumar, Amit},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{i--xv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.i},
  URN =		{urn:nbn:de:0030-drops-33196},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.xvi
Author Index

Authors: Supratik Chakraborty and Amit Kumar

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
Author Index
Cite as

Supratik Chakraborty and Amit Kumar. Author Index. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 16-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.FSTTCS.2011.xvi,
  author =	{Chakraborty, Supratik and Kumar, Amit},
  title =	{{Author Index}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{16--17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.xvi},
  URN =		{urn:nbn:de:0030-drops-33636},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.xvi},
  annote =	{Keywords: Author Index}
}
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