A lower bound for DLL algorithms for k-SAT

被引：0

作者：

Pudlák, P

Impagliazzo, R

机构：

来源：

PROCEEDINGS OF THE ELEVENTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS | 2000年

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

There exist constants c(k) > 0, c(k) --> 0 as k --> infinity, such that every DLL algorithm for the satsfiability of sets of disjunctions of size less than or equal to k using m variables runs for at least Omega(2(m(1-ck))) steps on some inputs. Our proof is based on proving such a lower bound on the tree-like resolution proofs of generalized Tseitin tautologies.

引用

页码：128 / 136

页数：3

共 22 条

[1] Simplified and improved resolution lower bounds [J].