Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
summary
Paper proves that standard QBF CDCL and Q-resolution are incomparable by giving two explicit families: QParity has polynomial-size QCDCL refutations but requires exponential Q-resolution, and a trapdoor formula built from pigeonhole-like hard cores has polynomial Q-resolution but forces exponential QCDCL. Techniques are constructive: build formulas, extract/simulate proofs, and use proof-complexity lower bounds. Then a modified QCDCL model with asserting-order no-reduction policy is defined and shown to simulate Q-resolution in polynomial size, so the modified solver is P-equivalent to Q-resolution.
AI-written summary · about