Editing Constraint programming (section)

==Constraint satisfaction problem==
{{main|Constraint satisfaction problem}}

A constraint is a relation between multiple variables that limits the values these variables can take simultaneously.
{{math theorem
|Definition
|A constraint satisfaction problem on finite domains (or CSP) is defined by a triplet <math>(\mathcal{X},\mathcal{D},\mathcal{C})</math> where:
* <math>\mathcal{X} = \{x_1, \dots, x_n \}</math> is the set of variables of the problem;
* <math>\mathcal{D} = \{\mathcal{D}_1, \dots, \mathcal{D}_n \}</math> is the set of domains of the variables, i.e., for all <math>k \in [1; n]</math> we have <math>x_k \in \mathcal{D}_k</math>;
* <math>\mathcal{C} = \{C_1, \dots, C_m \}</math> is a set of constraints. A constraint <math>C_i=(\mathcal{X}_i, \mathcal{R}_i)</math> is defined by a set <math>\mathcal{X}_i = \{x_{i_1}, \dots, x_{i_k}\}</math> of variables and a relation <math>\mathcal{R}_i \subseteq \mathcal{D}_{i_1} \times \dots \times \mathcal{D}_{i_k}</math> that defines the set of values allowed simultaneously for the variables of <math>\mathcal{X}_i</math>.
}}

Three categories of constraints exist:
* extensional constraints: constraints are defined by enumerating the set of values that would satisfy them;
* arithmetic constraints: constraints are defined by an arithmetic expression, i.e., using <math><, >, \leq, \geq, =, \neq,...</math>;
* logical constraints: constraints are defined with an explicit semantics, i.e., ''AllDifferent'', ''AtMost'',''...''

{{math theorem
|Definition
| An assignment (or model) <math>\mathcal{A}</math> of a CSP <math>P = (\mathcal{X},\mathcal{D},\mathcal{C})</math> is defined by the couple <math>\mathcal{A} = (\mathcal{X_{\mathcal{A}}}, \mathcal{V_{\mathcal{A}}})</math> where:
* <math>\mathcal{X_{\mathcal{A}}} \subseteq \mathcal{X} </math> is a subset of variable;
* <math>\mathcal{V_{\mathcal{A}}} = \{ v_{\mathcal{A}_1}, \dots,  v_{\mathcal{A}_k}\} \in  \{ \mathcal{D}_{\mathcal{A}_1}, \dots, \mathcal{D}_{\mathcal{A}_k}\}</math> is the tuple of the values taken by the assigned variables.
}}

Assignment is the association of a variable to a value from its domain. A partial assignment is when a subset of the variables of the problem has been assigned. A total assignment is when all the variables of the problem have been assigned.

{{math theorem|Property|Given <math>\mathcal{A} = (\mathcal{X_{\mathcal{A}}}, \mathcal{V_{\mathcal{A}}})</math> an assignment (partial or total) of a CSP <math>P = (\mathcal{X},\mathcal{D},\mathcal{C})</math>, and <math>C_i = (\mathcal{X}_i, \mathcal{R}_i)</math> a constraint of <math>P</math> such as <math>\mathcal{X}_i \subseteq \mathcal{X_{\mathcal{A}}}</math>, the assignment <math>\mathcal{A}</math> satisfies the constraint <math>C_i</math> if and only if all the values <math>\mathcal{V}_{\mathcal{A}_i} = \{ v_i \in \mathcal{V}_{\mathcal{A}} \mbox{ such that } x_i \in \mathcal{X}_{i} \}</math> of the variables of the constraint <math>C_i</math> belongs to <math>\mathcal{R}_i</math>.
}}

{{math theorem
|Definition
|A solution of a CSP is a total assignment that satisfies all the constraints of the problem.}}

During the search of the solutions of a CSP, a user can wish for:

* finding a solution (satisfying all the constraints);
* finding all the solutions of the problem;
* [[automated theorem proving|proving]] the unsatisfiability of the problem.