Abstract
The quantified version QCDCL of CDCL is one of the main approaches to solve quantified Boolean formulas (QBF). While CDCL is known to be tightly captured by propositional resolution, we show that QCDCL and Q-Resolution are exponentially incomparable. We also explore different versions of QCDCL and compare their strength. Technically we use develop lower bound techniques that are effective for QBF resolution systems as well as for QCDCL. The talk is based on a series of papers with Benjamin Böhm and Tomas Peitl, which appeared at ITCS’21, SAT’21, SAT’22, IJCAI’22.