Alladi Ramakrishnan Hall

Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs

Meena Mahajan

IMSc

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 from runs of (Q)CDCL solvers. While for CDCL, it
is known that the proof size in the underlying proof system
propositional resolution matches the CDCL runtime up to a polynomial
factor, we show that in QBF there is an exponential gap between
QCDCL runtime and the size of the extracted proofs in QBF resolution
systems. We demonstrate that this is not just a gap between QCDCL
runtime and the size of any QBF resolution proof, but even the
extracted proofs are exponentially smaller for some instances. Hence
searching for a small proof via QCDCL (even with non-deterministic
decision policies) will provably incur an exponential overhead for
some instances.

Joint work with Olaf Beyersdorff and Benjamin Boehm.
To appear at AAAI 2024.