Boolean Summary

We summarize the results of this section by completing the first row of our table as follows:

		p-simulation		unit
	rep. eff.	hierarchy	inference	propagation	learning
SAT	1	EEE	resolution	watched literals	relevance
cardinality
PB
symmetry
QPROP

The entries are really just an informal shorthand:

• Representational efficiency: Boolean satisfiability is the benchmark against which other languages will be measured; we give here the relative savings to be had by changing representation.
• $p$-simulation hierarchy: We give the proof complexity for the three problem classes discussed in Section 2.4. For Boolean satisfiability, all of the problems require proofs of exponential length.
• Inference: The basic inference mechanism used by DPLL is resolution.
• Propagation: Watched literals lead to the most efficient implementation.
• Learning: Relevance-based learning appears to be more effective than other poly-sized methods.