PC和URC公式的大小的界
Bounds on the size of PC and URC formulas
摘要：
在本文中，我们调查CNF公式，单位传播是强大到足以得出一个矛盾，如果公式连同部分分配的变量是不可满足的（单位反驳完成或URC公式）或另外得出所有隐含的文字，如果公式是可满足的（传播完成或PC公式）。如果一个公式使用存在量化的辅助变量表示一个函数，它被称为函数的编码。我们证明了PC和URC公式和编码的大小的几个结果。其中之一是不同类型公式大小之间的分隔。也就是说，我们证明了URC公式和PC公式的大小之间的指数分离和使用辅助变量和URC公式的PC编码的大小之间的指数分离。除此之外，我们证明了任何两个无冗余的PC公式的大小不同的相同的功能，最多由一个因子多项式的变量的数量，并提出了一个函数的例子，证明了类似的声明是不真实的URC公式。上述分离之一意味着q-Horn公式可能需要指数数量的附加子句才能成为URC公式。另一方面，对于每一个q-Horn公式，我们提出了一个多项式大小的URC编码相同的功能，使用辅助变量。这种编码一般不是q-Horn。
英文摘要：
In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
