\chapter{Testing e validazione}\label{chapTesting}

\section{Validazione preliminare con dati anno precedente}
Per poter validare il funzionamento del tool è stato necessario utilizzare un primo dataset di testing in attesa di recepire i dati ufficiali ottenuti solo successivamente. Per tale scopo sono stati usati i dati del primo semestre dell'Anno Accademico 2021-2022 poiché molto simili a quelli su cui operare successivamente\footnote{Mediamente variano 10/20 corsi tra un Anno Accademico e l'altro, con piccole variazioni all'interno della pianificazione dei vari Orientamenti.}.

\subsection{Dati provenienti dall'Ufficio Gestione Aule Anno Accademico 2021-2022}\label{bookGOFAnnoScorso}
Sorgente principale di dati per questa prima validazione è il documento pervenuto dall'Ufficio Gestione Aule, Area Edilizia e Logistica (EDILOG) del Politecnico di Torino, contenente per ogni Orientamente dei vari Cdl in capo ai collegi ICM e ETF gli Insegnamenti che ne fanno parte di cui è presente un estratto in Figura~\ref{fig:gof}.
\begin{figure}
    \centering
    \includegraphics[width=\textwidth]{images/figures/GOF.png}
    \caption{Estratto documento dell'Ufficio Gestione Aule.}
    \label{fig:gof}
\end{figure}
Da questo file sono stati estratti per ogni Orientamento tutti gli Insegnamenti con il rispettivo TipoInsegnamento ed inseriti a db secondo il formato definito nella sezione \ref{bookInsegnamentiInOrientamento} tramite script Python.\\
Il file è stato anche la sorgente per la definizione dei file XML degli Insegnamenti secondo lo schema Template Orario introdotto nella Sezione~\ref{bookTemplateOrario} dato che si trattava di dati inediti e non previsti fino allo scorso anno; anch'essi sono stati generati tramite script Python.

\subsection{Dati estratti dal sito del Politecnico}\label{bookSitoPoli}
Da una prima analisi dei dati estratti come descritto nella Sezione \ref{bookGOFAnnoScorso} è chiaro come risulti ambiguo ricavare il TipoInsegnamento di un dato Insegnamento all'interno di un Orientamento. 

Le informazioni mancanti sono estratte direttamente dai piani studi dei vari Orientamenti presenti sul sito del Politecnico.

L'importazione dei dati da tale fonte è avvenuta mediante la scrittura di un web scraper scritto in Python avvalendosi delle librerie Requests\footnote{https://pypi.org/project/requests/} e BeatifulSoup\footnote{https://beautiful-soup-4.readthedocs.io/en/latest/}. Di seguito vengono mostrati i risultati ottenuti in seguito ad alcune operazioni manuali volte ad uniformare i dati ricavati :
\begin{lstlisting}
['cdl', 'Corso  di Laurea in Ingegneria  fisica (Torino)', 'https://didattica.polito.it/pls/portal30/sviluppo.offerta_formativa_2019.vis?p_coorte=2022&p_sdu=37&p_cds=9']
,['orientamento', 'Percorso']
,['table_title', '1 anno 2021/2022']
,['table_content', [['periodo', 'codIns', 'cfu'], ['1', '16ACFOD', 'Analisi matematica I'], ['1', '15AHMOD', 'Chimica'], ['1', '14BHDOD', 'Informatica'], ['1; 2', '07LKIOD', 'Lingua inglese I livello'], ['2', '01RKCOD', 'Algebra lineare e geometria'], ['2', '17AXOOD', 'Fisica I'], ['2', '04BKTOD', 'Laboratorio di fisica']]]
,['table_title', '2 anno 2022/2023']
,['table_content', [['periodo', 'codIns', 'cfu'], ['1,2', '', ''], ['oppure'], ['1,2', '', ''], ['2', '01USBOD', '']]]
,['table_title', '3 anno 2023/2024']
,['table_content', [['periodo', 'codIns', 'cfu'], ['1', '02NKUOD', 'Elettromagnetismo applicato'], ['1', '06AXFOD', 'Fisica dello stato solido'], ['1', '02MZGOD', 'Applied electronics'], ['oppure'], ['1', '07ATIOD', 'Elettronica applicata'], ['1,2', 'Insegnamento a scelta da Tabella B', '6'], ['1,2', '32IBNOD', ''], ['2', 'Insegnamento a scelta da Tabella 1', '8'], ['1,2', 'Crediti liberi del 3 anno', '6'], ['2', '01NTQOD', 'Tecnologie per le nanoscienze']]]
\end{lstlisting}

Un'ulteriore informazione importata dal sito del Politecnico è il numero di studenti iscritti ad un determinato Insegnamento, avvenuto anch'esso tramite un altro web scraper scritto in Python mediante l'ausilio della libreria Requests in grado di ricavare i dati desiderati sulla base dei superi degli esami.
% \begin{figure}
%     \centering
%     \includegraphics[width=\textwidth]{images/superiInsegnamento.png}
%     \caption{Superi Insegnamento.}
%     \label{fig:superiInsegnamento}
% \end{figure}

\subsection{Problemi di performance}
Sulla base del dataset realizzato vengono fatti dei test al fine di valutare le performance del tool inizialmente in ambiente locale\footnote{L'ambiente locale prevede un PC portatile con processore Intel Core i7 (4 core) e 12 GB di RAM.} osservando come in modalità validazione restave in esecuzione per diversi giorni senza restituire soluzioni mentre in modalità ottimizzazione restituiva un eccezione in seguito ad una completa saturazione della memoria disponibile.\\

In seguito a richiesta all'Area IT del Politecnico di Torino viene messo a disposizione un nodo di calcolo interno al Politecnico disponente di 64 core e 192 GB di RAM. Con questa nuova configurazione il tempo di esecuzione del software in modalità validazione è di qualche giorno mentre è indefinito in ottimizzazione \footnote{Il tool è stato lasciato in esecuzione per circa tre settimane senza che iniziasse la fase di convergenza verso la soluzione ottima}. Da prove sperimentali successive emerge che tali tempistiche siano dovute a dei limiti particolarmente stretti circa le aule disponibili.

\subsection{Visualizzazione grafica dei risultati}
La validazione preliminare dei risultati è uno scoglio non indifferente a causa della mole di essi e dei vincoli a cui i vari Slot devono sottostare. Viene quindi implementata una web app minimale mediante la libreria React\footnote{https://it.reactjs.org/} che permette di filtrare gli Slot di una soluzione generata per CDL, Orientamento e Periodo didattico come mostrato in Figura~\ref{fig:figConfWebApp}.\\
\begin{figure}
    \centering
    \includegraphics[width=\textwidth]{images/figures/confWebApp.png}
    \caption{Finestra di configurazione dell'applicazione per la visualizzazione grafica dei risultati.}
    \label{fig:figConfWebApp}
\end{figure}
Questa applicazione permette una visualizzazione tabellare dell'orario settimanale di un dato Orientamento, mostrando in ogni slot orario i vari Slot allocati; inoltre prevede colorazioni differenti a seconda che si tratti di un Insegnamento obbligatorio, obbligatorio a scelta o suggerito (rosso), un Insegnamento a scelta (giallo) o un credito libero (verde) come mostrato in Figura~\ref{fig:orarioWebApp} permettendo di individuare immediatamente eventuali sovrapposizioni.
\begin{figure}
    \centering
    \includegraphics[width=\textwidth]{images/figures/orarioWebApp.png}
    \caption{Estratto orario applicazioneper la visualizzazione grafica dei risultati.}
    \label{fig:orarioWebApp}
\end{figure}

\section{Acquisizione dati Anno Accademico 2022-2023}
L'acquisizione dei nuovi dati ha comportato l'affrontare alcune nuove problematiche che verranno discusse qui di seguito.

\subsection{Dati provenienti dall'Ufficio Gestione Aule}

Come per i dati di prova vengono usati i dati dell'Ufficio Gestione Aule per ricavare gli Insegnamenti associati ai vari Orientamenti, tuttavia non vengono più generati i file XML degli Insegnamenti a partire da questa fonte. Questi dati vengono arricchiti con i dati presenti sul sito del Politecnico come descritto nella Sezione~\ref{bookSitoPoli}.

L'ufficio Gestione Aule stabilisce, compatibilmente con gli Insegnamenti erogati dagli altri collegi, il numero, il tipo e la capienza delle aule e dei laboratori resi disponibili per l'allocazione dei due collegi in esame. Questo documento è stato trasformato manualmente in XML seguendo lo schema introdotto in fase di progettazione nella Sezione~\ref{bookLocaliXmlSchema}

\subsection{Dati supplementari inseriti manualmente}
Dai risultati ottenuti dai primi tentativi in modalità validazione sono emersi alcuni problemi di dati mancanti con le sorgenti fin qui considerate, in particolare riguardo gli Orientamenti in cui compaiono gli Insegnamenti, nonchè gli Insegnamenti veri e propri di cui bisogna allocare l'Orario. La soluzione adottata prevede il completamento del database con i dati mancanti inseriti manualmente come mostrato qui di seguito\footnote{Purtroppo qualche sporadico errore è rimasto anche successivamente data la mole di dati. Il codice mostrato è solamente un estratto dei dati aggiunti.}:
\begin{lstlisting}
# Inserimenti Orientamenti puntuali

ins:List[Tuple[str,TipoInsegnamento]] = list()
ins.append(("261457", TipoInsegnamento.Obbligatorio))
ins.append(("261456", TipoInsegnamento.Obbligatorio))
ins.append(("258956", TipoInsegnamento.Obbligatorio))
ins.append(("258955", TipoInsegnamento.Obbligatorio))
ins.append(("258954", TipoInsegnamento.Obbligatorio))
db.update_InsegnamentiInOrientamento("Percorso", "COMMUNICATIONS ENGINEERING", ins, 'Z', '1-1')

ins:List[Tuple[str,TipoInsegnamento]] = list()
ins.append(("260275", TipoInsegnamento.Obbligatorio))
db.add_InsegnamentiInOrientamento("MNIS - Micro and Nanotechnologies for Integrated Systems", "NANOTECHNOLOGIES FOR ICTs (NANOTECNOLOGIE PER LE ICT)", 'Z', '1-1', ins)
\end{lstlisting}
\label{bookInsParallelizzabili}
Un altro affinamento dei dati è stato fatto per consentire un'allocazione anche parallela delle istanze in lingua italiana ed inglese di uno stesso Insegnamento, seppure venissero considerare entrambi di tipo Obbligatorio, Obbligatorio a scelta o Suggerito per un dato Orientamento. Viene quindi definita la seguente struttura ausiliaria come sorgente di dati per il tool di cui è riportato un estratto di codice:
\begin{lstlisting}
list_ID_INC_parallelizzabili = []
'''Ogni entry contiene gli ID_INC di corsi parallelizzabili tra loro anche se appartenenti allo stesso Orientamento
e Obbligatori (eg: alfabetiche diverse, Insegnamenti in italiano e in inglese).
Format: [[ID_INC_1, ID_INC_2], [.., ..], ..]'''
list_ID_INC_parallelizzabili.extend([['259206','260158', '259922'], ['259233','260158','259234'], ['259233','260302']])
\end{lstlisting}
Infine per completare la descrizione di Insegnamenti non sovrapponibili tra loro poichè non completa con i dati a disposizione, si è definita una nuova struttura in grado di modellare un conflitto binario tra Insegnamenti sia come soft che come hard constraint:
\begin{lstlisting}
# permette di specificare coppie di Insegnamenti non sovrapponibili tra loro (a prescindere da tutti gli altri vincoli)
list_InsegnamentiNonSovrapponibiliCustom:List[Tuple[Tuple[int,int], LV_Penalties]] = list() # ((ID_INC1, ID_INC2), LV_PEN)

# Hard Constraints
list_InsegnamentiNonSovrapponibiliCustom.append(((261125,259419),LV_Penalties.LV_H))
list_InsegnamentiNonSovrapponibiliCustom.append(((259328,259419),LV_Penalties.LV_H))
# Soft Constraints
list_InsegnamentiNonSovrapponibiliCustom.append(((261103,259419),LV_Penalties.LV_5))
list_InsegnamentiNonSovrapponibiliCustom.append(((263355,259419),LV_Penalties.LV_5))
\end{lstlisting}

\subsection{Jotform e desiderata Docenti}
% \todo[inline]{Lo faccio dall'altro pc che ho i link così metto 2 img}
Per poter collezionare tutte le informazioni relative ai Docenti che descriverssero un'allocazione desiderata dell'orario e le loro preferenze in termini di indisponibilità è stato necessario introdurre un'ulteriore sorgente di dati che doveva risultare accessibile ai vari Docenti in modo immediato e consentire al tempo stesso un'estrazione in un tempo limitato dei file XML compatibili col formato descritto nella Sezione \ref{bookTemplateOrario} e delle disponibilità dei Docenti secondo il formato descritto nell'Esempio \ref{esPreferenzeDocenti}.

Per poter soddisfare tale compito si è fatto ricorso al tool disponibile online Jotform\footnote{https://www.jotform.com/}.


\subsection{Insegnamenti appartenenti ai collegi ICM e ETF non presenti in Jotform}
Per alcuni Orientamenti e alcuni Insegnamenti viene mantenuto l'orario dello scorso anno. Per far fronte a questa richiesta, vista l'impossibilità di utilizzare la modalità ottimizzazione incrementale poichè nel database non è presente l'allocazione dell'orario dello scorso anno, vengono generati manualmente i diversi file XML secondo lo schema Template Orario indicato nella Sezione~\ref{bookTemplateOrario}.

\subsection{Orari da altri collegi}
Molti Docenti hanno lezioni appartenenti non solamente a Insegnamenti facenti capo ai collegi ICM e ETF di cui il tool deve elaborare l'orario, ma hanno lezioni anche in altri Insegnamenti di cui non se ne occupa il tool e che quindi devono essere descritti come slot orari preallocati per i Docenti.

Considerare tali Slot come indisponibilità dei Docenti non è corretto perchè sarebbe possibile allocare molti slot orari nella stessa giornata andando anche oltre il limite di slot orari giornalieri del Docente. Nemmeno considerarli SlotScelti del tipo definito fin qui non sarebbbe corretto poichè il tool allocherebbe anche i Locali necessari allo svolgimento di tali Slot.


La soluzione adottata prevede di creare Insegnamenti speciali caratterizzati da un ID\_INC < 0 così da permettere al tool di gestirli correttamente:
\begin{lstlisting}[language=XML,morekeywords={encoding,xs:schema,xs:element,xs:complexType,xs:sequence,xs:attribute,xs:simpleType,xs:restriction,xs:enumeration,TemplateOrario,ID_INC,NumIscritti,SlotScelto,SlotGenerico,Docente,NumSlotConsecutivi,Tipo,Locale,Giorno,FasciaOraria,PreseElettriche,id,Vincolo,Penalita,slotId1,slotId2,TipoVincolo,CatalogoTemplate}]
<CatalogoTemplate xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="../../models/schemaUseCase.xsd">
<TemplateOrario><!-- generated by Francesco -->
<id>Insegnamenti Gestionali</id>
<ID_INC>-2</ID_INC>
<NumIscritti>0</NumIscritti>

<!-- imprenditorialità e innovazione -->
<SlotScelto slotId="slot3"><Docente>Landoni Paolo</Docente><NumSlotConsecutivi>1</NumSlotConsecutivi><Tipo>L</Tipo><Locale>Aula multimediale</Locale><Giorno>Lun</Giorno><FasciaOraria>14.30-16.00</FasciaOraria></SlotScelto>
<SlotScelto slotId="slot4"><Docente>Landoni Paolo</Docente><NumSlotConsecutivi>2</NumSlotConsecutivi><Tipo>L</Tipo><Locale>Aula multimediale</Locale><Giorno>Gio</Giorno><FasciaOraria>16.00-17.30</FasciaOraria></SlotScelto>

<!-- Basi di dati -->
<SlotScelto slotId="slot7"><Docente>Cagliero Luca</Docente><NumSlotConsecutivi>2</NumSlotConsecutivi><Tipo>L</Tipo><Locale>Aula</Locale><Giorno>Lun</Giorno><FasciaOraria>10.00-11.30</FasciaOraria></SlotScelto>
<SlotScelto slotId="slot8"><Docente>Cagliero Luca</Docente><NumSlotConsecutivi>2</NumSlotConsecutivi><Tipo>L</Tipo><Locale>Aula</Locale><Giorno>Gio</Giorno><FasciaOraria>13.00-14.30</FasciaOraria></SlotScelto>

</TemplateOrario>
</CatalogoTemplate>
\end{lstlisting}

% \subsection{Limiti disponibilità Locali}
% \todo[inline]{Chi ci ha fornito i dati?}
% A livello di Ateneo viene stabilito, compatibilmente con gli Insegnamenti erogati dagli altri collegi, il numero, il tipo e la capienza delle aule e dei laboratori resi disponibili per l'allocazione dei due collegi in esame. Tale file di cui è mostrato un estratto in figura ... è stato trasformato manualmente in xml seguendo lo schema introdotto in fase di progettazione nella sezione Aule disponibili~\ref{bookLocaliXmlSchema}

\section{Validazione dati Anno Accademico 2022-2023}
\subsection{Primi tentativi UNSAT}
Le prime simulazioni lanciate in modalità validazione terminavano immediatamente poichè l'introduzione di molti Insegnamenti preallocati pregiudicava il soddisfacimento di tutti i vincoli definiti dai requisiti. In particolare è stato modificato parzialmente il tool per ignorare violazioni dei requisiti dovute ad un'approssimazione del modello reale nei seguenti casi:
\begin{itemize}

\item Slot di Insegnamenti di tipo Obbligatorio, Obbligatorio a scelta, Suggerito per un dato Insegamento paralleli tra loro in quanto la sovrapposizione risulta tollerata: viene sfruttata la struttura introdotta nella Sezione~\ref{bookInsParallelizzabili}.
\\Questo approccio non risulta corretto nel caso in cui i due Insegnamenti siano composti anche da SlotGenerici, in quanto l'allentamento dei vincoli così definito ha valore a livello di Insegnamento e non di singolo Slot; viene quindi introdotta la possibilità di allentare il vincolo di non sovrapposizione con granularità maggiore agendo sul singolo Slot con l'implementazione di una nuova funzione:
\begin{lstlisting}
def customCheckSlotParallelizzabili(self, slotId_i:str, slotId_j:str) -> bool:
    '''Controlla se due slot possono essere alloati in parallelo anche se secondo i normali requisiti non potrebbero'''
    
    # 259237 - Modeling and optimization of embedded systems Mar 14:30-17:30 pd: PeriodoDidattico.PrimoAnno_PrimoSemestre - 259236 - Electronics for embedded systems Mar 14:30-17:30 pd: PeriodoDidattico.PrimoAnno_PrimoSemestre
    if slotId_i in ["259237_slot_lab1", "259236_slot_lab2"] and slotId_j in ["259237_slot_lab1", "259236_slot_lab2"]:
        return True
\end{lstlisting}

\item In certi casi venivano allocati quotidianamente più di 4 slot orari allo stesso Docente, si è quindi aumentato tale limite giornaliero per il Docente specifico come indicato nell'Esempio \ref{esLimitiGiornalieriDocenti}.

\item Vi sono verificati casi di SlotScelti allocati in parallelo tenuti dallo stesso Docente: tale situazione è frutto di lezioni a settimane alterne all'interno di certi Insegnamenti che non creano veri conflitti. Si procede aggiungendo il suffisso \say{1} in uno dei due SlotScelti evitando di far considerare al tool allocati allo stesso Docente entrambi gli Slot.

\item Esistono alcuni casi particolari di Insegnamenti in cui il semestre è suddiviso in più parti e tali parti sono erogate in periodi diversi del semestre a seconda dell'alfabetica poichè la singola porzione di lezioni è tenuta da un singolo Docente e questo non farà tutte le lezioni nello stesso periodo. La descrizione tramite XML per questi Insegnamenti non risulta sufficiente poichè imporrebbe che tutti questi Insegnamenti non siano allocati in parallelo in quanto tenuti da almeno un Docente in comune; l'approcio descritto al punto precedente anche non sarebbe corretto in quanto in caso gli Slot non fossero poi comunque allocati in parallelo ci troveremmo ad avere degli slot orari in cui tale Docente risulta essere realmente indisponibile mentre così non sarebbe per il software.\\
L'approccio ideato prevede di inserire una nuova opzione come descritto nell'Esempio \ref{esInsSovrapponibili}.

\end{itemize}

\subsection{Allentamento vincoli con soft constraint}
Tutti i raffinamenti dei dati messi in atto fino ad ora non sono stati sufficienti a garantire un'allocazione valida dell'orario a causa del numero elevato di vincoli sugli Insegnamenti appartenenti ai diversi Orientamenti definiti come Hard Constraint ed hai limiti fisici di disponibilità delle Aule.
In seguito ad un allentamento di molti vincoli definiti precedentemente come Hard Constraint trasformandoli in Soft Constraint\footnote{A tali vincoli è stata associata una penalità pari a LV\_5.} la modalità validazione termina con esito positivo; lanciando il tool in modalità ottimizzazione è possibile ottenere allocazioni che garantiscano una sovrapposizione degli Insegnamenti relaviti ai vincoli allentati via via sempre minore con il decrescere della funzione obiettivo.

\subsection{Risultati}
I risultati in modalità validazione una volta raggiunto questo livello di affinamento dei dati sono stati ricavati in un tempo variabile dai 30 minuti all'ora e mezza e quindi sufficientemente basso da poter valutare differenti configurazioni dei dati in input.

Dati i tempi ristretti e la mancanza di soluzioni precedenti salvate nel database l'ottimizzazione viene lanciata solamente in modalità ottimizzazione globale e dopo una decina di ore di studio del problema inizia un lungo processo di convergenza alla soluzione matematicamente ottima partendo da una prima soluzione con costo della funzione obiettivo di circa 80.000. Dopo qualche giorno di calcolo arriva ad una soluzione con costo di circa 20.000 che viene utilizzata come base dell'orario del prossimo anno\footnote{Non è stato possibile utilizzare una soluzione con costo inferiore poichè si sono saturati i 192 GB di RAM del nodo di calcolo.}, al netto di qualche modifica manuale.

\subsection{Esportazione}\label{bookEsport}
Quest'ultima fase prevede l'estrazione della soluzione salvata in fase di solving nel database in un formato facilmente interpretabile dall'utente. Sono previsti 3 differenti files che rappresentano l'orario della soluzione:
\begin{itemize}

\item Slot orario: file csv contente una rappresentazione sintetica di tutti gli Slot allocati dell'orario con tutte le informazioni rilevanti di supporto come mostrato in Figura~\ref{fig:cvsSlotAllocati}, l'elenco completo dei campi presenti corrisponde a: \say{PianoAllocazione}, \say{idSlot}, \say{nStudentiAssegnati}, \say{tipoLez}, \say{numSlotConsecutivi}, \say{ID_INC}, \say{Insegnamento}, \say{Titolare}, \say{Giorno}, \say{Ora}, \say{tipoLocale}, \say{tipoErogazione}, \say{capienzaAula}, \say{squadra}, \say{preseElettriche}, \say{Note}, \say{Docenti}, \say{Orientamenti}.
\begin{figure}
    \centering
    \includegraphics[width=\textwidth]{images/figures/solCsv.png}
    \caption{File csv Slot allocati.}
    \label{fig:cvsSlotAllocati}
\end{figure}

\item Matrice allocazione Insegnamenti: file excel rappresentante una tabella in cui viene indicato per ogni Insegnamento gli slot orari allocati ed il tipo di Locale associato ad essi come in Figura~\ref{fig:matriceSol}.
\begin{figure}
    \centering
    \includegraphics[width=\textwidth]{images/figures/matriceSol.png}
    \caption{Matrice allocazione Insegnamenti negli slot orari.}
    \label{fig:matriceSol}
\end{figure}

\item Statistiche circa l'occupazione dei Locali nei vari slot orari della giornata come nell'Esempio \ref{esStatisticheSol}.
\begin{example}\label{esStatisticheSol}
\small
\\Lun:\\
8.30-10.00:\\
nSlot totali allocati: 20\\
nSlot in Aula con capienza Piccola: 7\\
nSlot in Aula con capienza Media: 3\\
nSlot in Aula con capienza MedioGrande: 3\\
nSlot in Aula con capienza Grande: 3\\
nSlot in Aula con capienza Piccola e necessità prese elettriche: 1\\
nSlot in Aula con capienza Media e necessità prese elettriche: 0\\
nSlot in Aula con capienza MedioGrande e necessità prese elettriche: 0\\
nSlot in Aula con capienza Grande e necessità prese elettriche: 0\\
nSlot in locale di tipo Aula: 0\\
nSlot in locale di tipo Laboratorio: 0\\
nSlot in locale di tipo LABINF: 1\\
nSlot in locale di tipo LAIB: 0\\
nSlot in locale di tipo LADISPE: 1\\
nSlot in locale di tipo LED: 2\\
nSlot in locale di tipo LED1: 0\\
nSlot in locale di tipo LED2: 0\\
nSlot in locale di tipo ACSLAB: 0\\
nSlot in locale di tipo Aula 5T: 0\\
nSlot in locale di tipo Aula attrezzata CA2: 4\\
nSlot in locale di tipo Aula attrezzata CA: 11\\
nSlot in locale di tipo Aula TableBox: 0\\
nSlot in locale di tipo Aula WallBox: 1
\end{example}



\end{itemize}

% validazione preliminare su orario anno precedente
% con dati usati l'anno scorso

% problemi di performance in opt

% aggiunta 128 core + 128GB


% sono stati acquisiti i seguenti dati per l'allocazione dell'orario dei collegi ICM ed ETF per il primo semestre dell'AA 2022-23
% \begin{itemize}
%     \item dati GOF
%     \item dati sul sito
%     \item JOTFORM
%     \item desiderata docenti
%     \item orari pervenuti da altri collegi per evitare sovrapposizioni
%     \item 
% \end{itemize}

% procedura in validazione

% che era UNSAT, sono stati allentati dei vincoli

% poi procedura in opt soft

% non pproduceva niente per giorni

% allentati vincoli soft

% risultato in qualche giorno

