7 citations · 7 across the 6 of their papers we have counts for
5 papers · 1 filter
On Knowledge Compilation Languages for QBFs
Sravanthi Chede, Vaibhav Krishan, Anil Shukla
In this work, we design knowledge compilation languages for quantified Boolean formulas (QBFs), with a particular focus on model counting. We introduce various languages in increas…
Extending Merge Resolution to a Family of Proof Systems
Sravanthi Chede, Anil Shukla
Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021]) is a recently introduced proof system for false QBFs. It stores the countermodels as merge maps. Merge maps are…
QRAT Polynomially Simulates Merge Resolution
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 wit…
Does QRAT simulate IR-calc? QRAT simulation algorithm for Exp+Res cannot be lifted to IR-calc
Sravanthi Chede, Anil Shukla
We show that the QRAT simulation algorithm of Exp+Res from [B. Kiesl and M. Seidl, 2019] cannot be lifted to IR-calc.
Feasible Interpolation for QBF Resolution Calculi
Olaf Beyersdorff, Leroy Chew, Meena Mahajan +1
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation techni…