Introduction and basic definitions¶

In this round we leave the purely Boolean domain and study CSP (constraint satisfaction problem) instances in which the domains of variables can be larger, but usually finite, sets. We see some useful “global constraints” that make the modelling of many problems much easier and study how such constraints can be solved. Note that this round is a very shallow introduction to the topic, please see the provided references and [HCP2006] for more information.

As a concrete problem description language, we will use the MiniZinc language in this round. For simplicity, we restrict the discussion to finite domain variables here. Variables with infinite domains are then discussed in the rounds for “Satisfiability Modulo Theories” later in this course.

Similarly to SAT, a problem instance in CSP consists of variables and some constraints, and the task of the constraint solver is then to find out whether there are some values for the variables so that all the constraints are satisfied.

Definition: Domains and assignments

The domain of a variable \( \Var \) is a finite set \( \Dom{\Var} \) of values that can be assigned to it. An assignment \( \Asgn \) to a set of variables \( \Vars \) is a function that assigns each variable \( \Var \) to a value \( \AsgnTo{\Var} \in \Dom{\Var} \).

Example

In MiniZinc, one can declare integer variables and constants as shown below.

var int: x;   % An integer variable
var 1..10: y; % An integer variable with the domain {1,2,...,10}
int: c = 3;   % An integer constant

The domain of the variable declared with var int: x depends on the underlying solver: it can be unbounded or restricted, for instance, to the finite range \( [-2^{31},2^{31}-1] \).

Mathematically, a constraint is just a relation that restricts the value combinations that a set of variables can have:

Definition: Constraint

A constraint over a set of variables \( \Set{\CVarI1,…,\CVarI{k}} \subseteq \Vars \) is a set \( \Constr(\CVarI1,…,\CVarI{k}) \subseteq \Dom{\CVarI1} \times \ldots \times \Dom{\CVarI{k}} \).

A tuple \( \Tuple{v_1,…,v_k} \in \Constr(\CVarI1,…,\CVarI{k}) \) is called a solution to \( \Constr \).

An assignment \( \Asgn \) to \( \Vars \) satisfies \( \Constr \) if \( \Tuple{\AsgnTo{\CVarI1},…,\AsgnTo{\CVarI k}} \in \Constr(\CVarI1,…,\CVarI{k}) \).

However, as the explicit relation presentation (that is, listing all the tuples in it) can contain up to \( \prod_{i=1}^k\Card{\Dom{\CVarI i}} \) tuples, constraints are usually given more concisely in some symbolic notation.

Example

The standard binary less-or-equal constraint between two integer-valued variables, \( \VarI1 \le \VarI2 \), corresponds to the set \( \Setdef{\Tuple{\ValI1,\ValI2} \in \Dom{\VarI1} \times \Dom{\VarI2}}{\ValI1 \le \ValI2} \).

For instance, if \( \Dom{x} = \Set{1,2,3,6} \) and \( \Dom{y} = \Set{1,4,5,9} \), then \( x \le y \) means the set \( \Set{\Tuple{1,1},\Tuple{1,4},\Tuple{1,5},\Tuple{1,9},\Tuple{2,4},\Tuple{2,5},\Tuple{2,9},\Tuple{3,4},\Tuple{3,5},\Tuple{3,9},\Tuple{6,9}} \).

Definition: Constraint satisfaction problem

A constraint satisfaction problem (CSP) instance consists of

a finite set \( \Vars \) of variables with domains, and
a finite set of constraints, each over a subset of \( \Vars \).

A solution to a CSP instance is an assignment to \( \Vars \) so that all the constraints are satisfied.

A CSP instance is satisfiable if it has at least one solution, otherwise it is unsatisfiable.

The constraint satisfaction problem is: given a CSP instance, is it satisfiable?

Example

Consider the verbal arithmetic problem \[\begin{array}{cccccc} & & s & e & n & d \\\\ + & & m & o & r & e \\\\ \hline = & m & o & n & e & y \end{array}\] requiring us to find distinct digits for the variables so that the equation holds and the first digits are not zero. We can model this with a simple CSP instance consisting of the variables \( \Set{s,e,n,d,m,o,r,y} \), each variable having the domain \( \Set{0,1,2,3,4,5,6,7,8,9} \), and the following 31 constraints: \begin{eqnarray*} \small 1000 s + 100 e + 10 n + d + 1000 m + 100 o + 10 r + e &=& 10000 m + 1000 o + 100 n + 10 e + y \\\\ s &\neq& 0 \\\\ m &\neq& 0 \\\\ \alpha &\neq& \beta \textrm{ for all \( \Set{\alpha,\beta} \subset \Set{s,e,n,d,m,o,r,y} \)} \end{eqnarray*} and the domains \( \Dom{\alpha}=\Set{0,1,2,3,4,5,6,7,8,9} \) for each variable \( \alpha \in \Set{s,e,n,d,m,o,r,y} \).

After this, we can use a CSP solver to find whether the CSP instance is satisfiable or not.

Example

The CSP instance in the previous example can be declared in the MiniZinc language as shown below.

include "alldifferent.mzn";
var 1..9: s;
var 0..9: e;
var 0..9: n;
var 0..9: d;
var 1..9: m;
var 0..9: o;
var 0..9: r;
var 0..9: y;
constraint    1000*s + 100*e + 10*n + d
            + 1000*m + 100*o + 10*r + e
  = 10000*m + 1000*o + 100*n + 10*e + y;
constraint alldifferent([s,e,n,d,m,o,r,y]);
solve satisfy;
output ["   \(s)\(e)\(n)\(d)\n",
        "+  \(m)\(o)\(r)\(e)\n",
     "= \(m)\(o)\(n)\(e)\(y)\n"];

Note that the requirements \( \Dom{m} \neq 0 \) and \( \Dom{s} \neq 0 \) are modelled by removing 0 from the domains of \( m \) and \( s \). Similarly, the digit distinctness requirement is handled by a “global constraint” \( \AllDiffC \). Executing a MiniZinc solver on this input gives us the solution

   9567
+  1085
= 10652

CNF SAT as CSP¶

As expected, Boolean formula satisfiability can be easily seen as a constraint satisfiability problem. That is, given a CNF formula \( \phi = C_1 \land … \land C_m \), we can construct a CSP instance that is satisfiable if and only if \( \phi \) is. The CSP instance is constructed as follows:

The variables are the same as in \( \phi \).
The domain of each variable is the Boolean domain \( \{\False,\True\} \).
For each clause \( C_i = (l_{i,1} \lor … \lor l_{i,p}) \) in \( \phi \), where \( l_{i,j} = x_{i,j} \) or \( l_{i,j} = \neg x_{i,j} \) for a variable \( x_{i,j} \), the CSP instance has the constraint \( \Constr_i(x_{i,1},…,x_{i,p}) \) consisting of all the tuples \( (v_1,…,v_p) \in \{\False,\True\}^p \) for which the truth assignment \( \Setdef{x_{i,j} \mapsto v_j}{0 \le j \le p} \) evaluates the clause to true.

Example

Consider the CNF formula \( (x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor \neg x_2) \land (\neg x_1 \lor \neg x_3) \land (\neg x_2 \lor \neg x_3) \) stating that exactly one of \( x_1 \), \( x_2 \), \( x_3 \) is true. Applying the construction above to it gives the CSP instance that consists of the variables \( \Vars = \{x_1,x_2,x_3\} \), each variable \( x \in \Vars \) having the domain \( \Dom{x} = \{\False,\True\} \), and the constraints

\( \small C_1(x_1,x_2,x_3) = \{(\False,\False,\True),(\False,\True,\False),(\False,\True,\True),(\True,\False,\False),(\True,\False,\True),(\True,\True,\False),(\True,\True,\True)\} \),
\( C_2(x_1,x_2) = \{(\False,\False),(\False,\True),(\True,\False)\} \),
\( C_3(x_1,x_3) = \{(\False,\False),(\False,\True),(\True,\False)\} \), and
\( C_4(x_2,x_3) = \{(\False,\False),(\False,\True),(\True,\False)\} \).