Tesi di laurea sulla programmazione a vincoli

Panoramica

Il simulatore esamina ripetutamente molte condizioni man mano che aumentano gli eventi possibili. Allora, se dal progresso si può giudicare che "questa condizione non si verificherà mai più", non si potrebbe smettere di verificarla in modo sicuro? Abbiamo progettato e implementato un metodo per il linguaggio di modellazione dei sistemi ibridi HydLa, che esclude le condizioni non necessarie dalla ricerca in corso utilizzando come indizio la direzione della variazione dei valori.

Nel modello di valutazione, il tempo di esecuzione è stato ridotto a circa la metà rispetto al metodo tradizionale, senza modificare i risultati della simulazione. L'importante non è stato velocizzare uniformemente tutti i calcoli, ma piuttosto ridurre le possibilità da considerare sfruttando la struttura del problema.

Il concetto di programmazione a vincoli appreso in questo studio costituisce la base dell'attuale La mia filosofia di design. Non si tratta di specificare direttamente i risultati uno per uno, ma di definire regole, priorità e confini, e di derivare le soluzioni che si realizzano all'interno di essi.

Problema — più aumentano le possibilità, più i calcoli diventano lenti

HydLa è un linguaggio per descrivere i "sistemi ibridi", in cui si combinano cambiamenti continui ed eventi discreti, come vincoli matematici e logici. Anche senza scrivere tutte le sequenze delle procedure, dichiarando ciò che deve essere soddisfatto è possibile simulare un comportamento che rispetta le condizioni.

D'altra parte, nei modelli in cui le regole diventano valide a seconda delle condizioni, il simulatore verifica ripetutamente un gran numero di candidati. Poiché rimangono candidati anche le condizioni già superate e quelle che non si verificheranno in futuro, man mano che il modello cresce, i calcoli inutili si accumulano.

Tema — un sistema in cui si mescolano continuo e discreto

Una palla che rimbalza è un esempio chiaro di un sistema ibrido. In aria, posizione e velocità cambiano continuamente, mentre nel momento in cui tocca il pavimento avviene un evento discreto, il rimbalzo. Anche termostati, automobili e robot, pur su scale diverse, possiedono internamente gli stessi due tipi di cambiamento.

Per la valutazione è stato utilizzato un modello in cui una palla che si muove orizzontalmente rimbalza su una superficie suddivisa in più settori. Ogni settore della superficie ha una regola condizionale del tipo "se la palla arriva in questo intervallo, rimbalza". Aumentando il numero di settori, aumenta la gamma degli oggetti che si possono rappresentare, ma aumentano anche le condizioni da esaminare per il simulatore.

Collo di bottiglia — il numero di condizioni aumenta la complessità computazionale

Una regola che diventa valida solo quando le condizioni sono soddisfatte è chiamata 'vincolo con guardia'. Nel modello di valutazione, la regola di rimbalzo di un'area diventa valida solo quando la palla raggiunge il pavimento e la sua posizione orizzontale è all'interno di quella specifica area.

Aumentando il numero di lotti da 10 a 200, i simulatori tradizionali diventavano circa proporzionalmente più lenti al quadrato del numero di lotti. Nei modelli di grande scala, poiché aumentano gli oggetti, le aree di contatto e gli eventi possibili, lo stesso problema diventa più grande.

Indagine — Dove si trovava il 96% del tempo di elaborazione

Misurando il tempo di elaborazione, nel modello con 100 sezioni, il 96% del tempo totale veniva utilizzato per FindMinTime. Si tratta del processo di ricerca del "prossimo evento più imminente" tra i candidati. Pertanto, tutte le condizioni di guardia venivano valutate ripetutamente.

I punti da migliorare sono diventati chiari. Non è necessario rifare l'intero metodo di calcolo, basta ridurre in sicurezza i candidati da passare a FindMinTime. L'obiettivo era evitare solo le possibilità che non è necessario verificare, senza modificare i risultati della simulazione.

Approccio — Rimuovere in sicurezza le condizioni che non si realizzeranno mai più

Immagina una palla che scende saltando le scale. Quando la palla supera un gradino e continua a muoversi in avanti, quel gradino non può più influenzare la palla. Chi guarda il diagramma ignora immediatamente i gradini dietro la palla. L'algoritmo originale continuava invece a esaminarli uno a uno.

La difficoltà sta nella parte che deve dimostrare che le guardie rimosse non saranno necessarie in seguito. Se le rimuovi solo perché al momento sono false, quando diventeranno di nuovo vere, potrebbero restituire dei risultati incorretti senza alcun avviso. La metodologia proposta utilizza quindi la monotonicità: si tratta di capire se è possibile garantire che una certa variabile continui ad aumentare o a diminuire durante un certo intervallo di tempo.

Quando la direzione del cambiamento non cambia

La prima misura si applica quando una variabile si muove in una sola direzione per tutta la simulazione. In un modello con la superficie suddivisa, la posizione orizzontale della palla aumenta sempre. Una volta superata una sezione, le condizioni di quella sezione non saranno più soddisfatte. Questa proprietà può essere verificata prima della simulazione tramite tecniche di model checking, quindi le guardie non più necessarie possono essere rimosse in sicurezza man mano che l'esecuzione procede.

Quando la direzione del cambiamento cambia a metà

Molti sistemi reali non si muovono in una sola direzione per sempre. Le variabili possono aumentare, cambiare direzione e poi diminuire. In questo contesto, il documento ha presentato una seconda corrispondenza. Prima, si assume una direzione, si monitora tale ipotesi con un'asserzione e si rifà il processo di riduzione dal momento in cui la direzione cambia. La guardia rimossa per un intervallo monotono viene ripristinata quando inizia l'intervallo successivo.

Risultato — Tempo di esecuzione del modello di valutazione ridotto di circa metà

Abbiamo implementato la gestione della monotonicità uniforme e valutato il modello suddividendo la superficie. Sia l'algoritmo originale sia il metodo proposto hanno tempi di esecuzione maggiori con l'aumentare del numero di suddivisioni. Tuttavia, il metodo proposto richiedeva costantemente meno lavoro. Confrontando le curve adattate, il coefficiente di ordine più alto è passato da 1,1463 a 0,6083, e in questo benchmark il tempo totale di simulazione si è ridotto circa della metà.

Questo non è un'affermazione che ogni modello HydLa diventerà il doppio più veloce. Ciò che viene indicato è dove questo metodo funziona: modelli che hanno molti oggetti con guardie, nei quali la direzione delle variazioni può essere dimostrata e le guardie divengono permanentemente irrilevanti durante l'esecuzione.

La prospettiva acquisita da questa ricerca

In questa ricerca, non si trattava di rendere ogni singolo calcolo un po' più veloce. Si trattava di usare ciò che si sa sul comportamento del sistema per ridurre l'insieme delle possibilità da considerare. L'idea di restringere lo spazio di ricerca senza cambiare i risultati è il punto di forza della programmazione a vincoli.

Abbiamo implementato e valutato il caso in cui le variabili continuano a muoversi in una sola direzione. Nel caso in cui la direzione del cambiamento cambi a metà, ci si è limitati alla progettazione, lasciando la valutazione come compito futuro. Utilizzando proprietà diverse dalla monotonicità, c'è anche spazio per identificare ulteriori vincoli non necessari.

Il motivo per cui attualmente cerco di progettare le condizioni e i confini che l'IA può esplorare, piuttosto che progettare direttamente l'output dell'IA, è collegato a questa esperienza. Quando si trattano risultati complessi, è importante definire cosa non è necessario considerare tanto quanto cosa calcolare.