Constraint Satisfiaibility Problems

CSPs explained

X = a set of variables {X1,...Xn}

This is the variables the problem you are trying to solve will have.

D = a set of domains for each X {D1,....Dn}

A set of domains for each variable (X).

For each of the variables, what are the possible values each variable (X) can take?

C = a set of constraints, scope, relationships between variables.

Either a solution exists or it doesn't. So how is a Rubik's cube defined? The variables for example are composed of 6 Boolean variables to represent each color on each facelet. The domain D is the possible colors these variables can represent. A search method called "backtracking" is often applied to this class of problem.

Generally to apply a SAT solver we must be able to define the problem in the right way. Once it's defined in the right way, if it fits into this class of problem, we know it can be solved by a SAT solver.

To define a problem is often a lot easier than to solve it.