Breaking down group testing. A MaxSAT based framework with theoretical perspectives

The success of MaxSAT (Maximum Satisfiability) solving in recent years has motivated researchers to apply MaxSAT solvers in diverse discrete combinatorial optimization problems. Group testing has been studied as a combinatorial optimization problem, where the goal is to find defective items among a set of items by performing tests on pools of items. In this thesis work, we propose a MaxSAT-based framework, called MGT, that solves the decoding phase of non-adaptive group testing. Such approach is motivated by past studies over the optimality of the so called Smallest Satisfying Set. We encode such formulation with partially-weighted MaxSAT and extend it to the noisy variant of group testing. We prove equivalence of a compact MaxSAT-based encoding and derive guarantees of optimality of its tuning. We perform an extensive experimental evaluation which shows that MGT grants unprecedeneted scalability feature in terms of number of items handled. Furthermore, MGT performance are impressive compared to all the other algorithms implemented as test bed. We leave a window wide open on theoretical perspective trying to give an interpretation to the observed phase transition with respect to the number of tests with an easy-hard-easy behaviour. This kind of transition has been already detected, but never deeply understood, in other artificial intelligence problem such as randomk-SAT.

Il successo nello sviluppo di risolutori per il problema MaxSAT(massima soddisfacibilità) negli ultimi anni ha motivato i ricercatori ad applicare tali codifiche, e quindi i relativi algoritmi, in diversi problemi discreti di ottimizzazione combinatoria. Il test di gruppo (Group Testing) è stato studiato come un problema di ottimizzazione combinatoria, in cui l’obiettivo è quello di trovare, data una serie di elementi, coloro i quali presentano una certa caratteristica, in generale chiamata difettosità, eseguendo test su sottogruppi di essi. In questo lavoro di tesi, proponiamo un framework basato su MaxSAT, chiamato MGT, che computa una soluzione per la fase di decodifica dei test in un contesto non adattativo. Tale approccio è motivato da studi precedenti riguardo l'ottimalità del cosiddetto Small Satisfying Set (minor insieme di soddisfacibilità). Codifichiamo la citata formulazione attraverso una particolare versione di MaxSAT(Partially Weighted)e la estendiamo con una variante in grado di considerare e gestire errori nei risultati dei test. Dimostriamo l’equivalenza di due codifiche basate su MaxSAT, la prima triviale, data la formulazione del problema di ottimizzazione, e la seconda compatta, in termini di clausole generate, ottenendone garanzie di ottimalità. A partire da una valutazione sperimentale approfondita mostriamo che MGT offre una scalabilità senza precedenti in termini di numero di elementi considerabili nel problema. Inoltre le prestazioni di MGT sono impressionanti rispetto a tutti gli altri algoritmi implementati come banco di prova. Per concludere delineiamo una prospettiva teorica cercando di dare un’interpretazione alla transizione di fase osservata, riguardante la probabilità di successo e il comportamento del problema in termini di complessità temporale come Facile-Difficile-Facile (in letteratura esattamente definita Easy-Hard-Easy), con dipendenza dal numero di test. Questo tipo di transizione è già stata osservata sperimentalmente, ma mai profondamente compresa, in altri problemi di intelligenza artificiale come la versione randomica di k-SAT.