2024
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs
AAAI 2024technical
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…