\chapter{Modellazione}\label{chapModellazione}

In seguito all'analisi dei requisiti vengo estrapolati due modelli differenti candidati a modellare il problema in esame: il \textit{Modello a Matrice Multidimensionale} e il \textit{Modello a Slot}.\\
La scelta definitiva di adottare un modello a scapito di un altro è dovuta sia alla possibilità di modellare un numero superiore di vincoli che a performance di calcolo più efficienti.
\section{Modello a Matrice Multidimensionale v1}
\subsection{Modellazione formale}
Variabili:
\begin{itemize}
\item\textit{Insegnamenti} indice \(\mathrm{i} \in \left[1,\mathrm{nIns}\right] = \mathrm{I}\), I è l'insieme di tutti gli Insegnamenti del modello\footnote{Comprende sia gli Insegnamenti da allocare che quelli già allocati e assunti come vincoli per il modello}.
\item\textit{Docenti} indice \(\mathrm{d} \in \left[1,\mathrm{nDoc}\right] = \mathrm{D}\), D è l'insieme di tutti i Docenti\footnote{I Docenti presi in considerazione sono solo quelli che si riferiscono ad almeno uno Slot.}.
\item\textit{Giorno} indice \(\mathrm{g} \in \left[1,6\right] = \mathrm{G}\), G è l'insieme delle fasce orarie allocabili dedotto dai requisiti.
\item\textit{Fascia oraria} indice \(\mathrm{f} \in \left[1,7\right] = \mathrm{F}\), F è l'insieme delle fasce orarie allocabili dedotto dai requisiti.
\item Insieme di variabili Booleane \(\mathrm{mat}_{\mathrm{i,d,g,f}} \in \{0,1\}\) destinate all'allocazione con cardinalità \(|I|\times |D|\times |G|\times |F|\)\footnote{L'ordine di grandezza del problema oggetto di Tesi risulta essere approssimativamente: \(200*300*6*7=2.52*10^6\).}:
\end{itemize}
\hspace{2ex}mat_{i,d,g,f} =
$\begin{cases}
1\text{, slot dell'Insegnamento \textit{i} allocato per il Docente \textit{d}}\\
0\text{, slot dell'Insegnamento \textit{i} non allocato per il Docente \textit{d}\footnote{Potrebbe essere allocato per altri Docenti.}}
\end{cases}$
\\\\\FloatBarrier
Funzioni:
\begin{itemize}
\item Insegnamenti di un Docente: una funzione \textit{assignDocente(d)} stabilisce gli Insegnamenti assegnati ad un Docente\footnote{Semplificazione nei vincoli in cui si considera che tutti gli Slot di un Insegnamento siano tenuti dagli stessi Docenti}:
\begin{equation}
\begin{split}
    &\textit{assignDocente}: D \rightarrow 2^I\\
    &d \mapsto I_d \subseteq I
\end{split}
\end{equation}

\item Indisponibilità di un Docente: una funzione \textit{indispDocente(d)} stabilisce gli slot orari in cui un Docente è impossibilitato a svolgere lezione:
\begin{equation}
    \begin{split}
        &\textit{indispDocente}: D \rightarrow 2^{G\times F} \\
        &d \mapsto \{\left(\mathrm{g,f}\right)\} \subseteq G\times F
    \end{split}
\end{equation}

\item Preferenza di un Docente: una funzione \textit{prefDocente(d)} stabilisce gli slot orari in cui un Docente vuole fare lezione:
\begin{equation}
    \begin{split}
        &\textit{prefDocente}: D \rightarrow 2^{G\times F}\\
        &d \mapsto \{\left(\mathrm{g,f}\right) \} \subseteq G \times F
    \end{split}
\end{equation}

\item Numero di Slot di un Insegnamento: una funzione \textit{numSlot(i)} stabilisce il numero di slot orari da 1.5h settimanali per un Insegnamento:
\begin{equation}
    \begin{split}
        &\textit{numSlot}: I \rightarrow \mathbb{N}\\
        &i \mapsto n_i \in \mathbb{N}
    \end{split}
\end{equation}

\item Max slot orari Docente giornalieri: una funzione \textit{maxSlotDocente(d)} restituisce il numero massimo di slot orari di 1.5h allocabili per un singolo Docente:
\begin{equation}
    \begin{split}
        &\textit{maxSlotDocente}: D \rightarrow \mathbb{N}\\
        &d \mapsto d_i \in \mathbb{N}
    \end{split}
\end{equation}

\item Slot di un Insegnamento: una funzione \textit{slotInsegnamento(i)} stabilisce gli slot orari allocati per un Insegnamento:
\begin{equation}
    \begin{split}
        &\textit{slotInsegnamento}: I \rightarrow 2^{G\times F}\\
        &i \mapsto \{\left(g,f\right)\} \subseteq G \times F
    \end{split}
\end{equation}

\item Slot scelto per un Insegnamento: una funzione \textit{slotScelti(i)} ritorna gli slot orari in cui un Insegnamento deve essere necessariamente tenuto\footnote{Non necessariamente tutti gli Slot di un Insegnamento sono preallocati.}:
\begin{equation}
    \begin{split}
        &\textit{slotScelti}:  I \rightarrow 2^{G\times F}\\
        &i \mapsto \{\left(g,f\right)\} \subseteq \textit{slotInsegnamento(i)}
    \end{split}
\end{equation}

\item Docenti di un Insegnamento: una funzione \textit{docentiIns(i)} ritorna i Docenti associati ad un Insegnamento:
\begin{equation}
    \begin{split}
      &\textit{docentiIns}: I \rightarrow 2^D\\
      &i \mapsto D_i \subseteq D
    \end{split}
\end{equation}

\end{itemize}

Vincoli:
\begin{itemize}
\item Non è possibile assegnare lezioni in slot orari dove i Docenti hanno indicato incompatibilità:
\begin{align} 
d \in D, \forall \left(g,f\right) \in \textit{indispDocente(d)}, \forall i \in I: mat_{i,d,g,f} = 0
\end{align}

\item Non viene assegnato ad un Docente uno slot orario riferito ad un Insegnamento in cui lui non tiene lezioni:
\begin{align} d \in D, \forall i \notin \textit{assingDocente(d)},\forall g \in G, \forall f \in F: mat_{i,d,g,f} = 0
\end{align}

\item Non vengono allocati sovrapposti due Slot appartenenti allo stesso Docente:
\begin{align}
d \in D, Idoc := \textit{assignDocente(d)}, \forall g \in G, \forall f \in F, \sum_{i \in Idoc} mat_{i,d,g,f} <= 1
\end{align}

\item Viene allocato uno Slot negli slot orari in cui il Docente ha espresso preferenza:
\begin{equation}
    \begin{gathered}
     d \in D, Idoc := \textit{assignDocente(d)},\\
     \forall \left(g,f\right) \in \textit{prefDocente(d)}, \sum_{i \in Idoc} mat_{i,d,g,f} = 1
    \end{gathered}
\end{equation}

\item Limite massimo di slot orari allocati per Docente:
\begin{equation}
    \begin{gathered}
    d \in D, Idoc := \textit{assignDocente(d)}, \forall g \in G,\\
    \sum_{i \in Idoc, f \in F} mat_{i,d,g,f} <=  \textit{maxSlotDocente(d)}
    \end{gathered}
\end{equation}

\item Gli Slot Scelti vanno preallocati:
\begin{equation}
    \begin{gathered}
    i \in I, \forall \left(g,f\right) \in \textit{slotScelti(i)},\\
    \forall \text{ } d \in \textit{docentiIns(i)}, \text{ } mat_{i,d,g,f} = 1
    \end{gathered}
\end{equation}

\item Si alloca esattamente il numero di slot orari richiesto per un Insegnamento:
\begin{equation}
    \begin{gathered}
    i \in I, d \in \textit{docentiIns(i)},\\
    \sum_{g \in G, f \in F} mat_{i,d,g,f} = \textit{numSlot(i)}
    \end{gathered}
\end{equation}

\item Si allocano tutti i Docenti relativi all'Insegnamento qualora venga allocato uno Slot per tale Insegnamento:
\begin{equation}
    \begin{gathered}
    i \in I, g \in G, f \in F, d \in \textit{docentiIns(i)}, \\
    mat_{i,d,g,f} = 1 \Rightarrow mat_{i,d^*,g,f} = 1 \text{ } \forall d^* \in \textit{docentiIns(i)}
    \end{gathered}
\end{equation}

\item Slot appartenenti allo stesso Insegnamento contigui se allocati lo stesso giorno\footnote{Se per un dato Insegnamento un certo slot orario è allocato è il successivo no, allora non potrò avere slot successivi allocati nello stesso giorno.}:
\begin{equation}
    \begin{gathered}
    i \in I, d \in \textit{docentiIns(i)}, g \in G, f1 \in F,\\
    \sum_{0 \leq f < f1} mat_{i,d,g,f} = \sum_{0 \leq f \leq f1} mat_{i,d,g,f} \Rightarrow \sum_{f \in F}mat_{i,d,g,f} = \sum_{0 \leq f < f1} mat_{i,d,g,f}
    \end{gathered}
\end{equation}
Che può essere tradotta in:
\begin{equation}
    \begin{gathered}
    i \in I, d \in \textit{docentiIns(i)}, g \in G,\\
    \forall f1, \text{ } 0 \leq f1 <  F-1, \text{ se: } mat_{i,d,g,f1} = 1 \wedge mat_{i,d,g,f1+1} = 0 \Rightarrow\\
    \sum_{0 \leq f2 \leq f1}mat_{i,d,g,f2} = \sum_{f \in F} mat_{i,d,g,f}
    \end{gathered}
\end{equation}

\end{itemize}



\subsection{Modellazione con equazioni}
Per la modellazione di basso livello si utilizza il software Z3 ed in particolare le sue API per Python. Di seguito vengono riportare le equazioni corrispondenti ai vincoli precedentemente discussi, per scelta stilistica si decide di collassare le due dimensioni fasciaOraria F e giorno G in un unica chiamata S avente cardinalità \(6\times 7=42\).\\\\
Matrice booleana \(mat_{i,d,g,f} \rightarrow mat_{i,d,s}, \text{ }s \in S\) è l'insieme di tutti gli slot orari.
\FloatBarrier
\begin{lstlisting}
# Insegnamenti X Docenti X Slot
mat = [[[z3.Bool("ins_%s doc_%s slot_%s" % (insegnamenti[i], docenti[d], slot[s]))
            for s in range(len(slot))]
            for d in range(len(docenti))] 
            for i in range(len(insegnamenti))]

I = len(insegnamenti)
D = len(docenti)
G = 6
F = 7
S = G*F
eqs = list()
\end{lstlisting}
\FloatBarrier

Equazioni:
\begin{itemize}
\item Non è possibile assegnare lezioni in slot orari dove i Docenti hanno indicato incompatibilità:
\FloatBarrier
\begin{lstlisting}
for d in range(D):
    for s in range(S):
        if s in indispDocente(d):
            eqs.append(mat[i][d][s] == False)
\end{lstlisting}
\FloatBarrier
\item Non viene assegnato ad un Docente uno slot orario riferito ad un Insegnamento in cui lui non tiene lezioni:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    for d in range(D):
        if d not in assignDocente(d):
            for s range(S):
                eqs.append(mat[i][d][s] == False)
\end{lstlisting}
\FloatBarrier
\item Non vengono allocati sovrapposti due Slot appartenenti allo stesso Docente:
\FloatBarrier
\begin{lstlisting}
for d in range(D):
    for s in range(S):
        eqs.append(Sum([If(mat[i][d][s], 1, 0) for i in range(I)]) <= 1))
\end{lstlisting}
\FloatBarrier
\item Viene allocato uno Slot negli slot orari in cui il Docente ha espresso preferenza:
\FloatBarrier
\begin{lstlisting}
for d in range(D):
    for s in prefDocente(d):
        eqs.append(Sum([If(mat[i][d][s], 1, 0) for i in assignDocente(d)]) == 1)
\end{lstlisting}
\FloatBarrier
\item Limite massimo di slot orari allocati per Docente:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    for d in range(D):
        for g in range(G):
            eqs.append(Sum([If(mat[i][d][g*F+f], 1, 0) for f in range(F)]) <= maxSlotDocente(d))
\end{lstlisting}
\FloatBarrier
\item Gli Slot Scelti vanno preallocati:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    for s in slotScelti(i):
        for d in docentiIns(i):
            eqs.append(mat[i][d][s] == True)
\end{lstlisting}
\FloatBarrier
\item Si alloca esattamente il numero di slot orari richiesto per un Insegnamento:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    d = docentiIns(i)[0]
    eqs.append(Sum([If(mat[i][d][s], 1, 0) for s in range(S)]) == numSlot(i))
\end{lstlisting}
\FloatBarrier
\item Si allocano tutti i Docenti relativi all'Insegnamento qualora venga allocato uno Slot per tale Insegnamento:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    for s in range(S):
        d = docentiIns(i)[0]
        for d_ in docentiIns(i)[1:]:
            eqs.append(Implies(mat[i][d][s], mat[i][d_][s] == True))
\end{lstlisting}
\FloatBarrier
\item Slot appartenenti allo stesso Insegnamento contigui se allocati lo stesso giorno:
\FloatBarrier
\begin{lstlisting}
for i in range(I):
    d = docentiIns(i)[0]
    for g in range(G):
        for f in range(F-1):
            eq = Implies(And(mat[i][d][g*F+f], Not(mat[i][d][g*F+f+1])),
                    Sum([If(mat[i][d][g*F+f1], 1, 0) for f1 in range(f+1)]) == Sum([If(mat[i][d][g*F+f2], 1, 0) for f2 in range(F)]))
            eqs.append(eq)
\end{lstlisting}
\FloatBarrier
\end{itemize}
\subsection{Conclusioni}
Questo modello presenta numerosi punti critici tra cui:
\begin{itemize}
\item Non tiene conto della dimensione Aule.
\item Suppone che tutti gli Slot di un Insegnamento siano uguali tra loro e quindi riferiti agli stessi Docenti.
\item Non si tiene conto di nessun vincolo tra Slot dello stesso Insegnamento.
\item Non si tiene conto di nessuna preferenza/penalità\footnote{Si ignorano tutti i soft constraint.}.
\item Non vengono presi in considerazione gli Insegnamenti che non possono essere sovrapposti tra loro a causa della loro appartenenza allo stesso Orientamento.
\end{itemize}
Si rende quindi necessaria la modellazione di una versione più precisa partendo da quella presa in esame ora.

\section{Modello a Matrice Multidimensionale v2}
\subsection{Modellazione formale}
Variabili (oltre a quelle precedentemente definite):
\begin{itemize}
\item \textit{Slot} indice s \(\in \left[1,\mathrm{nSlotIns} \right] = S_i\), sono gli Slot dell'Insegnamento I.
\item \textit{Aule} indice a \(\in \left[1,\mathrm{nAule} \right] = A\), è l'insieme delle Aule allocabili.
\item Ridefinizione dell'insieme di variabili Booleane \(\mathrm{mat}_{s,d,a,g,f} \in \{0,1\}\) con cardinalità \(|S|\times |D|\times  |A|\times |G|\times |F|\)\footnote{L'ordine di grandezza risultante corrisponde a \(600*300*60*6*7\cong 4.53*10^{8}\).}:
\end{itemize}
\hspace{2ex}mat_{i,d,g,f} =
$\begin{cases}
1\text{, slot allocato per il Docente \textit{d}} nell'Aula \textit{a}\\
0\text{, altrimenti}.
\end{cases}$
\\\\\FloatBarrier
\subsection{Conclusioni}
Prima di passare a definire i vincoli del nuovo modello si preferisce verificare le performance del software Z3 dato l'aumento di 2 ordini di grandezza delle dimensioni del problema.
\FloatBarrier
\begin{lstlisting}
# Slot_Insegnamenti X Docenti X Aule X Slot_Orari
mat = [[[z3.Bool("slotIns_%s doc_%s aula_%s slotOrario_%s" % (slotIns[si], docenti[d], aule[a], slotOrario[so]))
            for so in range(len(slotOrario))]
            for a in range(len(aule))]
            for d in range(len(docenti))] 
            for si in range(len(slotIns))]

I = len(slotIns)
D = len(docenti)
A = len(aule)
G = 6
F = 7
S = G*F
eqs = list()
\end{lstlisting}
\FloatBarrier
L'allocazione di tale matrice richiede troppe risorse\footnote{Da prove sperimentali è emerso come 64 GB di memoria non risultino sufficienti ad allocare il problema, non si hanno informazioni a sufficienza per stimare con attendibilità le risorse effettivamente richieste.}, ragione per cui si è deciso di utilizzare un modello completamente diverso.

\section{Modello a Slot}
\subsection{Modellazione formale}
Variabili:
\begin{itemize}
\item Slot indice \(s \in \left[1,\mathrm{nSlots}\right] = S\), S è l'insieme di tutti gli Slot del modello.
\item Insegnamenti indice \(i \in \left[1,\mathrm{nIns}\right] = I\), I è l'insieme di tutti gli Insegnamenti del modello\footnote{Comprende sia gli Insegnamenti da allocare che quelli già allocati e assunti come vincoli per il modello.}.
\item Orientamenti indice \(o \in \left[1,\mathrm{nOrient}\right] = O\), O è l'insieme di tutti gli Orientamenti del modello.
\item Docenti indice \(d \in \left[1,\mathrm{nDoc}\right] = D\), D è l'insieme di tutti i Docenti\footnote{I Docenti presi in considerazione sono solo quelli che si riferiscono ad almeno uno Slot.}.

\item \(\mathrm{N\_GIORNI}=6, \mathrm{N\_FASCE\_ORARIE}=7\).
\item Giorno indice \(g \in \left[0,\mathrm{N\_GIORNI}\right] = G\), G è l'insieme dei giorni. 
\item Giorno Slot \(X\_d_s \in \left[0,\mathrm{N\_GIORNI}\right]\).
\item Fascia oraria indice \(f \in \left[0,\mathrm{N\_FASCE\_ORARIE}\right] = F\), F è l'insieme delle fasce orarie.
\item Fascia oraria Slot \(X\_h_s \in \left[0,\mathrm{N\_FASCE\_ORARIE}\right]\).

\item Penalità Insegnamenti indice \(p \in \left[1,\mathrm{nPenalita}\right] = P\), P è l'insieme di tutte le penalità riguardanti la sovrapposizione di Insegnamenti dello stesso Orientamento e per vincoli riguardanti un Insegnamento nel modello.
\item Penalità per sovrapposizione Insegnamenti dello stesso Orientamento e per vincoli riguardanti un Insegnamento \(X\_penalties_p \in \left[0,..,7\right]\).
\item Penalità studenti indice \(pStud \in \left[1,\mathrm{nPenalitaStudenti}\right] = \mathrm{P\_STUD}\), P\_STUD è l'insieme di tutte le penalità riguardanti gli studenti nel modello.
\item Penalità studenti \(X\_penaltiesStud_{pStud} \in \left[-7,..0,..,7\right]\).
\item Penalità per preferenze/indisponibilità Docenti indice \(pDoc \in \\\left[1, \mathrm{nPenalitaDocenti}\right] = P\_DOC\), P\_DOC è l'insieme di tutte le penalità riguardanti i Docenti nel modello.
\item Penalità Docenti \(X\_penaltiesDoc_{pDoc} \in \left[-7,..,0,..,7\right]\).
\item Funzione obiettivo\footnote{Il software è configurabile al fine di scegliere come funzione obiettivo anche un sottoinsieme dei termini di somma presenti.}:
\begin{dmath}\label{funObiettivo}
min\left(\sum_{p \in P}X\_penalties_p + \sum_{pStud \in P\_STUD}X\_penaltiesStud_{pStud} + \sum_{pDoc \in P\_DOC}X\_penaltiesDoc_{pDoc} \right)
\end{dmath}
\item Slot orari del sabato: \textit{SlotSabato()}.
\item Slot orari allocati per ogni Anno Accademico per ogni Orientamento indice \(a,o, a \in \left[1,3\right], o \in\left[1,\mathrm{nOrient}\right] = \mathrm{X\_ORIENT}\) è l'insieme di tutti gli slot orari allocati per ogni Anno Accademico dei diversi Orientamenti.
\item Slot orari allocati per ogni Anno Accademico per ogni Orientamento\footnote{Vengono raggruppati insieme i PeriodiDidattici dello stesso anno accademico.} \( X\_orient_{o,a,g,f} \in \left[0,1\right] \).

\end{itemize}

Funzioni:
\begin{itemize}
\item Numero di slot orari di uno Slot: una funzione \textit{numSlot(s)} ritorna il numero di slot orari da 1.5h consecutivi dello Slot:
\begin{equation}\label{funNumSlot}
\begin{split}
&\textit{numSlot}: S \rightarrow \mathbb{N}\\
&s \mapsto n_s \in \mathbb{N}
\end{split}
\end{equation}

\item Tipologia di lezione di uno Slot: una funzione \textit{tipoLez(s)} ritorna il TipoLezione associato allo Slot:
\begin{equation}
\begin{split}
    &TipoLezione = \{\mathrm{L, EL, EA, L\_EA}\}\\
    &\textit{tipoLez}: S \rightarrow TipoLezione\\
    &s \mapsto tipoLezione_s \in TipoLezione
\end{split}
\end{equation}

\item Docenti associati ad uno Slot: una funzione \textit{docentiSlot(s)} ritorna i Docenti associati ad uno Slot:
% \todo[inline]{come si indica una lista di Docenti? Così è ok anche se non ho una matrice di fatto? Va bene l'allineamento delle eq multiline?}
\begin{equation}
\begin{split}
    &\textit{docentiSlot}: S \rightarrow 2^D\\
    &s \mapsto D_s \subseteq D
\end{split}
\end{equation}

\item Max slot orari Docente giornalieri: una funzione \textit{maxSlotDocente(d)} stabilisce il numero massimo di slot orari di 1.5h allocabili per un singolo Docente:
\begin{equation}
    \begin{split}
        &\textit{maxSlotDocente}: D \rightarrow \mathbb{N}\\
        &d \mapsto i_d \in \mathbb{N}
    \end{split}
\end{equation}

\item Slot di un Insegnamento: una funzione \textit{slotInsegnamento(i)} stabilisce gli slot orari allocati per un Insegnamento:
\begin{equation}
    \begin{split}
        &\textit{slotInsegnamento}: I \rightarrow 2^S\\
        &i \mapsto \{S_i\} \subseteq S
    \end{split}
\end{equation}

\item Slot scelto per un Insegnamento: una funzione \textit{slotScelti(i)} ritorna gli Slot preallocati di un Insegnamento \footnote{Non necessariamente tutti gli Slot di un Insegnamento sono preallocati.}:
\begin{equation}\label{funSlotScelti}
    \begin{split}
        &\textit{slotScelti}:  I \rightarrow 2^{S}\\
        &i \mapsto \{S_i\} \subseteq \textit{slotInsegnamento(i)}
    \end{split}
\end{equation}

\item Giorno e Fascia oraria di uno SlotScelto: una funzione \textit{detailsSlotScelto(s)} ritorna Giorno e Fascia oraria di uno SlotScelto:
\begin{equation}\label{funDetailsSlotScelto}
\begin{split}
    &\textit{detailsSlotScelto}: S \rightarrow 2^{G\times F}\\
    &s \mapsto \{(g,f)\} \subseteq G \times F
\end{split}
\end{equation}

\item Slot tenuti da un Docente: una funzione \textit{slotDocente(d)} restituisce gli Slot allocati per un dato Docente:
\begin{equation}\label{funSlotDocente}
    \begin{split}
    &\textit{slotDocente}: D \rightarrow 2^S\\
    &d \mapsto \{S_d\} \subseteq S
    \end{split}
\end{equation}

\item Insegnamenti in un Orientamento: una funzione \textit{insOrientamento(o)} restituisce gli Insegnamenti per un dato Orientamento:
\begin{equation}\label{funInsOrientamento}
    \begin{split}
    &\textit{insOrientamento}: O \rightarrow 2^I\\
    &o \mapsto \{I_o\} \subseteq I
    \end{split}
\end{equation}

\item Squadra di uno Slot (se presente): una funzione \textit{squadraSlot(s)} ritorna la squadra associata allo Slot (se presente):
\begin{equation}\label{funSquadraSlot}
\begin{split}
    &\textit{squadraSlot}: S \rightarrow Squadra\\
    &s \mapsto squadra_s \in Squadra\\\\
    Squadra = &\{\mathrm{NoSquadra, Squadra\_1, Squadra\_2,}\\&\mathrm{Squadra\_3, Squadra\_4}\}
\end{split}
\end{equation}

\item TipoSlot: una funzione \textit{tipoSlot(s)} ritorna il tipo di Slot:
\begin{equation}\label{funTipoSlot}
\begin{split}
    &\textit{tipoSlot}: S \rightarrow TipoSlot\\
    &s \mapsto tipoSlot_s \in TipoSlot\\\\
    TipoSlot =&\{\mathrm{SlotScelto, SlotGenerico, SlotScelto\_giorno,} \\&\mathrm{SlotScelto\_fasciaOraria}\}
\end{split}
\end{equation}

\item PeriodoDidattico di un Insegnamento all'interno di un Orientamento: una funzione \textit{periodoDidattico(i, o)} ritorna il periodoDidattico:
\begin{equation}\label{funPeriodoDidatticoIns}
\begin{split}
    &\textit{periodoDidattico}: (I,O) \rightarrow PeriodoDidattico\\
    &i,o \mapsto periodoDidattico_{i,o} \in PeriodoDidattico\\\\
    &PeriodoDidattico = \{\mathrm{PrimoAnno\_PrimoSemestre,} \\&\mathrm{PrimoAnno\_SecondoSemestre, SecondoAnno\_PrimoSemestre,}\\
    &\mathrm{SecondoAnno\_SecondoSemestre, TerzoAnno\_PrimoSemestre,} \\&\mathrm{TerzoAnno\_SecondoSemestre}\}
\end{split}
\end{equation}

\item Alfabetica di un Insegnamento all'interno di un Orientamento: una funzione \textit{alfabetica(i, o)} ritorna l'alfabetica:
\begin{equation}\label{funAlfabeticaIns}
\begin{split}
    &\textit{alfabetica}: (I,O) \rightarrow Alfabetica\\
    &i,o \mapsto alfabetica{i,o} \in Alfabetica\\\\
    Alfabetica &= \{\mathrm{NoAlfabetica, PrimaAlfabetica,} \\&\mathrm{SecondaAlfabetica, TerzaAlfabetica}\}
\end{split}
\end{equation}

\item Penalita sovrapposizione: una funzione \textit{penalitaSovr(i1,i2,o)} ritorna il livello di penalità da aggiungere al modello in caso di sovrapposizione di due Insegnamenti i1 e i2 per l'Orientamento o\footnote{Dato che un Insegnamento può essere parte di più Orientamenti è possibile che in differenti Orientamenti la penalità del sovrapporsi degli stessi Insegnamenti assuma un valore differente.}:
\begin{equation}\label{funGetPenalitaInsInOrientamento}
\begin{split}
&\textit{penalitaSovr}: (I^2,O) \rightarrow LV\_Penalties\\
&i1,i2,o \mapsto penalita_{i1,i2,o} \in LV\_Penalties\\\\
LV\_Penalties & = \{\mathrm{LV\_H,LV\_0,LV\_1,LV\_2,LV\_3,}\\&\mathrm{LV\_4,LV\_5,LV\_6,LV\_MAX} \}
\end{split}
\end{equation}

\item Insegnamenti di un Orientamento in un dato Anno Accademico: una funzione \textit{insInAnnoOrientamento(o,a)} ritorna gli Insegnamenti di un Orientamento in un dato Anno Accademico:
\begin{equation}\label{funAnnoAccademicoIns}
\begin{split}
    &\textit{insInAnnoOrientamento}: (O,A) \rightarrow 2^I\\
    &o,a \mapsto \{I_{o,a}\} \subseteq \textit{insOrientamento(O)}\\\\
    &A = \{1,2,3\}
\end{split}
\end{equation}

\item Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito un Orientamento in un dato Anno Accademico: una funzione \textit{kernelInsInAnnoOrientamento(o,a)} ritorna gli Insegnamenti di un Orientamento in un dato Anno Accademico:
\begin{equation}\label{funAnnoAccademicoInsObb}
\begin{split}
    &\textit{kernelInsInAnnoOrientamento}: (O,A) \rightarrow 2^I\\
    &o,a \mapsto \{I_{o,a}\} \subseteq \textit{insOrientamento(O)}\\\\
    &A = \{1,2,3\}
\end{split}
\end{equation}

\item Numero di Locali disponibili per un dato tipo e una data capienza: una funzione \textit{numLocaliDisponibili(g,f,l,c)} ritorna il numero di Locali di tale tipo e capienza\footnote{Se valorizzabile per il tipo di Locale corrente.} disponinili in uno slot orario\footnote{Esiste una funzione analoga che considera solo i Locali dotati di prese elettriche.}:
\begin{equation}\label{funLocaliDisponibili}
\begin{split}
    &\textit{numLocaliDisponibili}: (G,F,L,C) \rightarrow \mathbb{N}\\
    &g,f,l,c \mapsto \mathbb{N}\\\\
    L = \{&\mathrm{Aula,LABINF,LAIB,LADISPE,LED,LED1,}\\&\mathrm{LED2,ACSLAB,Aula5T,Aula\_CA2,}\\
    &\mathrm{Aula\_CA,Aula\_TB,Aula\_WB} \}\\
    C = \{&\mathrm{Piccola,Media,MedioGrande,Grande}\}
\end{split}
\end{equation}

\item Tipo di Locale di uno Slot: una funzione \textit{tipoLocale(s)} restituisce il tipoLocale di uno Slot:
\begin{equation}\label{funTipoLocale}
\begin{split}
    &\textit{tipoLocale}: (S) \rightarrow L\\
    &s \mapsto tipoLocale \in L
\end{split}
\end{equation}

\item Capienza del Locale associato ad uno Slot: una funzione \textit{capienzaLocale(s)} restituisce la capienza del locale associato ad uno Slot:
\begin{equation}\label{funCapienzaLocale}
\begin{split}
    &\textit{capienzaLocale}: (S) \rightarrow C\\
    &s \mapsto capienza \in C
\end{split}
\end{equation}


\end{itemize}

Vincoli:
\begin{itemize}
\item Gli Slot devono essere assegnati in fasce orarie e gioni validi:
\begin{align}\label{eqDominio}
s \in S, \text{ } 0\leq X\_d_s \leq |G| \text{ }\wedge\text{ } 0\leq X\_h_s \leq |F|-\textit{numSlot(s)} 
\end{align}

\item Al Sabato sono disponibili meno fasce orarie:
\begin{align}\label{eqDominioSabato}
s \in S, se: X\_d_s = |G|-1 \Rightarrow X\_h_s + \textit{numSlot(s)} \leq  \textit{SlotSabato()}
\end{align}

\item Slot appartenenti allo stesso Insegnamento se allocati lo stesso giorno, tenuti da uno o più Docenti in comune e non Esercitazioni di Laboratorio devono essere consecutivi:
\begin{equation}\label{eqSlotSameInsSameDocConsec}
\begin{gathered}
i \in I, \forall s1,s2 \in \textit{slotInsegnamento(i)}, s1\neq s2,\\
se: \textit{docentiSlot(s1)} \cap \textit{docentiSlot(s2)} \neq \emptyset \text{ } \land\\ (\textit{tipoLez(s1)} \neq EL \lor \textit{tipoLez(s2)} \neq EL) \land\\
X\_d_s1 = X\_d_s2\Rightarrow\\
(X\_h_{s1} = X\_h_{s2}+\textit{numSlot(s2)}) \lor (X\_h_{s2} = X\_h_{s1}+\textit{numSlot(s1)})
\end{gathered}
\end{equation}

\item Docente allocato in un solo slot orario alla volta:
\begin{equation}\label{eqDocUnSoloSlotAllaVolta}
\begin{gathered}
d \in D, \forall s1,s2 \in \textit{slotDocente(d)}, s1\neq s2,\\
se: X\_d_{s1} = X\_d_{s2} \Rightarrow \\
(X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)}) \lor (X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)})
\end{gathered}
\end{equation}

\item Se uno Slot di un Insegnamento è termina alle 19.00 di un dato giorno, il giorno successivo alle 8.30 non potrà esserci un altro Slot dello stesso Insegnamento a meno di esercitazioni di laboratorio o di lezioni suddivise per squadre\footnote{La stessa equazione è implementata anche invertendo s1 e s2.}:
\begin{equation}\label{eqSlotInsGiornoDopoNonSubito}
\begin{gathered}
i \in I, \forall s1,s2 \in \textit{slotInsegnamento(i)}, s1 \neq s2,\\
se: \textit{tipoLez(s1)} \neq EL \text{ }\land \textit{tipoLez(s2)} \neq EL\text{ } \land\\
\textit{squadraSlot(s1)} \neq NoSquadra \text{ } \land \textit{squadraSlot(s2)} \neq NoSquadra \text{ } \land\\
X\_d_{s1}+1 = X\_d_{s2} \land X\_h_{s2}+\textit{numSlot(s2)}=7\\
\Rightarrow X\_h_{s1} > 0
\end{gathered}
\end{equation}

\item Slot di un Insegnamento non sovrapposti se non si tratta di Slot relativi a squadre differenti\footnote{Viene considerata la non intersezione tra i Docenti titolari dei differenti Slot poichè in tal caso si cadrebbe nel vincolo descritto dalla \eqref{eqSlotSameInsSameDocConsec}.}:
\begin{equation}\label{eqSlotInsNonSovrapposti}
\begin{gathered}
i \in I, \forall s1,s2 \in \textit{slotInsegnamento(i)}, s1 \neq s2,\\
se: \textit{docentiSlot(s1)} \cap \textit{docentiSlot(s2)} = \emptyset \text{ } \land\\
\textit{squadraSlot(s1)} \neq NoSquadra \land \textit{squadraSlot(s2)} \neq NoSquadra \text{ } \land\\
\textit{squadraSlot(s1)} \neq \textit{squadraSlot(s2)} \land X\_d_s1 = X\_d_s2\Rightarrow\\
(X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)} \lor X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)})
\end{gathered}
\end{equation}

\item Slot scelti di un Insegnamento:

\begin{equation}\label{eqSlotScelti}
\begin{gathered}
i \in I, \forall s \in \textit{slotScelti(i)} \Rightarrow\\
X\_d_s = \textit{detailsSlotScelto(s)}.g \land X\_h_s = \textit{detailsSlotScelto(s)}.f
\end{gathered}
\end{equation}

\item Slot di Insegnamenti appartenenti allo stesso Orientamento non possono sovrapporsi come soft o hard constraint seguendo la Tabella \ref{table:tabPenalitaInsInOrient}:
\begin{equation}\label{eqPenalitaInOrientamentoHeader}
\begin{gathered}
o \in O, \forall i1,i2 \in \textit{insOrientamento(o)}, i1 \neq i2,\\
\forall s1 \in \textit{slotInsegnamento(i1)}, \forall s2 \in \textit{slotInsegnamento(i2)},\\
se: \textit{periodoDidattico(i1,o)} = \textit{periodoDidattico(i2,o)} \text{ } \land \\ 
(\textit{alfabetica(i1,o)} = \textit{alfabetica(i2,o)} \text{ }\lor\\ \textit{alfabetica(i1,o)} = NoAlfabetica \lor \textit{alfabetica(i2,o)} = NoAlfabetica) \text{ } \land \\
(\textit{squadraSlot(s1)} = NoSquadra \text{ }\lor\\ \textit{squadraSlot(s2)} = NoSquadra \lor \textit{squadraSlot(s1)} = \textit{squadraSlot(s2)}) \text{ }
\end{gathered}
\end{equation}
\begin{equation}\label{eqPenalitaInOrientamentoHard}
\begin{gathered}
\eqref{eqPenalitaInOrientamentoHeader} \text{ } \land \textit{penalitaSovr(i1,i2,o)} = LV\_H \land X\_d_{s1} = X\_d_{s2}\Rightarrow \\
(X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)} \lor X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)})
\end{gathered}
\end{equation}
\begin{equation}\label{eqPenalitaInOrientamentoSoft}
\begin{gathered}
\eqref{eqPenalitaInOrientamentoHeader} \text{ } \land \textit{penalitaSovr(i1,i2,o)} \neq LV\_H \land X\_d_{s1} = X\_d_{s2} \text{ } \land \\
\neg(X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)}) \text{ } \land \\
\neg(X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)}) \Rightarrow\\
X\_penalties_{s1,s2,o} = \textit{penalitaSovr(i1,i2,o)}
\end{gathered}
\end{equation}
Vengono aggiunte al modello le Equazioni \eqref{eqPenalitaInOrientamentoHard} e \eqref{eqPenalitaInOrientamentoSoft}.

\item Preferenza su quando allocare o non allocare gli Slot di un Insegnamento i passato come parametro seguendo l'esempio \ref{esPreferenzeDocenti}\footnote{Data la possibilità di specificare diverse combinazioni possibili a livello di preferenza (favorevole, contrario) e di logica temporale (primaDi, ugualeA, dopoDi) vengono riportati a titolo esemplificativo i casi di riga 9 e 8 dell'Esempio \ref{esPreferenzeDocenti}. In questo modo vengono modellate le indisponibilità dei Docenti.}:
\begin{equation}\label{eqPreferenzaInsegnamentoHard}
\begin{gathered}
\forall s \in \textit{slotInsegnamento(i)},\\
se: X\_d_{s} = Lun \Rightarrow \\
( X\_h_{s} > 8.30-10.00 \lor X\_h_{s} + \textit{numSlot(s)} \leq 8.30-10.00)
\end{gathered}
\end{equation}


\begin{equation}\label{eqPreferenzaInsegnamentoSoft}
\begin{gathered}
\forall s \in \textit{slotInsegnamento(i)},\\
se: X\_d_{s} = Lun \land \\
\neg ( X\_h_{s} > 17.30-19.00 \lor X\_h_{s} + \textit{numSlot(s)} \leq 17.30-19.00)\\
\Rightarrow X\_penalties_{prefI} = LV\_2
\end{gathered}
\end{equation}

\item Associazione degli slot orari di lezione degli Insegnamenti appartenenti ad un dato Orientamento ed un dato Anno Accademico a X\_ORIENT:
\begin{equation}\label{eqAddX_Orient}
\begin{gathered}
o \in O, a \in \left[1,3\right], i \in \textit{kernelInsInAnnoOrientamento(o,a)},\\
\forall s \in \textit{slotInsegnamento(i)}, \forall g \in G, \forall f \in F, \forall n \in \left[0,\textit{numSlot(s)},\right]\\
se: X\_d_s = g \land X\_h_s = f \\
\Rightarrow X\_orient_{o,a,g,f+n} = 1
\end{gathered}
\end{equation}

\item Per ogni Anno Accademico di ogni Orientamento, non devono esserci più di 6 slot orari giornalieri allocati per Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito:
\begin{equation}\label{eqMaxSlotGiornalieri}
\begin{gathered}
o \in O, a \in \left[1,3\right], g \in G,
\sum_{f \in F}X\_orient_{o,a,g,f} \leq 6
\end{gathered}
\end{equation}

\item Per ogni Anno Accademico di ogni Orientamento, non devono esserci più di 5 slot orari consecutivi allocati lo stesso giorno per Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito:
\begin{equation}\label{eqMaxSlotGiornalieriConsecutivi}
\begin{gathered}
o \in O, a \in \left[1,3\right], g \in G,\\
se: \sum_{f \in F}X\_orient_{o,a,g,f} = 6 \Rightarrow\\
X\_orient_{o,a,g,0} = 1 \land X\_orient_{o,a,g,6} = 1
\end{gathered}
\end{equation}

\item Per ogni Anno Accademico di ogni Orientamento, se ci sono 4 slot orari consecutivi allocati lo stesso giorno per Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito allora viene assegnata una penalità pari a LV\_1\footnote{Lo stesso vincolo è modellato su un limite di 5 slot orari consecutivi con penalita pari a LV\_2.}:
\begin{equation}\label{eq4SlotLezioneConsecutivi}
\begin{gathered}
o \in O, a \in \left[1,3\right], g \in G, f1 \in \left[0,3\right],\\
se: \sum_{0+f1 \leq f < f1+4}X\_orient_{o,a,g,f} = 4 \Rightarrow\\
X\_penaltiesStud_{pStud} = LV\_1
\end{gathered}
\end{equation}

\item Per ogni Anno Accademico di ogni Orientamento, se c'è un intervallo di 2 slot orari consecutivi lo stesso giorno per Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito allora viene assegnata una penalità pari a LV\_1\footnote{Lo stesso vincolo è modellato su un intervallo di più di 2 slot orari con penalità pari a LV\_4}:
\begin{equation}\label{eqBucoDa2Slot}
\begin{gathered}
o \in O, a \in \left[1,3\right], g \in G, f1 \in \left[1,4\right],\\
se: \sum_{0 \leq f < f1}X\_orient_{o,a,g,f} = \sum_{0 \leq f < f1+2}X\_orient_{o,a,g,f} \text{ }\land\\
\sum_{0 \leq f < f1}X\_orient_{o,a,g,f} \neq \sum_{0 \leq f < f1+3}X\_orient_{o,a,g,f}\Rightarrow\\
X\_penaltiesStud_{pStud} = LV\_1
\end{gathered}
\end{equation}

\item Per ogni Anno Accademico di ogni Orientamento, se ci sono 2 intervalli lo stesso giorno per Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta e Suggerito allora viene assegnata una penalità pari a LV\_6:
\begin{equation}\label{eq2BuchiOrario}
\begin{gathered}
o \in O, a \in \left[1,3\right], g \in G, f1 \in \left[1,3\right], f2 \in \left[f1+2,5\right],\\
se: \sum_{0 \leq f < f1}X\_orient_{o,a,g,f} = \sum_{0 \leq f < f1+1}X\_orient_{o,a,g,f} \text{ }\land\\
\sum_{0 \leq f < f1}X\_orient_{o,a,g,f} \neq \sum_{0 \leq f < f2}X\_orient_{o,a,g,f} \text{ }\land\\
\sum_{0 \leq f < f2}X\_orient_{o,a,g,f} = \sum_{0 \leq f < f2+1}X\_orient_{o,a,g,f} \text{ }\land\\
\sum_{0 \leq f < f2}X\_orient_{o,a,g,f} \neq \sum_{f \in F}X\_orient_{o,a,g,f} \text{ }\land\\
\Rightarrow X\_penaltiesStud_{pStud} = LV\_6
\end{gathered}
\end{equation}

% \todo[inline]{Non sapevo come modellare diversamente un'eq che è un prodotto di equazioni}
% \todo[inline, color=orange!30]{esistono i case delle equazioni \url{https://tex.stackexchange.com/questions/67702/using-cases-inside-equation-gives-errorwith-amsmath-loaded}}

\item In ogni slot orario della settimana gli Slot allocati per un determinato tipo di Locale e per la relativa capienza devono essere minori o uguali di quelle disponibili:
\begin{equation*}
W(s,g,f,c) = \begin{cases}
1 &\text{se 
\begin{equation*}
\begin{split}
&\textit{tipoLocale(s)} = l \land \textit{capienzaLocale(s)} = c \text{ } \land\\
&X\_d_s = g \land X\_h_s \leq f \land\\
&X\_h_s+\textit{numSlot(s)} > f 
\end{split}
\end{equation*}}\\
0 &\text{altrimenti}

\end{cases}
\end{equation*}

\begin{equation}\label{eqLocali}
\begin{gathered}
g \in G, f \in F, c \in C, l \in L,\\
\sum_{s \in S}W(s,g,f,c) \leq \textit{numLocaliDisponibili(g,f,l,c)}
% (X\_h_s \leq f)(X\_h_s+\textit{numSlot(s)} > f)\\
% \leq \textit{numLocaliDisponibili(g,f,l,c)}
\end{gathered}
\end{equation}

\item In un giorno il numero di slot orari associati ad un Docente è limitato superiormente:
\begin{equation*}
Y(g,s) = \begin{cases}
\textit{numSlot(s)} &\text{se 
X\_d_s = g}\\
0 &\text{altrimenti}
\end{cases}
\end{equation*}

\begin{equation}\label{eqMaxSlotGiornalieriDocente}
\begin{gathered}
d \in D, g \in G,\\
\sum_{s \in \textit{slotDocente(d)}}Y(g,s)\leq \textit{numSlotDocente(d)}
\end{gathered}
\end{equation}

\item Preferenza su quando allocare o non allocare gli Slot di un Docente d passato come parametro seguendo l'esempio \ref{esPreferenzeDocentiGen}: stessa struttura delle equazioni \eqref{eqPreferenzaInsegnamentoHard} e \eqref{eqPreferenzaInsegnamentoSoft}

\item Distanza minima tra due Slot associati ad uno stesso Docente d ad una distanza minima \(dist \in \mathbb{N}\)\footnote{{Questo vincolo non è attivato di default, per attivarlo va definito come nell'Esempio \ref{esVincoliVariDocente}.}}. Può essere trattato come hard constraint \eqref{eqDistMinimaHard} o come soft constraint \eqref{eqDistMinimaSoft}:
\begin{equation}\label{eqDistMinimaHard}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)}, se X\_d_{s1}=X\_d_{s2} \Rightarrow\\
X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)} + dist \text{ }\lor\\
X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)} + dist
\end{gathered}
\end{equation}
\begin{equation}\label{eqDistMinimaSoft}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)}, se X\_d_{s1}=X\_d_{s2} \land\\
\neg (X\_h_{s1} \geq X\_h_{s2} + \textit{numSlot(s2)} + dist \text{ }\lor\\
X\_h_{s2} \geq X\_h_{s1} + \textit{numSlot(s1)} + dist) \Rightarrow\\
X\_penaltiesDoc_{pDoc} = LV\_*
\end{gathered}
\end{equation}

\item Distanza massima tra due Slot associati ad uno stesso Docente d ad una distanza massima \(dist \in \mathbb{N}\)\footnote{{Questo vincolo non è attivato di default, per attivarlo va definito come nell'esempio \ref{esVincoliVariDocente}.}}. Può essere trattato come hard constraint \eqref{eqDistMassimaHard} o come soft constraint \eqref{eqDistMassimaSoft}:
\begin{equation}\label{eqDistMassimaHard}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)},\\\\
se: X\_d_{s1}=X\_d_{s2} \land X\_h_{s1} > X\_h_{s2}\\
\Rightarrow X\_h_{s1} \leq X\_h_{s2} + \textit{numSlot(s2)} + dist\\
se: X\_d_{s1}=X\_d_{s2} \land X\_h_{s2} > X\_h_{s1}\\
\Rightarrow X\_h_{s2} \leq X\_h_{s1} + \textit{numSlot(s1)} + dist
\end{gathered}
\end{equation}
\begin{equation}\label{eqDistMassimaSoft}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)},\\\\
se: X\_d_{s1}=X\_d_{s2} \land (\\
(X\_h_{s1} > X\_h_{s2} \land X\_h_{s1} > X\_h_{s2} + \textit{numSlot(s2)} + dist) \text{ } \lor\\
(X\_h_{s2} > X\_h_{s1} \land X\_h_{s2} > X\_h_{s1} + \textit{numSlot(s1)} + dist))\\
\Rightarrow X\_penaltiesDoc_{pDoc} = LV\_*\\
se: \neg(X\_d_{s1}=X\_d_{s2} \land (\\
(X\_h_{s1} > X\_h_{s2} \land X\_h_{s1} > X\_h_{s2} + \textit{numSlot(s2)} + dist) \text{ } \lor\\
(X\_h_{s2} > X\_h_{s1} \land X\_h_{s2} > X\_h_{s1} + \textit{numSlot(s1)} + dist)))\\
\Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot associati ad uno stesso Docente d e appartenenti ad Insegnamenti diversi non dovrebbero essere allocati lo stesso giorno\footnote{Questo vincolo non è attivato di default, per attivarlo va definito come nell'esempio \ref{esVincoliVariDocente}.}. Può essere trattato come hard constraint \eqref{eqSlotStessoGiornoHard} o come soft constraint \eqref{eqSlotStessoGiornoSoft}:
\begin{equation}\label{eqSlotStessoGiornoHard}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)},\\\\
X\_d_{s1} \neq X\_d_{s2}
\end{gathered}
\end{equation}
\begin{equation}\label{eqSlotStessoGiornoSoft}
\begin{gathered}
s1,s2 \in \textit{slotDocente(d)},\\\\
se: X\_d_{s1}=X\_d_{s2} \Rightarrow X\_penaltiesDoc_{pDoc} = LV\_*\\
se: X\_d_{s1} \neq X\_d_{s2} \Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot s1 almeno un giono dopo un altro Slot s2. Può essere trattato come hard constraint \eqref{eqVincoloAlmenoUnGiornoDopoHard} o come soft constraint \eqref{eqVincoloAlmenoUnGiornoDopoSoft}:
\begin{equation}\label{eqVincoloAlmenoUnGiornoDopoHard}
\begin{gathered}
X\_d_{s1}>X\_d_{s2}
\end{gathered}
\end{equation}
\begin{equation}\label{eqVincoloAlmenoUnGiornoDopoSoft}
\begin{gathered}
se: X\_d_{s1}>X\_d_{s2} \Rightarrow X\_penaltiesDoc_{pDoc} = -LV\_*\\
se: \neg(X\_d_{s1}>X\_d_{s2}) \Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot s1 in un giorno diverso da un altro Slot s2. Può essere trattato come hard constraint \eqref{eqVincoloGiornoDiversoHard} o come soft constraint \eqref{eqVincoloGiornoDiversoSoft}:
\begin{equation}\label{eqVincoloGiornoDiversoHard}
\begin{gathered}
X\_d_{s1} \neq X\_d_{s2}
\end{gathered}
\end{equation}
\begin{equation}\label{eqVincoloGiornoDiversoSoft}
\begin{gathered}
se: X\_d_{s1} \neq X\_d_{s2} \Rightarrow X\_penaltiesDoc_{pDoc} = -LV\_*\\
se: \neg(X\_d_{s1} \neq X\_d_{s2}) \Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot s1 stesso giorno di un altro Slot s2. Può essere trattato come hard constraint \eqref{eqVincoloStessoGiornoHard} o come soft constraint \eqref{eqVincoloStessoGiornoSoft}:
\begin{equation}\label{eqVincoloStessoGiornoHard}
\begin{gathered}
X\_d_{s1} = X\_d_{s2}
\end{gathered}
\end{equation}
\begin{equation}\label{eqVincoloStessoGiornoSoft}
\begin{gathered}
se: X\_d_{s1} = X\_d_{s2} \Rightarrow X\_penaltiesDoc_{pDoc} = -LV\_*\\
se: \neg(X\_d_{s1} = X\_d_{s2}) \Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot s1 parallelo ad un altro Slot s2. Può essere trattato come hard constraint \eqref{eqVincoloParalleloHard} o come soft constraint \eqref{eqVincoloParalleloSoft}:
\begin{equation}\label{eqVincoloParalleloHard}
\begin{gathered}
X\_d_{s1} = X\_d_{s2} \land X\_h_{s1} = \land X\_f_{s2}
\end{gathered}
\end{equation}
\begin{equation}\label{eqVincoloParalleloSoft}
\begin{gathered}
se: X\_d_{s1} = X\_d_{s2} \land X\_h_{s1} = \land X\_f_{s2} \\
\Rightarrow X\_penaltiesDoc_{pDoc} = -LV\_*\\
se: \neg(X\_d_{s1} = X\_d_{s2} \land X\_h_{s1} = \land X\_f_{s2})\\
\Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}

\item Slot s1 subito dopo un altro Slot s2. Può essere trattato come hard constraint \eqref{eqVincoloSubitoDopoHard} o come soft constraint \eqref{eqVincoloSubitoDopoSoft}:
\begin{equation}\label{eqVincoloSubitoDopoHard}
\begin{gathered}
X\_d_{s1}=X\_d_{s2} \land X\_h_{s1} = X\_h_{s2} + \textit{numSlot(s2)}
\end{gathered}
\end{equation}
\begin{equation}\label{eqVincoloSubitoDopoSoft}
\begin{gathered}
se: X\_d_{s1}=X\_d_{s2} \land X\_h_{s1} = X\_h_{s2} + \textit{numSlot(s2)}\\
\Rightarrow X\_penaltiesDoc_{pDoc} = -LV\_*\\
se: \neg(X\_d_{s1}=X\_d_{s2} \land X\_h_{s1} = X\_h_{s2} + \textit{numSlot(s2)})\\
\Rightarrow X\_penaltiesDoc_{pDoc} = 0
\end{gathered}
\end{equation}


\end{itemize}
\subsection{Modellazione con equazioni}
La rappresentazione in Python di tutte le equazioni presenti nel modello sono riportate  in Appendice~\ref{bookEqModelloASlot}.

\subsection{Conclusioni}
Questo modello consente di modellare tutti i requisiti di alto livello ad eccezione della gestione della distanza tra Locali.
Inoltre le performance ottenute con il software CPLEX garantiscono un elevato grado di scalabilità con un aumento accettabile delle risorse necessarie.


