ABSTRACT
In this chapter we show a generic use of SAT as a vehicle for solving constraint satisfaction problems over finite domains. First, we discuss extensional and intentional relations. Roughly, extensional relations are those that are stored (they are our data). Intentional relations are those relations that we search for (and the solver computes). The difference between the two is expressed by so-called closed world assumption (CWA). After illustrating what this is all about (and showing how CWA is related to the existence of the least model) we discuss constraint satisfaction problems (CSP). We show how the propositional logic (and the version of predicate logic considered above) can be used to reformulate and solve CSPs. Then we show that, in fact, the search for satisfying valuations is a form of CSP. We also discuss the Schaefer theorem on classification of Boolean constraint satisfaction problems.
