# On CNF formulas irredundant with respect to unit clause propagation

arXiv: https://arxiv.org/abs/2309.01750 · HTML: https://mlsanity.com/paper/2309.01750/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 21 references that are in the map.
- First posted on arXiv 4 Sep 2023.

## Builds on (most cited first, 2 of 2)

- [On Tackling the Limits of Resolution in SAT Solving](https://mlsanity.com/paper/1705.01477/) (2017)
- [Bounds on the size of PC and URC formulas](https://mlsanity.com/paper/2001.00819/) (2020)

## Abstract (arXiv)

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 n2, 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.