All reports by Author Sravanthi Chede:

__
TR24-081
| 2nd April 2024
__

Sravanthi Chede, Leroy Chew, Anil Shukla#### Circuits, Proofs and Propositional Model Counting

Revisions: 1

__
TR23-129
| 21st August 2023
__

Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla#### Understanding Nullstellensatz for QBFs

__
TR22-002
| 11th December 2021
__

Sravanthi Chede, Anil Shukla#### Extending Merge Resolution to a Family of Proof Systems

Revisions: 1

__
TR21-109
| 20th July 2021
__

Sravanthi Chede, Anil Shukla#### QRAT Polynomially Simulates Merge Resolution.

__
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

Sravanthi Chede, Leroy Chew, Anil Shukla

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

Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla

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

Sravanthi Chede, Anil Shukla

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

Sravanthi Chede, Anil Shukla

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

Sravanthi Chede, Anil Shukla

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