不可满足的线性CNF公式庞大且复杂
摘要：线性CNF公式的定义是，任意两个子句之间最多只有一个变量相同。我们证明了存在不可满足的线性k-CNF公式，其中子句数量最多为4k^2 4^k个；另一方面，任意一个线性k-CNF公式，如果子句数量最多为4^k/(8e^2k^2)，则可满足。上界是使用概率方法得到的，并且我们并没有给出接近上界的显式构造。其中一个原因是不可满足的线性公式比一般的（非线性）公式具有更复杂的结构：首先，任何不可满足的线性k-CNF公式的树式分辨证明的大小至少为2^(2^(k/2-1))；这意味着小的不可满足的线性k-CNF公式对于Davis-Putnam风格的分裂算法来说是难的实例。其次，如果我们要求公式F具有严格的分辨树，即F中的每个子句在分辨树中只使用一次，那么我们需要至少a^a^...^a个子句，其中a约为2，这个指数塔的高度大致为k。
作者：Dominik Scheder
论文ID：0905.1587
分类：Discrete Mathematics
分类简称：cs.DM
提交时间：2010-10-29