Research Interests

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

Contact

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

Office: Room 314, CSE Department, IIT Ropar-140001.

Publications

• 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.
  • [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.
  • [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.

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

Under Review

• Sravanthi Chede & Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems. An Extended version of this paper is under review in a Journal.
  • [Summary]

    In this manuscript, we additionally show that Regular versions of our systems are exponential stronger than that of the MRes proof system.

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]

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

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.
  • [Proceedings], [ArXiv]