On CNF formulas irredundant with respect to unit clause propagation
This is an incremental theoretical result for computational logic and SAT solving, refining bounds on formula redundancy under unit clause propagation.
The paper tackled the problem of bounding the size ratio between ucp-irredundant CNF formulas and their smallest ucp-equivalent versions, demonstrating an example where the ratio is Ω(n/ln n), improving the known upper bound from n^2.
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 $Ω(n/\ln n)$. Consequently, a general upper bound on the above ratio cannot be smaller than this.