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:

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