In questo progetto consideriamo diversi aspetti dello studio di
algoritmi su grafi: (1) la sintesi di nuovi algoritmi per problemi
importanti; (2) l'analisi degli algoritmi noti e i lori limiti di
efficienza; (3) l'implementazione distribuita di algoritmi per
applicazioni dove tipicamente i grafi sono enormi.
Il progetto si occupa della sintesi di algoritmi per importanti
parametri come la vitalità e la centralità di elementi del grafo,
parametri calcolati rispetto a problemi come quello del flusso massimo
o dei cammini minimi. Tipicamente questi problemi hanno complessità
quadratica, che non è accettabile per grafi di grandi dimensioni.
L'analisi teorica di algoritmi per problemi sui grafi è basata
principalmente sulla proof complexity ovvero sullo studio dei
certificati di insoddisfacibilità che questi algoritmi producono.
Questi certificati vengono studiati per dare limiti inferiori
all'efficienza dei corrispondenti algoritmi (e.g. se il certificato
deve essere molto lungo, l'algoritmo deve impiegare molto tempo
a produrlo). Questi certificati possono anche essere usati per
verificare la correttezza delle computazioni.
Per la parte sperimentale si considerano i grafi che rappresentano le
interazioni tra gruppi di proteine. Tipicamente questi grafi sono
enormi e non possono essere memorizzati su un singolo calcolatore, il
che esclude la possibilità di analizzali con gli algoritmi sequenziali
presenti in letteratura. Qui cerchiamo di impostare versioni
distribuite di questi algoritmi nell'architettura MarReduce, oppure di
ideare nuovi algoritmi adatti al contesto.
Mentre per grafi s-t planari è stato mostrato come calcolare la
vitalità di tutti gli archi del grafo rispetto al flusso massimo in
tempo ottimale (cioè in tempo pari al tempo necessario per calcolare
il flusso stesso), non sono noti algoritmi efficienti per lo stesso
problema su grafi planari non s-t. Nell'ambito del progetto ci si
propone di esaminare il caso planare generale, o una classe comunque
più ampia dei grafi s-t planari, e di studiare eventuali riducibilità
tra il problema della vitalità e il problema del calcolo del flusso
massimo. Vista la stretta connessione tra problemi di flusso e di
cammino minimo nel caso planare, si intende anche studiare il problema
del cammino minimo tra coppie multiple, in cui a partire da un insieme
di k coppie s_i-t_i si vuole individuare un cammino minimo per
ciascuna delle k coppie. L'obiettivo è semplificare e/o estendere
i risultati presentati in [Takahashi], possibilmente senza far ricorso
a strutture di dati di complessa implementazione.
L'uso della proof complexity per l'analisi degli algoritmi è un metodo
che ha dato frutti importanti ma che ancora è in stato embrionale, ci
sono ancora molti problemi lasciati aperti dai primi articoli
pubblicati sul tema. Questo progetto vuole consolidare la metodologia
e portarla a maturazione. Sarebbe un progresso significativo modellare
algoritmi per l'ottimizzazione combinatoria tramite dimostrazioni in
Cutting Planes, per poi dimostrare lower bound sul tempo di
esecuzione. Membri di questo gruppo di lavoro hanno già ottenuto
risultati notevoli per sistemi più semplici [STOC 2018]), ed
è ragionevole credere possano fare progressi in questo senso.
L'uso dei sistemi di dimostrazioni proposto non è solo un modo per
analizzare algoritmi, è anche uno strumento per la verifica delle
computazioni. Qualunque programma, anche se ben pensato e ben
implementato, può contenere errori. Ma ancora più sottile è il
pericolo che un programma corretto possa essere eseguito in maniera
difettosa. La verifica formale del software non ci salva da questo,
mentre la produzione di una dimostrazione di correttezza della
computazione dà maggiori garanzie. Rendere praticabile questa idea non
è affatto banale ma recentemente ci sono stati dei passi [IJCAI 2020,
AAAI 2020], grazie all'uso di PseudoBoolean Solvers basati su
cutting planes.
La prevalenza degli algoritmi sviluppati sino ad oggi per l'analisi di
PPI networks è concepita per operare su architetture di calcolo
sequenziali, con evidenti ripercussioni sui tempi di analisi e sulla
trattabilità dei problemi nel caso di reti di dimensioni molto grandi.
L'uso dell'approccio distribuito consente di incrementare
significativamente il range di problemi trattabili permettendo, al
contempo, di ridurre il tempo di risoluzione dei problemi in
proporzione alle risorse di calcolo allocate. Nel caso del progetto in
questione, la realizzazione di algoritmi distribuiti basati su
MapReduce consentirebbe di ottenere un ottimo speed-up rispetto alle
soluzioni tradizionali. Tale risultato sarebbe inoltre sostanziato
dalla realizzazione di una serie di implementazioni prototipali degli
algoritmi in questione, al fine di valutarne l'efficienza sperimentale
e la scalabilita'. A tal proposito, si utilizzerebbero come benchmark
alcune delle PPI networks piu' note e meglio caratterizzate in
letteratura, quali quelli disponibili presso la Stanford Biomedical
Network Dataset Collection.
[STOC 2018] Albert Atserias, Ilario Bonacina, Susanna de Rezende,
Massimo Lauria, Jakob Nordstrom and Alexander Razborov. Clique is hard
on average for regular resolution.
[IJCAI 2020] Stephan Gocht, Ciaran McCreesh and Jakob Nordström:
Subgraph Isomorphism Meets Cutting Planes: Solving With
Certified Solutions.
[AAAI 2020] Jan Elffers, Stephan Gocht, Ciaran McCreesh and Jakob
Nordström: Justifying All Differences Using Pseudo-Boolean Reasoning.
[Takahashi] Jun-ya Takahashi, Hitoshi Suzuki, Takao Nishizeki.
Shortest Noncrossing Paths in Plane Graphs. Algorithmica 16(3):
339-357 (1996)