Satisfaction Hypothesis
Try to satisfy as much as possible with next literal
Take account of different lengths
- clause of length i rules out a fraction 2-i of all solutions
- weight each clause by the number 2-i
For each literal, calculate weighted sum
- add the weight of each clause the literal appears in
- the larger this sum, the more difficulties are eliminated
This is the Jeroslow-Wang Heuristic
Variable and value ordering