On the expressive power of unit resolution

Unit resolution is a key feature of state of the art sat solvers [13] [7] [5], where it speeds up the search for solutions and inconsistencies. It is well known that different cnf representations of a given problem do not always allow unit resolution to deduce the same information. For example, the cnf encoding for pseudo Boolean constraints proposed in [3] allows unit resolution to restore generalized arc consistency. This is not the case with the encoding proposed in [16], which does not allow unit resolution to deduce as much information as the former encoding does. As a manner of speaking, the expressive power of unit resolution is best exploited using the encoding proposed in [3], with notable consequences on the resolution time.