证明复杂度中的硬度放大
摘要：将难以予解决的最简化证明系统——树证明（tree resolution）的不可满足CNF公式族转化为在任何操纵多项式或最高度为k（即Th(k)证明）的证明系统中，需要大排名的公式。这些系统包括Lovasz-Schrijver和Cutting Planes证明系统及其高度模拟。 这些基于对两个新的证明系统——T^cc(k)和R^cc(k)的分析。T^cc(k)的证明行是任意的布尔函数，每个函数都可以通过高效的k方通信协议进行评估。它们包括Th{k-1}证明作为一个特殊情况。R^cc(k)证明更强，只需要每个推理通过高效的k方通信协议在本地可检验。 我们的主要结果如下： (1) 当k=O(loglogn)时，对于任何不可满足的CNF公式F，需要解决排名r，存在相关的CNF公式G=Lift\_k(F)需要在所有R^cc(k)系统中证明排名r^Omega(1/k) log^O(1) n。 (2) 当k=O(loglogn)时，对于T^cc(k)和R^cc(k)系统，存在严格的层次结构，其中存在不可满足的CNF公式，需要大排名R^cc(k)证明，但只有log^O(1) n排名Th(k)证明。 (3) 当k=O(loglogn)时，存在对于大类别的升级CNF公式的树形T^cc(k)证明大小的2^(n^Omega(1/k))下界。 (4) 一种产生低排名R^cc(2)推理（因此包括Cutting Planes和Th(1)推理）整数间隙的一般方法，基于低排名解决的相关间隙。这些间隙对于MAX-2t-SAT是最优的。
作者：Paul Beame, Trinh Huynh, Toniann Pitassi
论文ID：0912.0568
分类：Computational Complexity
分类简称：cs.CC
提交时间：2009-12-04