Random Circle Minus(Log N)-Cnfs Are Hard For Cutting Planes
2017 IEEE 58TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE (FOCS)(2017)
摘要
The random k-SAT model is the most important and well-studied distribution over k-SAT instances. It is closely connected to statistical physics and is a benchmark for satisfiability algorithms. We show that when k = circle minus( logn), any Cutting Planes refutation for random k-SAT requires exponential size in the interesting regime where the number of clauses guarantees that the formula is unsatisfiable with high probability.
更多查看译文
关键词
Proof complexity, random k-SAT, Cutting Planes
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络