CSPs: Adding Structure to SAT

摘要

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.