| ||||
| ||||
![]() Title:Lower Bounds for QCDCL via Formula Gauge Conference:SAT-2021 Tags:lower bounds, proof complexity, QBF, QCDCL and resolution Abstract: QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size. We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL. Lower Bounds for QCDCL via Formula Gauge ![]() Lower Bounds for QCDCL via Formula Gauge | ||||
Copyright © 2002 – 2025 EasyChair |