On CNF formulas irredundant with respect to unit clause propagation

要約

2 つの CNF 式は、単位句の伝播 (UCP) に関して同じように動作する場合、ucp 同等と呼ばれます。
句を削除すると、元の式と ucp に等価ではない式が生成される場合、その式は ucp 非冗長と呼ばれます。
既知の結果の結果として、ucp に非冗長な式のサイズと最小の ucp に相当する式のサイズの比は最大 $n^2$ です ($n$ は変数の数です)。
対称定ホーン関数に対する ucp 非冗長公式の例を示します。この公式は、ucp に相当する最小の公式よりも係数 $\Omega(n/\ln n)$ だけ大きく、したがって、
上記の比率をこれより小さくすることはできません。

要約(オリジナル)

Two CNF formulas are called ucp-equivalent, if they behave in the same way with respect to the unit clause propagation (UCP). A formula is called ucp-irredundant, if removing any clause leads to a formula which is not ucp-equivalent to the original one. As a consequence of known results, the ratio of the size of a ucp-irredundant formula and the size of a smallest ucp-equivalent formula is at most $n^2$, where $n$ is the number of the variables. We demonstrate an example of a ucp-irredundant formula for a symmetric definite Horn function which is larger than a smallest ucp-equivalent formula by a factor $\Omega(n/\ln n)$ and, hence, a general upper bound on the above ratio cannot be smaller than this.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google