Modélisation et résolution du problème des quatre cubes avec le solveur Choco 4 \cite{chocoSolver}.
\subsection{Constantes}
\label{sec:q1constantes}
Deux constantes sont définies dans l'énoncé du problème. Il s'agit du nombre de cubes $N$ ainsi que du nombre de faces $F$ sur le prisme rectangulaire. Ces deux constantes sont fixées à 4.
Afin de faciliter la création des contraintes dans le solveur Choco, on définit une application: l'ensemble de nombres $\lbrace1,2,3,4\rbrace$ sert à représenter l'ensemble de quatre couleurs $\lbrace rouge, vert, bleu, jaune \rbrace$, dans cet ordre \eqref{eq:q1mapping}.
\begin{align}
\label{eq:q1mapping}
\left\{
\begin{array}{lll}
1 &\mapsto&\text{Rouge}\\
2 &\mapsto&\text{Vert}\\
3 &\mapsto&\text{Bleu}\\
4 &\mapsto&\text{Jaune}
\end{array}
\right\}
\end{align}
\subsection{Variables}
\label{sec:q1variables}
On définit une matrice $FC$ de taille $N \times F$ où chaque variable $fc_{ij}$ correspond à la couleur que présente le cube $i$ sur la face $j$ du prisme rectangulaire.
\begin{align}
\label{eq:q1v1}
fc_{ij}&\in\lbrace 1,2,3,4 \rbrace&\forall 1 \leq i \leq N, 1 \leq j \leq F\\
dom(fc_{ij}) &= \lbrace 1,2,3,4 \rbrace\in\theta(1) &\forall 1 \leq i \leq N, 1 \leq j \leq F\nonumber
\end{align}
\subsubsection{Nombre total de variables et de valeurs}
\label{sec:q1nbtotvar}
Le nombre total de variables pour la définition \eqref{eq:q1v1}:
\begin{align}
\label{eq:q1vartot}
NF \in\theta(NF)
\end{align}
Le nombre total de valeurs possibles pour ces mêmes définitions est:
\begin{align}
\label{eq:q1valtot}
NF \times 4 &= 4NF \in\theta(NF)
\end{align}
\subsection{Contraintes}
\label{sec:q1contraintes}
\subsubsection{Tableaux des couleurs}
\label{sec:tableauCouleurs}
La contrainte du tableau des couleurs s'énonce comme suit: pour chaque cube $i$, un tableau doit être construit dans lequel seront énumérées toutes les séquences possibles des couleurs apparaissant sur les 4 faces du prisme. Pour chacun des 4 cubes, il y a 24 combinaisons (6 faces pointant dans une direction $\times$ 4 orientations par face) possibles. Si certaines combinaisons se répètent, ces doublons seront pris en charge par le solveur.
Il s'agit d'une contrainte de type \textsc{Tableau} qui s'écrit de la façon suivante :
\begin{align}
\label{eq:q1c1}
&\textsc{Tableau}(\lbrace fc_{i1},\dots,fc_{iF}\rbrace, T) &\forall 1 \leq i \leq N
\end{align}
\subsubsection{Couleurs différentes sur les 4 faces}
\label{sec:couleur4faces}
Le problème des 4 cubes consiste à trouver un agencement de ces cubes permettant d'obtenir chacune des 4 couleurs sur les 4 faces rectangulaires du prisme créé. Ce qui équivaut à ne pas avoir une paire de couleurs identiques sur une face latérale du prisme \eqref{eq:q1c2eq}.
\begin{align}
\label{eq:q1c2eq}
&fc_{ij_1}\neq fc_{ij_2}&\forall 1 \leq i \leq N, 1 \leq j_1 < j_2 \leq F\\
\end{align}
Il s'agit d'une contrainte de type \textsc{AllDifferent}\eqref{eq:q1c2} pour chaque face latérale du prisme.
\begin{align}
\label{eq:q1c2}
\textsc{AllDifferent}(\lbrace fc_{i1},\ldots, fc_{iF}\rbrace ) &\forall 1 \leq i \leq N
\end{align}
\subsubsection{Nombre total de contraintes}
\label{sec:q1totcontr}
Le nombre total de contraintes pour les définitions \eqref{eq:q1c1} et \eqref{eq:q1c2} est:
N \text{contraintes «tableau»} + \frac{4*N(N-1)}{2}\text{contraintes de différence}&= 2N^{2}-N \in\theta(N^{2})
\end{align}
\begin{center}
De plus, chaque tableau contient au plus 24 $\in O(24)$ entrées.
\end{center}
\subsection{Résultats}
\label{sec:q1resultats}
Nous avons demandé au solveur Choco de trouver une solution au problème des 4 cubes à l'aide de la méthode \texttt{findSolution}. Nous avons utilisé les euristiques par défaut, car elles permettaient d'obtenir un résultat en moins d'une seconde. Le solveur trouve une seule solution en n'effectuant aucun retour arrière, et ce en 0,038s.
