On CNF formulas irredundant with respect to unit clause propagation

TL;DR

This paper investigates the properties of ucp-irredundant CNF formulas, demonstrating that their size can significantly exceed the smallest ucp-equivalent formulas, especially for symmetric definite Horn functions.

Contribution

It provides the first known example of a ucp-irredundant formula substantially larger than the minimal ucp-equivalent formula, establishing a lower bound on their size ratio.

Findings

A ucp-irredundant formula can be larger than the smallest ucp-equivalent formula by a factor of (n/ ln n)

The known upper bound on the size ratio is tight up to a polynomial factor

The results apply to symmetric definite Horn functions

Abstract

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)$. Consequently, a general upper bound on the above ratio cannot be smaller than this.