Search Results

Documents authored by Shukla, Anil

Document
DOI: 10.4230/LIPIcs.FSTTCS.2024.18
Circuits, Proofs and Propositional Model Counting

Authors: Sravanthi Chede, Leroy Chew, and Anil Shukla

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

Abstract
In this paper we present a new proof system framework CLIP (Circuit Linear Induction Proposition) for propositional model counting (#SAT). A CLIP proof firstly involves a Boolean circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit. This concept is remarkably simple and CLIP is modular so it allows us to use existing checking formats from propositional logic, especially strong proof systems. CLIP has polynomial-size proofs for XOR-pairs which are known to require exponential-size proofs in MICE [Fichte et al., 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in Beyersdorff et al. [Olaf Beyersdorff et al., 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Florent Capelli, 2019], CPOG [Bryant et al., 2023], MICE). Furthermore, CLIP has a theoretical advantage over the other #SAT proof systems in the sense that CLIP only has lower bounds from its propositional proof system or if 𝖯^#𝖯 is not contained in P/poly, which is a major open problem in circuit complexity. CLIP uses unrestricted circuits in its proof as compared to restricted structures used by the existing #SAT proof systems. In this way, CLIP avoids hardness or limitations due to circuit restrictions.
Cite as

Sravanthi Chede, Leroy Chew, and Anil Shukla. Circuits, Proofs and Propositional Model Counting. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chede_et_al:LIPIcs.FSTTCS.2024.18,
  author =	{Chede, Sravanthi and Chew, Leroy and Shukla, Anil},
  title =	{{Circuits, Proofs and Propositional Model Counting}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{18:1--18:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.18},
  URN =		{urn:nbn:de:0030-drops-222079},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.18},
  annote =	{Keywords: Propositional model counting, Boolean circuits, #SAT, Proof Systems, Certified Partition Operation Graph (CPOG)}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.21
Extending Merge Resolution to a Family of QBF-Proof Systems

Authors: Sravanthi Chede and Anil Shukla

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
Merge Resolution (MRes [Olaf Beyersdorff et al., 2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player (countermodels) within the proofs as merge maps. Merge maps are deterministic branching programs in which isomorphism checking is efficient, as a result MRes is a polynomial time verifiable proof system. In this paper, we introduce a family of proof systems MRes-ℛ in which the information of countermodels are stored in any pre-fixed complete representation ℛ. Hence, corresponding to each possible complete representation ℛ, we have a sound and refutationally complete QBF-proof system in MRes-ℛ. To handle these arbitrary representations, we introduce consistency checking rules in MRes-ℛ instead of the isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable (Non-P). Consequently, the paper shows that using merge maps is too restrictive and with a slight change in rules, it can be replaced with arbitrary representations leading to several interesting proof systems. We relate these new systems with the implicit proof system from the algorithm in [Joshua Blinkhorn et al., 2021], which was designed to solve DQBFs (Dependency QBFs) using clause-strategy pairs like MRes. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in [Joshua Blinkhorn et al., 2021] and deduce that "Ordered" versions of the proof systems in MRes-ℛ are indeed polynomial time verifiable. On the lower bound side, we lift the lower bound result of regular MRes ([Olaf Beyersdorff et al., 2020]) by showing that the completion principle formulas (CR_n) from [Mikolás Janota and João Marques-Silva, 2015] which are shown to be hard for regular MRes in [Olaf Beyersdorff et al., 2020], are also hard for any regular proof system in MRes-ℛ. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use various complete representations, including those undiscovered, instead of only merge maps. Thereby proving that the hardness of CR_n formulas is intact even after changing the weak isomorphism checking in MRes to the stronger consistency checking in MRes-ℛ.
Cite as

Sravanthi Chede and Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chede_et_al:LIPIcs.STACS.2023.21,
  author =	{Chede, Sravanthi and Shukla, Anil},
  title =	{{Extending Merge Resolution to a Family of QBF-Proof Systems}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.21},
  URN =		{urn:nbn:de:0030-drops-176737},
  doi =		{10.4230/LIPIcs.STACS.2023.21},
  annote =	{Keywords: Proof complexity, QBFs, Merge Resolution, Simulation, Lower Bound}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.40
Understanding Cutting Planes for QBFs

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res. Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2016.40,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Understanding Cutting Planes for QBFs}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40},
  URN =		{urn:nbn:de:0030-drops-68758},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.40},
  annote =	{Keywords: proof complexity, QBF, cutting planes, resolution, simulations}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.15
Are Short Proofs Narrow? QBF Resolution is not Simple

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
The groundbreaking paper 'Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that space lower bounds again can be obtained via width lower bounds. Here we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Forall-Exp+Res and IR-calc, however only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are Short Proofs Narrow? QBF Resolution is not Simple. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2016.15,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Are Short Proofs Narrow? QBF Resolution is not Simple}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.15},
  URN =		{urn:nbn:de:0030-drops-57164},
  doi =		{10.4230/LIPIcs.STACS.2016.15},
  annote =	{Keywords: proof complexity, QBF, resolution, lower bound techniques, simulations}
}
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact