Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Sravanthi Chede:

TR24-081 | 2nd April 2024
Sravanthi Chede, Leroy Chew, Anil Shukla

Circuits, Proofs and Propositional Model Counting

In this paper we present a new proof system framework CLIP (Cumulation Linear Induction Proposition) for propositional model counting. A CLIP proof firstly involves a 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 ... more >>>

TR23-129 | 21st August 2023
Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla

Understanding Nullstellensatz for QBFs

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 ... more >>>

TR22-002 | 11th December 2021
Sravanthi Chede, Anil Shukla

Extending Merge Resolution to a Family of Proof Systems

Revisions: 1

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 within the proofs. Every line of this proof system consists of existential clauses along with countermodels. MRes stores ... more >>>

TR21-109 | 20th July 2021
Sravanthi Chede, Anil Shukla

QRAT Polynomially Simulates Merge Resolution.

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>

TR21-104 | 26th June 2021
Sravanthi Chede, Anil Shukla

Does QRAT simulate IR-calc? QRAT simulation algorithm for $\forall$Exp+Res cannot be lifted to IR-calc

We show that the QRAT simulation algorithm of $\forall$Exp+Res from [B. Kiesl and M. Seidl, 2019] cannot be lifted to IR-calc.

more >>>

ISSN 1433-8092 | Imprint