论文标题
CNF平价编码
CNF Encodings of Parity
论文作者
论文摘要
均等函数的CNF表示中的最小条款数量$ x_1 \ oplus x_2 \ oplus \ dotsb \ oplus x_n $ as $ 2^{n-1} $。可以通过使用非确定性变量（也称为猜测或辅助变量）获得更紧凑的CNF编码。在本文中，我们证明了以下下限，几乎匹配已知的上限，数字$ m $条款和最大宽度$ k $ of Lecauses：1）如果最多有$ s $ s $ auxilariary变量，则$ m \geΩ 2）最低条款数量至少为$ 3N $。我们从Paturi，Pudlak和Zane引起的可满足性编码引理中得出了前两个界限。
The minimum number of clauses in a CNF representation of the parity function $x_1 \oplus x_2 \oplus \dotsb \oplus x_n$ is $2^{n-1}$. One can obtain a more compact CNF encoding by using non-deterministic variables (also known as guess or auxiliary variables). In this paper, we prove the following lower bounds, that almost match known upper bounds, on the number $m$ of clauses and the maximum width $k$ of clauses: 1) if there are at most $s$ auxiliary variables, then $m \ge Ω\left(2^{n/(s+1)}/n\right)$ and $k \ge n/(s+1)$; 2) the minimum number of clauses is at least $3n$. We derive the first two bounds from the Satisfiability Coding Lemma due to Paturi, Pudlak, and Zane.
