Open Collections

Description

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 (QCDCL), a generalization of CDCL to the quantified setting. The proof system defined by Beyersdorff and Boehm (LMCS 2023) provides an abstract framework that captures the reasoning employed by QCDCL 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.