On CNF formulas irredundant with respect to unit clause propagation

要約

2つのCNF式が単位節伝搬（UCP）に関して同じ振る舞いをする場合、ucp-equivalentと呼ばれる。ある節を取り除くと、元の式とucp-equivalentでない式になる場合、その式はucp-irredundantと呼ばれる。既知の結果から、ucp-irredundantな式のサイズと最小のucp-equivalentな式のサイズの比は最大$n^2$である。対称定数ホーン関数のucp-冗長式の例を示すが、これは最小のucp-等価式より$Omega(n/jln 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, DeepL