Il nostro obiettivo è studiare le soluzioni efficienti di problemi computazionali da un punto di vista più organico possibile. Lo studio ha tre parti: (1) determiniamo limiti inferiori all'efficienza delle soluzioni utilizzando una combinazione dei metodi della complessità computazionale e della proof theory; (2) progettiamo algoritmi per la soluzione di problemi su grafi computazionalmente complessi; (3) sviluppiamo algoritmi sperimentalmente efficienti per la risoluzione di problemi caratterizzati da istanze di taglia estremamente elevate (big data), anche mediante un approccio distribuito.
Per il primo punto partiamo da problemi specifici, e.g. soddisfacibilità nella logica proposizionale (satisfiability), colorazione di grafi, ricerca di clique, per poi studiare le performance di algoritmi. L'intenzione è di dimostrare limitazioni inferiori all'efficienza senza fare uso di assunzioni non dimostrate (come invece si fa nella teoria dell'NP-completezza), ma studiando la "proof complexity". Essenzialmente analizzeremo l'efficienza di algoritmi per grafi e dimostreremo matematicamente che non sono efficienti.
Per il secondo punto si studieranno problemi su grafi di complessità elevata, come ad esempio la sensibilità del massimo flusso rispetto a variazioni della capacità di archi, e altre generalizzazioni che presentano complessità computazionali quadratiche, o comunque superlineari, rispetto alla dimensione del grafo, e problemi nell'ambito della Formal Concept Analysis
Per il terzo punto il progetto si concentrerà su particolari categorie di problemi, particolarmente studiate in ambito bioinformatico, che hanno come scopo quello di confrontare due o più sequenze di caratteri allo scopo di determinarne la similarità. Ci si concentrerà in particolare su algoritmi di tipo alignment-free, che consentono di stimare il grado di similarità di due sequenze in un tempo subquadratico rispetto alla taglia delle stesse.
Punto 1. Complessità computazionale
Per risolvere un problema computazionale si vuole usare l'algoritmo più efficiente possibile, naturalmente. Mentre si cercano algoritmi sempre più veloci, la teoria della complessità computazionale cerca di dimostrare matematicamente che certi problemi non possono avere soluzioni più efficienti di un certo limite. Ottenere questi risultati è molto complesso: come si fa infatti ad affermare che nessun algoritmo (neppure quelli ancora da scoprire) può superare un certo limite? L'uso dell'ipotesi non dimostrata "P diverso da NP" fornisce una base su cui appoggiarsi, ma il nostro progetto vuole superare questa scelta.
Le tecniche della proof complexity che verranno usate in questo progetto, benché consolidate e robuste quando si tratta di studiare la soddisfacibilità nella logica proposizionale, vanno sviluppate molto se si vogliono applicare a problemi su grafi. Sono pochi i risultati già noti. Una difficoltà è che nella letteratura della proof complexity le formule UNSAT studiate sono ad hoc e artificiali, fatte apposta per non avere dimostrazioni brevi. Invece nel nostro caso il problema iniziale proviene dalla teoria dei grafi e deve essere codificato in una formula che non possiamo controllare completamente. Questo vuol dire che dare dei lower bound alla sua refutazione può essere molto più difficile, come in effetti è stato nei pochi casi già risolti.
Oltretutto più l'algoritmo da studiare è utile e complesso, più il proof system corrispondente deve essere espressivo, e quindi dimostrare limitazioni inferiori alla lunghezza delle refutazioni in quel sistema diventa più difficile.
Grazie a questa linea di ricerca potremmo avere una comprensione maggiore di svariati algoritmi per problemi su grafi, specialmente quelli usati in pratica, e questo può anche dare lo spunto per implementarne di nuovi.
Punto 2. Algoritmi superlineari su grafi
Intendiamo progettare algoritmi efficienti per la determinazione della vitalità di singoli archi e/o di singoli nodi, anche per classi specifiche di grafi. In particolare si studieranno classi di grafi planari, o classi in cui è possibile determinare efficientemente la vitalità non solo di singoli archi ma di insiemi di archi/nodi corrispondenti a strutture locali o con elevata connettività.
Su grafi bipartiti, si studieranno estensioni della classe dei grafi domino-free o C6-free, poiché per tali classi esistono già caratterizzazioni dei grafi in termini di caratteristiche del reticolo, e di conseguenza algoritmi efficienti per il calcolo esplicito del reticolo. Con riferimento a queste ultime classi di grafi, si studieranno estensioni del concetto di "convessità" di un grafo bipartito, che in alcuni casi noti induce una struttura particolarmente semplice del reticolo. Così come attualmente si conoscono rappresentazioni implicite in termini di cammini su una arborescenza (come nel caso di grafi convessi è noto che le biclique massimali sono rappresentabili come sottointervalli in un ordinamento lineare), si cercherà di determinare possibili generalizzazioni di tali rappresentazioni implicite.
Punto 3. Algoritmi sperimentalmente efficienti
L'oggetto della ricerca è, ad oggi, decisamente attuale. I progressi compiuti con le tecnologie per il sequenziamento dei genomi mette a disposizione della comunità scientifica una quantità ingente di dati difficile da analizzare con gli approcci tradizionali. D'altro canto il ricorso ai sistemi distribuiti di ultima generazione non è sufficiente, da solo, a garantire prestazioni in linea con le aspettative dal momento che framework come Spark ed Hadoop sacrificano sovente l'efficienza sperimentale in cambio della semplicità d'uso. Per questo motivo, l'innovatività della ricerca da condursi sarà nella possibilità di progettare algoritmi che siano efficienti sia da un punto di vista computazionale che sperimentale. Così facendo, si realizzerebbe un deciso passo avanti rispetto alla letteratura scientifica, dal momento che le uniche soluzioni ad oggi disponibili per il confronto di sequenze con metodi alignment-free operano su architetture sequenziali oppure, pur essendo formulate come algoritmi distribuiti (Cattaneo et al., 2016), non sono in grado di sfruttare in modo ottimale le risorse del sistema di calcolo sottostante.