  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.
