稠密随机3CNF公式的短命题证伪
摘要：斯托普斯基随机3CNF公式构成了衡量命题证明系统平均行为的重要分布。已知在许多命题证明系统中，随机3CNF的反驳下界。特别重要的是对于具有Omega(n^{1.5-epsilon})子句的随机3CNF公式，已知指数规模的分辨反驳下界。另一方面，对于非抽象命题证明系统中随机3CNF的反驳大小的已知的非平凡的上界只有在具有Omega(n^{2}/log n)子句的分辨中由 Beame 等人(2002)给出。在本文中，我们展示了标准命题证明系统，即Frege证明层次结构中，对于具有足够大字句与变量比的随机3CNF公式，存在短的反驳。具体地，我们展示了多项式规模的命题反驳，其线条是TC^0公式(即TC^0-Frege证明)，用于具有n个变量和Omega(n^{1.4})子句的随机3CNF公式。这个想法是基于对Feige、Kim和Ofek(2006)给出的随机3CNF不可满足证据的有效命题正确性证明。由于这些证据的正确性是使用谱技术来验证的，我们开发了一种合适的方式来推理命题系统中的特征向量。为了完成完整的论证，我们在弱算术形式系统内工作，并使用一种通用的翻译方案将其转化为命题证明。
作者：Sebastian M"uller and Iddo Tzameret
论文ID：1101.3970
分类：Computational Complexity
分类简称：cs.CC
提交时间：2011-06-06