Meena Mahajan

Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs

Conflict-driven clause learning (CDCL) is the dominating algorithmic paradigm for SAT solving and hugely successful in practice. In its lifted version QCDCL, it is one of the main approaches for solving quantified Boolean formulas (QBF). In both SAT and QBF, proofs can be efficiently extracted fr…