Abstract
We investigate CNF formulas with a high level of propagation strength - they are unit refutation complete or propagation complete. The class of unit refutation complete (URC) formulas was introduced by del Val (1994) and it consists of formulas whose consistency with any given partial assignment can be tested by unit propagation.
Gwynne and Kullmann (2013) showed that the class of URC formulas coincides with the class SLUR (single lookahead unit resolution) introduced by Schlipf et al. (1995). Later Bordeaux and Marques-Silva (2012) introduced the class of propagation complete formulas (PC) which are URC and, moreover, unit propagation derives all implied literals provided the formula is satisfiable with a given partial assignment of its variables.
Every boolean function has a URC and a PC representation. In particular, a canonical CNF which consists of all prime implicates is always PC and, hence, URC.
On the other hand, it is co-NP complete to check if a formula is URC (Cepek et al. 2012) or PC (Babka et al. 2013). In this talk, we present the following results on the size of PC and URC formulas: - an exponential separation between the size of URC formulas and PC formulas (the example is a Horn formula), - an exponential separation between the size of PC encodings with existentially quantified auxiliary variables and URC formulas (the example is a q-Horn formula, see below), - we prove that the sizes of all irredundant PC formulas for the same function differ at most by a polynomial factor, - we present an example of a function demonstrating that a similar statement is not true for URC formulas.
The class of q-Horn formulas was introduced by (Boros et al. 1990) as a generalization of both Horn and 2-CNF formulas. It is a tractable class which means that satisfiability of q-Horn formulas can be tested in polynomial time, the class of q-Horn formulas is closed under partial assignment, and we can check if a formula is q-Horn in linear time by results of (Boros et al. 1994).
Both Horn and 2-CNF formulas are URC while q-Horn formulas are not URC in general. In this presentation, we show that for every $n$ there is a q-Horn formula on $n$ variables with $4n$ clauses such that any equivalent URC formula has size at least $2^{n-1}$.
On the other hand, we show that given a q-Horn formula $\phi$ which represents a q-Horn function $f$ on $n$ variables we can construct in polynomial time a URC encoding of $f$ which uses existentially quantified auxiliary variables.