In Quantified Boolean Formulas (QBFs), dependency schemes help identify spurious or superfluous variable dependencies introduced by the quantifier prefix but not essential for constructing countermodels. Detecting such dependencies can provably shorten refutations in certain proof systems and is expected to improve the performance of QBF solvers. Among the most prominent solving techniques for QBFs is Quantified Conflict-Driven Clause Learning, a generalization of CDCL to the quantified setting. The QCDCL proof system provides an abstract framework that captures the reasoning employed by such solvers.  In this talk, I will describe how dependency schemes can be incorporated into QCDCL-based proof systems in various phases: during preprocessing, in the decision heuristics, or within propagation and learning.

Based on joint work with Abhimanyu Choudhury.

Short Bio: Meena Mahajan is a professor at The Institute of Mathematical Sciences, HBNI, Chennai, India. Her interests span several sub-areas within theoretical computer science. Her research focusses primarily on understanding the limits of efficient computation, and encompasses many aspects of complexity theory, including Boolean function complexity, algebraic circuits, and proof complexity. https://www.imsc.res.in/~meena