Next: PseudoBoolean and Cardinality Constraints
Up: Boolean Satisfiability
Previous: Clique coloring problems
We summarize the results of this section by completing the first row
of our table as follows:


psimulation 

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.
 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: Relevancebased learning appears to be more
effective than other polysized methods.
Next: PseudoBoolean and Cardinality Constraints
Up: Boolean Satisfiability
Previous: Clique coloring problems
Matt Ginsberg
20040219