Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR23-061 | 2nd May 2023 03:39

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


Authors: Abhimanyu Choudhury, Meena Mahajan
Publication: 2nd May 2023 04:16
Downloads: 273


We formalize the notion of proof systems obtained by adding normal dependency schemes into the QCDCL proof system underlying algorithms for solving Quantified Boolean Formulas, by exploring the addition of the dependency schemes via two approaches: one as a preprocessing tool, and second in propagation and learnings in the QCDCL trails.

We show that QCDCL augmented with the reflexive resolution path dependency scheme D=D$^{rrs}$ produces three proof systems of interest: QCDCL(D), D+QCDCL and D+QCDCLD(D). We show that these three systems are not only pairwise incomparable, but also each system is incomparable with the standard QCDCL and QCDCL$^{cube}$, as well as with QCDCL$^{LO}_{NORED}$, QRes, QURes, and Q(D$^{rrs}$)Res.

ISSN 1433-8092 | Imprint