Contributions to automatic configuration and selection for satisfiability

Abstract

En l’àrea de les ciències de la computació, és sabut que els algoritmes poden exhibir comportaments completament diferents depenent de com estiguin configurats els seus paràmetres, fet que s’aguditza quan els problemes que s’aborden són NPComplets. Per exemple, s’ha demostrat experimentalment que configurar solvers pels problemes de la SATisfactibilitat (SAT), la Màxima SATisfactibilitat (MaxSAT) o la programació lineal d’enters mixta (MIP), pot resultar en millores d’ordres de magnitud.

En aquesta tesi, mostrem com algoritmes metaheurístics configurats de manera automàtica poden resoldre de forma eficient diverses families d’instancies industrials i artificails del problema MaxSAT. A continuació, ens centrem a millorar el configurador automàtic d’algoritmes GGA proporcionant un nou configurador distribuït que el supera en diverses famílies d’instancis industrials i artificials dels problemes SAT i MIP.

Finalment, per fer aquesta tecnologia més accessible a totes les comunitats científiques i la indústria, presentem l’eina PyDGGA que implementa el nostre nou configurador. A més, presentem el paquet OptiLog, el qual permet la creació ràpida de sistemes basats en SAT que addicionalment incorpora un mòdul de configuració automàtica per facilitar l’ús de diverses eines de configuració.

En el área de las ciencas de la computación, es sabido que los algoritmos pueden exhibir comportamientos completamente diferentes dependiendo de como estén configurados sus parámetros, agudizándose este fenómeno cuando los problemas que se abordan son NP-Completos. Por ejemplo, se ha demostrado experimentalmente que configurar solvers para los problemas de la SATisfactibilidad (SAT), la Maxima SATisfactibilidad (MaxSAT) o la programación lineal de enteros mixta (MIP), puede resultar en mejoras de órdenes de magnitud.

En esta tesis, mostramos cómo algoritmos metaheurísticos configurados de manera automática pueden resolver de forma eficiente diversas familias de instancias industriales y artificiales del problema MaxSAT. A continuación, nos centramos en mejorar el configurador automático de algoritmos GGA proporcionando un nuevo configurador distribuido que lo supera en varias familias de instancias industriales y artificiales de los problemas SAT y MIP.

Finalmente, para hacer que esta tecnología sea más accesible para todas las comunidades científicas y la industria, presentamos la herramienta PyDGGA que implementa nuestro nuevo configurador. Además, presentamos el paquete OptiLog el cual permite la creación rápida de sistemas basados en SAT que adicionalmente incorpora un módulo de configuración automática para facilitar el uso de varias herramientas de configuración.

Within the computer science community, it is well known that algorithms may exhibit completely different behaviours depending on how their parameters are configured. This is even more obvious when the problems being tackled are NP-Complete. For example it has been proved experimentally that configuring solvers for the SATisfiabilty (SAT) problem, the Maximum SATisfiability (MaxSAT) problem or for Mixed Integer Programming (MIP), can result in improvements of orders of magnitude.

In this thesis, we show how automatically configured metahueristic algorithms can efficiently solve families of industrial and crafted instances of the MaxSAT problem. Then, we focus on improving the automatic algorithm configurator GGA providing a new distributed configurator which outperforms GGA on families of industrial and crafted SAT and MIP instances.

Finally, in our aim of making this technology more accessible for all research communities and industry we present the tool PyDGGA that implements our new configurator. We additionally introduce the OptiLog framework for rapid prototyping of SAT-based systems that also incorporates a module for automatic configuration for the easy application of several configuration tools.