On the size of irredundant propagation complete CNF formulas

We investigate propagation complete (PC) CNF formulas for a symmetric definite Horn function of $n$ variables and demonstrate that the minimum size of these formulas is closely related to specific covering numbers, namely, to the smallest number of $k$-subsets of an $n$-set covering all $(k-1)$-subsets for a suitable $k$. As a consequence, we demonstrate an irredundant PC formula whose size is larger than the size of a smallest PC formula for the same function by a factor $\Omega(n/\ln n)$. This complements a known polynomial upper bound on this factor.

@article{savický2025_2309.01750,
  title={ On CNF formulas irredundant with respect to unit clause propagation },
  author={ Petr Savický },
  journal={arXiv preprint arXiv:2309.01750},
  year={ 2025 }
}