\chapter{Background}\label{chapBackground}

% \todo[inline]{Scrivere meglio}
Dopo una ricerca nella letteratura informatica di problemi noti simili a quello oggetto di Tesi si sono individuati due approcci differenti per affrontarlo: modellandolo come \textit{Maximum Satisfiability problem} con l'ausilio del software Z3 e modellandolo come  \textit{Integer Linear Programming problem} con l'ausilio del software CPLEX\footnote{Il problema è NP-Completo}. Entrambi gli approcci sono presentati in questo Capitolo.

\section{Problema Job-Shop Scheduling}
Nella letteratura informatica il problema del Job-Shop Scheduling consiste nell'allocare risorse condivise e presenti in maniera limitata a diverse attività nel tempo\cite{jobShopScheduling,z3Rosselli}. Il modello descrive un insieme di n jobs \(\{J_i\}_{0\leq i<n}\) costituiti ognuno da diverse Operazioni O da eseguire in ordine sequenzialie su m macchine \(\{M_r\}_{0<\leq r < m}\). 


Esistono vincoli di precedenza tra i diversi Job tali per cui:
\begin{equation*}
    time(J_i) < time(J_j)
\end{equation*}
L'esecuzione di un'Operazione di un Job su una macchina ne prevede un uso esclusivo, mentre il tempo necessario al suo completamento viene chiamato l. 

La funzione obiettivo del Job-Shop scheduling è di minimizzare il \textit{makespan} L corrispondente al tempo necessario a completare tutti i jobs.

Viene definita schedulazione un'allocazione che permette di eseguire in un tempo L tutti i jobs. Il problema è NP-Completo.

\section{SAT e maxSAT}
\subsection{Logica proposizionale}
Nella logica proposizionale le proposizioni sono costruite partendo da variabili booleane e composte usando solamente connettivi logici quali \(\land, \lor, \lnot\).\\I SAT solver utilizzano un approccio chiamato \textit{systematic search} in cui lo spazio di ricerca è un albero in cui ogni nodo rappresenta una singola variabile booleana e gli archi uscenti dal vertice la scelta \textit{true} o \textit{false} per quella variabile. Data una formula con \(n\) variabili, ci sono \(2^n\) foglie nell'albero. Viene definito \textit{model (modello)} un percorso dalla radice a una foglia tale per cui la formula risulti vera \cite{wikipediaCNF,z3Tutorial}.

La costruzione del modello avviene mediante l'algoritmo \textit{DPLL}\footnote{Davis-Putnam-Logemann-Loveland: algoritmo di ricerca esaustiva, basato su backtracking, utilizzato per decidere la soddifabilità booleaa di formule di logica proposizionale CNF.}\index{DPLL} usando tre operazioni: \textit{decide}, \textit{propagate} e \textit{backtrack}. L'algoritmo sfrutta la possibilità di scrivere ogni proposizione logica in una equivalente forma detta \textit{Forma Normale Congiuntiva CNF}\footnote{Una formula CNF è una formula booleana tale per cui ogni clausola è una disgiunzione di letterali; un letterale è una variabile atomica o la negazione di una variabile atomica.}.
\begin{example}
\footnotesize{Una proposizione CNF valida è:
\begin{align}
    (A\lor \lnot B\lor \lnot C)\land(\lnot D \lor E \lor F) 
\end{align}
supponendo che tutte le variabili siano atomiche booleane.
Per chiarezza si noti che ogni clausola corrisponde alla singola espressione tra parentesi.
Una proposizione non CNF è:
\begin{align}
    \lnot(B \lor C)
\end{align}
 che può essere riscritta nella corrispondente forma CNF: 
 \begin{align}
      (\lnot B) \land (\lnot C)
 \end{align}

}\end{example}
L'operazione \textit{decide} sceglie euristicamente una variabile atomica a cui non è ancora stato assegnato un valore e vi assegna true o false\footnote{Questa operazione è detta anche \textit{branching} o \textit{case splitting}.}. L'operazione \textit{propagate} ricava le conseguenze della soluzione parziale usando alcune regole di deduzione, tra cui la principale si chiama \textit{unit-clause rule}\index{Unit-clause rule} che asserisce \say{se tutti i letterali di una clausola tranne uno sono assegnati a false il letterale rimanente \(l\) è ancora indefinito, allora l'unica possibilità per la clausola per essere valuta true è quella di assegnare true a \(l\)}.

Data la clausola  \(C:= p \lor \lnot q \lor \lnot r\) e la soluzione parziale \(M:= \{p \rightarrow false, r \rightarrow true\}\), allora l'unico modo per \(C\) per essere true è assegnare a \(q\) false. Con una parziale valorizzazione \(M\) e una clausola \(C\) all'interno della CNF tale per cui tutti i letterali di di \(C\) sono assegnati a false, allora non è possibile estendere \(M\) ad un modello completo \(M'\) che soddisfa la formula data ma si è in \textit{conflitto} e \(C\) è in una \textit{clausola conflittuale}.

Un conflitto indica che alcune delle decisioni precedentemente prese non portano ad un assegnamento valido per la formula data e quindi l'algoritmo DPLL procede con un \textit{backtrack} e prova ad usare un branch differente. Se è rilevato un conflitto e non è possibile effettuare \textit{backtrack} su nessuna decisione si deduce che la formula è \textit{unsatisfiable (non soddisfacibile)}\index{Unsatisfiable}.


\subsection{Satisfiability Modulo Theories}
La logica booleana introdotta non risulta sufficiente per modellare il problema del Job Shop Scheduling; per ovviare a questo si introduce un nuovo tipo di problema chiamato \textit{Satisfiability Modulo Theories} (SMT); questo consiste nel verificare se una formula logica F è soddisfacibile secondo una derminata teoria con dei vincoli su F. Si dice che una formula F è soddisfacibile se esiste un'interpretazione tale per cui F è vera \cite{z3Tutorial}.
\begin{example}
\footnotesize La formula 
\begin{equation}
a+b>3 \land a<0 \land b>0
\end{equation}
è soddisfacibile secondo la teoria aritmetica poichè esiste l'interpretazione
\begin{equation}
    a \mapsto -1, b \mapsto 5
\end{equation}
\end{example}
Il problema del Job-Shop Scheduling come detto necessita di disequazioni lineari per essere modellato, ed in particolare combinando un SAT solver con un solver SMT che supporti la teoria dell'aritmentica delle differenze\footnote{Supportata da Z3.}. L'aritmetica delle differenze è una branchia dell'aritmetica lineare dove i predicati sono ristretti alla forma \( t - s \leq c\) dove t e s sono variabili mentre c è una costante numerica.
Un problema SMT estende un problema di logica booleana includendo oltre alle proposizioni logiche anche predicati riferiti ad un insieme di variabili non binarie, come ad esempio disequazioni. Questo fatto permetterà anche di trasformare un problema di soddisfacibilità in un problema di ottimizzazione assegnando dei costi alle variabili.

\subsection{Il solver Z3}
Z3 è un solver SMT che sfrutta in sinergia l'analisi, la verifica e l'esecuzione simbolica del codice. Nella realizzazione del software oggetto di questa Tesi si è fatto uso delle API sviluppate per Python.

Tra i vari tipi di proposizioni supportate da Z3 ve ne sono due di particolare rilevanza che sono state utilizzate nella realizzazione del modello: \textit{Propositional Logic} e \textit{Integer Linear Arithmetic}.

\begin{example}
\footnotesize{Di seguito un esempio di \textit{Propositional solving} in Z3 in cui il modello è rappresentato da 3 variabili atomiche booleane.}
\begin{lstlisting}
from z3 import *
Auto, Patente, Bicicletta = Bools("auto patente bicicletta")
s = Solver()
s.add(Or(
    And(Patente, Auto), Bicicletta
    ))
s.add(Not(
    And(And(Patente,Auto), Bicicletta
    )))
print(s.check())
print(s.model())

# output:
sat # s.check()
[bicicletta = False, auto = True, patente = True] # s.model()
\end{lstlisting}
\end{example}
Dopo l'allocazione delle variabili si procede con l'instanziazione del solver (riga 3) e con l'aggiunta di due proposizioni logiche (riga 4 e 7) che porta il solver a generare le seguenti asserzioni come constraint per il modello:
\[(Patente \land Auto) \lor Bicicletta\]
\[\lnot((Patente \land Auto) \land Bicicletta)\]
Alla riga 10 viene quindi verificata la \textit{soddisfacibilità}\footnote{Un problema si definisce sat se ne esiste almeno una soluzione che soddisfa tutte le proposizioni.}\index{Soddisfacibilità} del modello ed in caso di esito positivo viene estratta una soluzione (riga 11).\\
Z3 prevede anche l'utilizzo di proposizioni aritmetiche lineari sia nell'insieme dei numeri Interi che in quello dei Reali; nella realizzazione del modello si è fatto uso solamente di proposizioni aritmetiche con numeri Interi.

\subsection{Problema MaxSAT con Z3}
La definizione di problema MaxSAT è di minimizzare il numero di soft constraint violati. Assumendo che tutti i vincoli non siano pesati, ovvero di peso unitario, si definisce un problema MaxSAT con associati i predicati constraint \( P_1,...,P_n,F_1,...,F_n \) dove i predicati \(P_*\) sono hard constraint mentre quelli \(F_*\) sono soft. L'obiettivo sarà quindi quello di trovare un'interpretazione tale per cui sia soddisfatti tutti i \(P_*\) ed al contempo sia soddisfatto il numero maggiore possibile di \(F_*\)\cite{ProgrammingZ3}.
\begin{example}
\footnotesize
Dato il problema MaxSAT con \(P,F_1,..,F_5\) dove i primi 4 soft constraint non possono essere soddisfatti insieme all'hard constraint P. Scritto formalmente:
\begin{equation}
    \mathrm{A}: \mathrm{P,F_1,F_2,F_3,F_4,F_5}
\end{equation}
Si definisce quindi il prblema "allentato" \(A'\):
\begin{equation}
    \mathrm{A'}:\mathrm{P},\mathrm{F_2}\lor \mathrm{F_1}, \mathrm{F_3}\lor (\mathrm{F_2}\land \mathrm{F_1}), \mathrm{F_4} \lor (\mathrm{F_3}\land (\mathrm{F_3}\land(\mathrm{F_2}\land \mathrm{F_1})), \mathrm{F_5}
\end{equation}
A questo punto la risoluzione di \(A'\) corrisponde a trovare una soluzione ottima per A. Si definisce quindi il \textit{costo(M,A)} come numero di soft constraint di A che sono falsi nell'interpretazione M. Di conseguenza:
\begin{equation}
\forall \text{ model M di F, }\textit{costo(M,A)} = 1+\textit{costo(M,A')}
\end{equation}
La dimostrazione è disponibile in un articolo pubblicato dall'università di Stanford \cite{Bjorner2019}.
\end{example}
% \todo[inline]{Non ho capitono la dimostrazione, la metto?}

\begin{example}
\footnotesize
Di seguito un esempio di definizione di un problema MaxSAT in Z3.
\begin{lstlisting}
from z3 import *
Auto, Patente, Bicicletta = Bools("auto patente bicicletta")
s = Optimize()
s.add(Or(And(Patente, Auto), Bicicletta))
s.add(Not(And(Auto, Bicicletta)))

s.add_soft(Bicicletta,1)
    
print(s.check())
print(s.model())

# output:
sat # s.check()
[bicicletta = True, patente = True, auto = False] # s.model()

# se aggiungo anche s.add_soft(Auto,2)
[bicicletta = False, patente = True, auto = True] # s.model()
\end{lstlisting}
\end{example}


\section{Integer Linear Programming}
% \todo[inline]{se riesci metti una frasetta...}
% \subsection{Problemi di programmazione lineare}
Un problema di programmazione intera vincolata è un problema ottimizzazione o ammissibilità in cui parte o tutte le variabili sono intere. Nella Tesi si utilizza un particolare caso di questo problema chiamato \textit{Integer Linear Programming} (ILP) in cui i vincoli e la funzione obiettivo sono lineari. La complessità del problema risulta NP-completa.

\subsection{Definizione}

Un problema di ottimizzazione lineare ha come scopo trovare la soluzione che minimizza la funzione obiettivo \(f\) tra tutte le soluzioni \(X\) che soddisfano l'insime di m vincoli \(V\) per le \(n\) variabili intere del problema  \cite{zambelliSimplesso}:
\begin{equation}
\begin{gathered}
    min(max) f(x)\\
    v_i(x) \leq,\geq o = b_i, \forall i = 1..m\\
    x \in \mathrm{N}^n
\end{gathered}
\end{equation}
dove:
\begin{itemize}
    \item \(x = (x_1,x_2,..,x_n) \) è il vettore di \(n\) variabili intere che rappresenta una possbilie soluzione del problema
    \item \(f(x)\) e tutte le \(v_i(x)\) sono definite come \(\mathrm{N}^n \rightarrow \mathrm{N} \)
    \item \(0 \leq i<m, \text{ } b_i \in \mathrm{N}\).
\end{itemize}

La linearità del problema permette di definire \(f\) e tutti i vincoli \(v_i\) come funzioni lineari delle variabili di \(x\):
\begin{equation}
\begin{gathered}
f: c_1x_1 + c_2x_2 + .. + c_nx_n\\
v_i: a_{i1}x_1 + a_{i2}x_2 + .. + c_{in}x_n = b_i\\
oppure:\\
v_i: a_{i1}x_1 + a_{i2}x_2 + .. + c_{in}x_n = b_i\\
oppure:\\
v_i: a_{i1}x_1 + a_{i2}x_2 + .. + c_{in}x_n = b_i, 0 \leq i < m\\
\end{gathered}
\end{equation}
Una \textit{soluzione ammissibile} di un problema di programmazione lineare è un vettore \(x_@\) che soddisfa tutti i vincoli.

Una \textit{soluzione ottima} di un problema di programmazione lineare è un vettore \(x_*\) che minimizza o massimizza la funzione obiettivo \(f\).

L'insieme \(X\) di tutte le soluzioni ammissibili è detto \textit{regione ammissibile}.

La risoluzione di un problema di programmazione lineare può ricadere in 3 casi:
\begin{itemize}
\item problema \textit{innammissibile}: l'insieme \(X\) delle soluzioni ammissibili è vuoto
\item problema \textit{illimitato}: è possibile trovare soluzioni ammissibili che migliorano la funzione obiettivo all'infinito
\item problema che \textit{ammette soluzione ottima}: esiste almeno una soluzione \(x_*\) che minimizza o massimizza la funzione obiettivo; ne segue che il valore k definito come \(f(x_*) = k\), appartiene ai numeri naturali.
\end{itemize}

% \todo[inline]{Esempio grafico}

% \todo[inline]{cercare formato per proprietà stile esempi}
\textbf{Proprietà 1}: Dato un problema di programmazione lineare, se il poliedro P delle soluzioni ammissibili è non vuoto e limitato, allora esiste almeno una soluzione ottima corrispondente con un vertica di P chiamato vertice di P ottimo.

% \todo[inline]{Chiedere ad Aldo se devo mettere richiami di Alg lineare}

\subsection{Forma standard}
Prima di procedere ad una manipolazione algebrica di un problema di programmazione lineare lo si trasforma nella \textit{forma standard}:
\begin{equation}\label{eqFormaStandardProgLineare}
    \begin{gathered}
    \mathrm{min } z: c_1x_1 + c_2x_2 + .. + c_nx_n\\
    \mathrm{s.t.} a_{i1}x_1 + a_{i2}x_2 + .. + a_{in}x_n = b_i, 0 \leq  m\\
        x_i \in \mathrm{N_{+}}
    \end{gathered}
\end{equation}
dove:
\begin{itemize}
\item la funzione obiettivo è di minimo (si moltiplicano per -1 le funzioni di massimizzazione)
\item  tutte le variabili sono positive o nulle (si effettuano cambi di variabili)
\item  tutti i vincoli sono delle equazioni (si aggiunge una variabile positiva di slack per i vincoli \(\leq\) e si sottrae una variabile positiva di surplus per i vincoli \(\geq\)
\item  i termini noti \(b_i\) sono tutti positivi o nulli (si moltiplicano per -1 i vincoli con termine noto negativo).
\end{itemize}
Questa trasformazione permette di risolvere il problema di programmazione lineare tramite un sistema di equazioni lineari.

\subsection{Soluzioni di base}
Un articolo di Zambelli \cite{zambelliSimplesso} introduce un metodo per risolvere un sistema di equazioni lineari facendo uso del concetto di base di una matrice. Sia data una matrice \(\mathrm{A} \in \mathrm{R^{m\times n}}\) di rango massimo. Una base di A è una sottomatrice quadrata di A di rango massimo definita come \(\mathrm{B} \in \mathrm{R^{m\times m}}\) ottenuta scegliendo \textit{m} colonne linearmente indipendenti della matrice A.


Da una rielaborazione del sistema lineare si può quindi scrivere:
\begin{equation}\label{eqMatrBasePlusF}
    \begin{gathered}
    Ax=b \Longrightarrow [B|F] \begin{bmatrix}x_B\\x_F \end{bmatrix} = Bx_B + Fx_F = b
    \end{gathered}
\end{equation}
dove F è l'insieme delle colonne di A non appartenenti alla base, \(x_B\) il vettore delle variabili corrispondenti alle colonne nella base e \(x_F\) il vettore delle restanti variabili.

Data l'invertibilità di B possiamo esplicitare nella \eqref{eqMatrBasePlusF} \(x_B\):
\begin{align}
    x_B = B^{-1}b + B^{-1}Fx_F
\end{align}
Al variare delle \((n-m)\) variabili fuori dalla base si ottengono differenti soluzioni \(\left[x_B x_F\right]\) che risultanto ammissibili soltanto se tutte le loro componenti sono positive. Una soluzione al sistema \(Ax=b\) si ottiene ponendo a 0 tutte le variabili fuori dalla base:
\begin{align}
    x = \begin{bmatrix}x_B\\x_F \end{bmatrix} = \begin{bmatrix}B^{-1}\\0\end{bmatrix}
\end{align}
Scelta una base B le soluzioni ottenute si dicono \textit{soluzioni di base} con al più \textit{m} variabili diverse da 0.

\textit{Caratterizzazione algebrica dei vertici di un politopo}: dato un sistema di equazioni \(Ax=b\) ed il corrispondente poliedro della regione ammissibile \(P=\{x \in \mathcal{R}^n:Ax=b\}\), x è soluzione base del sistema \(Ax=b \Leftrightarrow x\) è vertice di P.

\subsection{Metodo e algoritmo del simplesso}
Il metodo del simplesso permette di trovare la soluzione ottima di un problema di programmazione linerare partendo da una soluzione ammissibile sotto in modo iterativo generando ad ogni iterazione una nuova soluzione che migliora la precedente.

Di seguito vengono elencati i passaggi fondamentali del metodo, per una trattazione esaustiva fare riferimento all'articolo \cite{zambelliSimplesso}.

\begin{itemize}
    
    \item Passaggio alla forma standard: il problema va riscritto nella forma standard come descritto nella \eqref{eqFormaStandardProgLineare}, andando eventualmente a cambiare il verso della funzione obiettivo
    \begin{equation}
        \begin{gathered}
        \mathrm{min}\text{ } z = c^Tx\\
        \mathrm{t.c.}\text{ } Ax=b, x \geq 0
        \end{gathered}
    \end{equation}
    
    \item Scelta della base iniziale e passaggio alla forma canonica (o di tableau): viene scelta la base di partenza in modo che nei vincoli le variabili in base siano espresse unicamente in termini delle variabili non di base e che la funzione obiettivo sia scritta in termini delle sole variabili non di base. In termini matriciali moltiplicando per \(B^{-1}\) la \eqref{eqMatrBasePlusF} si ottiene:
    \begin{equation}
        \begin{gathered}
         \mathrm{min}\text{ } z = c^Tx\\
         Ix_B + B^{-1}Fx_F=B^{-1}b, x\geq 0
        \end{gathered}
    \end{equation}
    Con le sostituzioni \(x_B = B^{-1}b-B^{-1}Fx_F\) e successivamente \(\mathrm{\overline{F}}= B^{-1}F\text{, } \mathrm{\overline{c}^T_F}=c^T_F-c^T_BB^{-1}F \text{, } \mathrm{\overline{b}} = B^{-1}b \text{, e } z_B = c^T_BB^{-1}b\) si ottiene una definizione del problema equivalente all'originario dove \(z_B\) è il valore della funzione obiettivo per la soluzione di base \(x_B = B^{-1}b, x_F=0\) associata a B:
    \begin{equation}\label{eqFormaTableau}
        \begin{gathered}
         \mathrm{min}\text{ } z = \mathrm{\overline{c}}^T_Fx_F + z_B\\
         Ix_B + \mathrm{\overline{F}}x_F=\mathrm{\overline{b}}, x\geq 0
        \end{gathered}
    \end{equation}
    
    \item Scelta della variabile entrante per il cambio di base: permette di passare ad una soluzione ammissibile adiacente scambiando una variabile in base con una fuori base. La scelta della variabile da far entrare in base è determinata dalla ricerca di una nuova soluzione che migliori la funzione obiettivo. Partendo dalla defininizione della funzione obiettivo nella \eqref{eqFormaTableau} (forma di tableau) si ha:
    \begin{align}
        z = z_B + \mathrm{\overline{c}}^T_{F}x_{F} = \mathrm{\overline{c}}_{F_1}x_{F_1} + .. + \mathrm{\overline{c}}_{F_j}x_{F_j} + ..
    \end{align}
    da cui viene introdotta in base la variabile \(x_{F_j}\) che assumerà un valore positivo mentre le restanti variabili rimarranno a 0, da cui il nuovo costo della funzione obiettivo sarà:
    \begin{align}
        z = z_B+\mathrm{\overline{c}}_{F_j}x_{F_j}
    \end{align}
    Il valore \(\mathrm{\overline{c}}_{F_j}\) rappresenta quindi l'incremento marginale della funzione obiettivo all'aumentare di \(x_{F_j}\) e viene detto \textit{costo ridotto}. In conclusione conviene far entrare in base una variabile fuori base con costo ridotto negativo (\(\mathrm{\overline{c}}_{F_j} < 0\)) tale da avere un miglioramento della funzione obiettivo (\(x_{F_j}\) è > 0).
    
    \item Scelta della variabile uscente: data \(x_j\) la variabile appena entrata i base e \(\mathrm{\overline{a}}_{ij}\) il coefficiente della variabile \(x_j\) nel vincolo i-esimo, la variabile uscente sarà data dalla regola del quoziente minimo in quanto l'obiettivo è di massimizzare \(x_j\) senza violare i vincoli:
    \begin{align}
        \mathrm{min}_{i:\mathrm{\overline{a}}_{ij}>0} :\Biggl\{\frac{\mathrm{\overline{b}}_i}{\mathrm{\overline{a}}_{ij}}\Biggl\}
    \end{align}
    
    \item Cambio base (pivot): la variabile entrante \(x_j\) deve prendere posto nella riga della variabile uscente \(x_k\) nella nuova base.
    
    \item Terminazione: il problema può terminare in una condizione di ottimalità una volta che tutti i costi ridotti sono non negativi. Il probema è invece illimitato qualora tutti i coefficienti della colonna corrispondente alla variabile entrante sono negativi o nulli.

\end{itemize}

L'applicazione del metodo del simplesso richiede la presenza di una soluzione ammissibile di base. La ricerca di tale soluzione è possibile tramite il metodo delle due fasi; per ulteriori dettagli si faccia riferimento a \cite{zambelliSimplesso}.

\subsection{Il solver CPLEX}
In accordo con l'articolo \cite{cplexDocuLP} estratto dalla documentazione ufficiale del software CPLEX, esso è in grado di risolvere, tra gli altri, anche problemi di programmazione lineare. L'utilizzo del software in questa modalità prevede la definizione di vincoli lineari come quelli definiti nell'equazione \eqref{eqFormaStandardProgLineare}\footnote{In realtà CPLEX non accetta direttamente disuguaglianze del tipo \(\leq\) o \(\geq\), risulta tuttavia immediato il passaggio a < o >.}.

Il software implementa tre algoritmi per risolvere problemi di programmazione lineare:
\begin{itemize}
    
    \item Simplex Optimizer: prevede di muoversi lungo i bordi del poliedro per raggiungere i vertici rappresentanti una soluzione ammissibile per il problema, fino a raggiungere quello corrispondente alla soluzione ottima come mostrato in Figura~\ref{fig:SimpelxCPLEX}.
    \begin{figure}[tb]
        \centering
        \includegraphics[width=.6\textwidth]{images/figures/CPEX simplex.png}
        \caption{Algoritmo del Simplesso implementato in CPLEX.}
        \label{fig:SimpelxCPLEX}
    \end{figure}
    
    \item Dual-simplex Optimizer: la sua trattazione andrebbe al di fuori degli scopi della Tesi, si faccia riferimento a \cite{cplexDocuLP}.
    
    \item Barrier Optimizer: utilizza un approccio diverso muovendosi non lungo i bordi della regione ammissimibile ma di muoversi al suo interno correggendo continuamente il suo percorso tramite un algoritmo predictor-corrector. La Figura \ref{fig:BarrierCPLEX} mostra graficamente il comportamento di questo algoritmo.
    
    \begin{figure}
        \centering[tb]
        \includegraphics[width=.6\textwidth]{images/figures/CPLEX barrier method.png}
        \caption{Algoritmo Barrier Otpimizer.}
        \label{fig:BarrierCPLEX}
    \end{figure}
\end{itemize}


I vincoli logici definiti in termini di \textit{if\_then()}, \textit{logical\_and()} e \textit{logical\_or()} sono trasformati automaticamente in equazioni lineari con l'introduzione di ulteriori variabili in accordo con la documentazione ufficiale di CPLEX \cite{cplexOfficialDocu}.

\begin{example}
\footnotesize
Di seguito viene mostrato un semplice esempio di utilizzo del software CPLEX tramite le API per Python.
\begin{lstlisting}
# istanziazione del modello
mdl = CpoModel("Modello")

# definizione delle variabili del modello
mat1 = mdl.integer_var_list(LEN*LEN, -9, 9, "mat")
matSlack = mdl.binary_var_list(LEN*LEN, "slack")

# aggiunta dei vincoli
for i in range(LEN):
    mdl.add(mdl.sum([mat1[i*LEN+j] for j in range(LEN)]) == 10)
mdl.add(if_then(mat1[i] == 8, matSlack[i] == 1) for i in range(LEN*LEN))
mdl.add(mdl.sum([(mat1[i] == 9) * 1 for i in range(LEN*LEN)]) <= 30)

# definizione della funzione obiettivo
mdl.minimize(mdl.sum(mat1[i] for i in range(LEN*LEN)))

# avvio del solver
msol = mdl.solve(TimeLimit=10)
\end{lstlisting}
\end{example}