Research Interests

• Proof Complexity
• Algebraic Proof Systems
• Quantified Boolean Formulas, SAT
• Model Counting, MaxSAT
• Knowledge Compilation

Contact

Email: sravanthi.20csz0001@iitrpr.ac.in, sravanthichede@gmail.com, sravanthic@imsc.res.in

Office: Room G-14, Main Building, IMSc Chennai-600113.

Publications

Journal publications

• Sravanthi Chede & Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems.
  ACM Transactions on Computation Theory (ACM TOCT) 2026, Volume 18, Issue 2, Article no. 11. [Invited Paper]
  doi:10.1145/3786779.
  • [Published version], [Summary]

    This is an extended version of our STACS23 paper and here we additionally show that Regular versions of our systems are exponential stronger than that of the MRes proof system.

Conferences Proceedings

• Sravanthi Chede, Leroy Chew, Vaibhav Krishan & Anil Shukla. On Proof Systems for #QBF.
  The 29th International Conference on Theory and Applications of Satisfiability Testing (SAT) 2026.
  doi:10.4230/LIPIcs.SAT.2026.10.
  • [Proceedings], [Abstract]

    For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages.
    In this paper, we explore #QBF proof systems to count the number of Skolem functions. In addition to a naive system, we study #QBF systems based on the ∀-expansion rule of QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from ∀-expansion based #QBF proof systems.
    

• Sravanthi Chede, Leroy Chew & Anil Shukla. Circuits, Proofs and Propositional Model Counting.
  44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2024.
  doi:10.4230/LIPIcs.FSTTCS.2024.18.
  • [Proceedings], [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 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., SAT 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in [Beyersdorff et al., SAT 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Capelli, SAT 19], CPOG [Bryant et. al., SAT, 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 P^{#P} 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.

• Sravanthi Chede & Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems.
  40th International Symposium on Theoretical Aspects of Computer Science (STACS) 2023.
  doi:10.4230/LIPIcs.STACS.2023.21.
  • [Proceedings], [Abstract]

    Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'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-R in which the information of countermodels are stored in any pre-fixed complete representation R. Hence, corresponding to each possible complete representation R, we have a sound and refutationally complete QBF-proof system in MRes-R. To handle these arbitrary representations, we introduce consistency checking rules in MRes-R 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 [Blinkhorn et al. SAT.'2021], which was designed to solve DQBFs (Dependency QBFs) using MRes like clause-strategy pairs. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in the paper and deduce that `Ordered' versions of the proof systems in MRes-R are indeed polynomial time verifiable.
    On the lower bound side, we lift the lower bound result of regular MRes ([Beyersdorff et al. FSTTCS.'2020]) by showing that the completion principle formulas (CR_n) from [Jonata et al. Theor. Comput. Sci.'2015] which are shown to be hard for regular MRes in [Beyersdorff et al. FSTTCS.'2020], are also hard for any regular proof system in MRes-R.
    Hence, the results of this paper show that the family of proof systems in MRes-R have the power to refute false DQBFs efficiently, which are beyond the power of regular MRes.

DataSets

• Anil Shukla & Sravanthi Chede. Hamming weight based model counting benchmarks [Data set].
  Zenodo (2025). doi:10.5281/zenodo.15238543.
  • [Access Dataset], [Benchmark Description]

Preprints

• Sravanthi Chede, Leroy Chew, Balesh Kumar & Anil Shukla. Understanding Nullstellensatz for QBFs.
  • [ECCC], [Abstract]

    QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful in line-based proof systems, is not refutationally complete for static proof systems.
    Nullstellensatz (NS, [Beame et al. FOCS.'1994]) is a well known static propositional proof system, inspired by Hilbert's theorem [Hilbert Math. Ann.'1893] of the same name. It falls into the category of algebraic proof systems such as the Polynomial Calculus [Book, Krajíček Cam. Uni.'2019, p.162] or the Ideal Proof System (IPS,[Grochow et al. J. ACM.'2018]). In this paper, we initiate the study of the NS proof system for QBFs using the existing expansion (∀Exp) framework and a new "∀Strat" framework. We introduce four new static QBF refutation systems: ∀Exp+NS, ∀Exp+NS', ∀Strat+NS and ∀Strat+NS', which use NS and a more powerful version of NS (NS') with twin variable encoding that allows it to simulate tree-like resolution without an exponential blowup.
    We explore relationships among the proposed systems and analyse their proof sizes for a few well-known hard QBF-families. We find that ∀Exp+NS' and ∀Strat+NS' are incomparable. This result is in line with the incomparability result between ∀Exp+Res and Q-Res [Beyersdorff et al. STACS.'2015].

• Sravanthi Chede & Anil Shukla. Does QRAT simulate IR-calc? QRAT simulation algorithm for ∀Exp+Res cannot be lifted to IR-calc.
  • [ECCC]

Other works

• Ranjana Roy Chowdhury, Shivam Gupta & Sravanthi Chede. World War III analysis using signed social networks. Social Network Analysis and Mining Journal, Volume 11.
  • [Published version], [ArXiv]

Teaching Assistant Experience (IIT Ropar)

• Feb-May 2021: (GE103) Introduction to Computing and Data Structure
• July-Dec 2021, 2022, 2023, 2024: (CS201) Data Structures
• Jan-May 2022, 2023, 2024, 2025: (CS306) Theory of Computation
• July 2025-Present: (CS302) Design and Analysis of Algorithms