One way of viewing the difference between SAT and CSPs is to think of programming in assembler vs programming in C. It can
be considerably simpler to program in C than assembler. Similarly it can be considerably simpler to model real world problems
in CSP than in SAT. On the other hand C’s machine model is still rather close to the underlying hardware model accessed directly
in assembler. Similarly, in CSPs the main method of reasoning, backtracking search, can be viewed as being an extension of
DPLL, the main method of reasoning for SAT. Where the analogy breaks down is that unlike C and assember whose machine models
are computationally equivalent, some CSP techniques offer a considerable boost in inferential power over the resolution inferences
preformed in DPLL. An intresting question is how to combine this additional inferential power with the more powerful forms
of resolution preformed in modern DPLL solvers. One approach for achieving such a combination will be presented.