论文标题
PC和URC公式大小的界限
Bounds on the size of PC and URC formulas
论文作者
论文摘要
在本文中，我们研究了CNF公式，如果该公式足够强，则如果公式以及变量的部分分配不可令人满意（单位反驳或URC公式），或者如果可以得出所有插入的文字，则如果该公式不满意（单位反驳或URC公式），则如果该公式不满意（宣传完整或PC公式）。如果公式使用存在量化的辅助变量表示函数，则称为该函数的编码。我们证明了PC和URC公式和编码的大小的几个结果。其中之一是不同类型公式的大小之间的分离。也就是说，我们证明了URC公式和PC公式的大小之间的指数分离以及使用辅助变量和URC公式之间的PC编码大小之间的指数分离。除此之外，我们证明，同一函数的任何两个不繁殖的PC公式的大小最大都不同于变量数量中的一个因子多项式，并提供了一个函数的示例，表明对URC公式对于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.
