Summary

		p-simulation		unit
	rep. eff.	hierarchy	inference	propagation	learning
SAT	1	EEE	resolution	watched literals	relevance
cardinality	exp	P?E	not unique	watched literals	relevance
PB	exp	P?E	uniquely defined	watched literals	+ strengthening
symmetry
QPROP

As before, a few notes are in order:

• While both cardinality and pseudo-Boolean representations can be exponentially more efficient than their Boolean counterpart, it is not clear how often compressions of this magnitude will occur in practice.
• The entries in the $p$-simulation column indicate that the pigeonhole problem is easy, clique coloring remains hard, and the complexity of parity problems is unknown if no new variables are introduced.
• The cardinality entry for ``inference'' is intended to reflect the fact that the natural resolvent of two cardinality constraints need not be one.
• Pseudo-Boolean systems can use existing learning techniques, augmented with the strengthening idea.