Bounds on the size of PC and URC formulas

TL;DR

This paper explores the size complexity of PC and URC formulas, establishing exponential separations and polynomial bounds, and investigates their implications for encoding functions with auxiliary variables.

Contribution

It proves exponential size separations between PC and URC formulas and provides polynomial-size URC encodings for q-Horn formulas using auxiliary variables.

Findings

Exponential separation between URC and PC formula sizes.

Any two irredundant PC formulas for the same function differ by at most a polynomial factor.

Polynomial-size URC encoding exists for q-Horn formulas using auxiliary variables.

Abstract

In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a factor polynomial in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.