#### 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.)

Done