Alladi Ramakrishnan Hall

IMSc Dependency schemes in CDCL-based QBF solving: a proof-theoretic study

Abhimanyu Choudhury

IMSc

In Quantified Boolean Formulas QBFs, dependency schemes help
to detect spurious or superfluous dependencies that are implied by the
variable ordering in the quantifier prefix but are not essential for
constructing countermodels. This detection can provably shorten
refutations in specific proof systems, and is expected to speed up
runs of QBF solvers. The proof system QCDCL recently defined by
Beyersdorff and Boehm (LMCS 2023) abstracts the reasoning employed by
QBF solvers based on conflict-driven clause-learning (CDCL)
techniques. We show how to incorporate the use of dependency schemes
into this proof system, either in a preprocessing phase, or in the
propagations and clause learning, or both. We then show that when the
reflexive resolution path dependency scheme Drrs is used, a mixed
picture emerges: the proof systems that add Drrs to QCDCL in these
three ways are not only incomparable with each other, but are also
incomparable with the basic QCDCL proof system that does not use Drrs
at all, as well as with several other resolution-based QBF proof
systems. A notable fact is that all our separations are achieved
through QBFs with bounded quantifier alternation.

(Joint work with Meena Mahajan. To appear in FSTTCS2023.)