Lower Bounds for QCDCL via Formula Gauge

被引：5

作者：

Boehm, Benjamin ^{[1
]}

Beyersdorff, Olaf ^{[1
]}

机构：

[1] Friedrich Schiller Univ Jena, Jena, Germany

来源：

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021 | 2021年 / 12831卷

关键词：

QBF; QCDCL; Proof complexity; Resolution; Lower bounds; RESOLUTION;

D O I：

10.1007/978-3-030-80223-3_5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：47 / 63

页数：17

共 34 条

[1]

Balabanov V, 2014, LECT NOTES COMPUT SC, V8561, P154, DOI 10.1007/978-3-319-09284-3_12

[2] Unified QBF certification and its applications [J].