关于单位子句传播不可约的 CNF 公式

如果两个 CNF 公式关于单位子句传播（UCP）表现相同，则称它们是 ucp-等价的。如果一个公式删去任意子句后得到的公式不与原公式 ucp-等价，则称该公式是 ucp-不可约的。作为已知结果的推论，ucp-不可约公式的大小与最小的 ucp-等价公式的大小之比至多为 $n^2$，其中 $n$ 为变量个数。我们给出一个对称确定 Horn 函数的 ucp-不可约公式的例子，其大小比最小的 ucp-等价公式大 $\Omega(n/\ln n)$ 倍。因此，上述比值的一般上界不可能小于此。