Synergies and Applications of Maximum Satisfiability and Automatic Configuration

Abstract

Aquest document presenta els resultats de la tesi "Synergies and Applications of Maximum Satisfiability and Automatic Configuration", on hem treballat amb la tecnologia de la Màxima Satisfactibilitat (MaxSAT) i la tecnologia de configuració automàtica (AC), i crea sinergies entre elles per millorar-ne l'eficàcia. En particular, podem dividir aquest treball en tres blocs principals:

En primer lloc, hem explorat com aplicar la tecnologia MaxSAT al problema de l'Arbre de Decisió Pur Mínim (MPDT problem). Proporcionem una nova codificació MaxSAT per al problema i una estratègia de resolució alternativa. Mostrem l'eficàcia del nostre enfocament, obtenint resultats similars o millors que l'eina Scikit-Learn.

El segon bloc aplica la tecnologia d'AC de forma exitosa al problema d'ajustar models epidèmics. Presentem un enfocament agnòstic que permet ajustar els models epidèmics usats en els processos de decisió, i demostrem que el nostre enfocament aconsegueix ajustar millor que alguns mètodes existents. Finalment, presentem una eina que facilita l'ús d'aquesta tecnologia.

Finalment, l'últim bloc se centra a connectar MaxSAT i AC per millorar el rendiment dels resolutors MaxSAT anytime. Mostrem que podem millorar els resultats que van aconseguir aquests resolutors en la MaxSAT Evaluation 2023. La novetat presentada és un nou enfocament per crear "sequential portfolios" a partir de configuracions descartades durant el procés d'AC i aconsegueixen obtenir resultats encara millors.

Este documento presenta los resultados de la tesis “Synergias y Applications of Maximum Satisfiability and Automatic Configuration”, donde hemos trabajado con la tecnología de la Máxima Satisfactibilidad (MaxSAT) y la tecnología de configuración automática (AC), y crea sinergias entre ellas para mejorar su eficacia. En particular, podemos dividir este trabajo en tres bloques principales:

En primer lugar, hemos explorado cómo aplicar la tecnología MaxSAT al problema del Árbol de Decisión Puro Mínimo (MPDT problem). Proporcionamos una nueva codificación MaxSAT para el problema y una estrategia de resolución alternativa. Mostramos la eficacia de nuestro enfoque, obteniendo resultados similares o mejores que Scikit-Learn.

El segundo bloque aplica la tecnología de AC de forma exitosa en el problema de ajustar modelos epidémicos. Presentamos un enfoque agnóstico que permite ajustar los modelos epidémicos usados ​​en los procesos de decisión, demostrando que nuestro enfoque consigue ajustar mejor que algunos métodos existentes. Por último, presentamos una herramienta que facilita el uso de esta tecnología.

Por último, el último bloque se centra en conectar MaxSAT y AC para mejorar el rendimiento de los resolutores MaxSAT anytime. Mostramos podemos mejorar los resultados que consiguieron estos resolutores en la MaxSAT Evaluation 2023. La novedad presentada es un nuevo enfoque para crear “sequential portfolios” a partir de configuraciones descartadas durante el proceso de AC para obtener mejores resultados.

This document presents the results of the thesis "Synergies and Applications of Maximum Satisfiability and Automatic Configuration", which works with the technology of Maximum Satisfiability (MaxSAT) and the technology of Automatic Configuration (AC), and creates synergies between them to improve their effectiveness. In particular, we can divide this work into three main blocks:

First, we explored how to apply MaxSAT technology to the Minimum Pure Decision Tree problem (MPDT problem). We provide a new MaxSAT encoding for the problem and an alternative solution strategy. We show the effectiveness of our approach, obtaining similar or better results than the Scikit-Learn tool.

The second block successfully applies AC technology to the problem of fitting epidemic models. We present an agnostic approach that allows fitting epidemic models used in decision processes, and we demonstrate that our approach manages to fit better than some existing methods. Finally, we present a tool that facilitates the use of this technology.

Finally, the last blog focuses on connecting MaxSAT and AC to improve the performance of MaxSAT anytime solvers. We show that we can improve the results achieved by these solvers in the MaxSAT Evaluation 2023. The novelty presented is a new approach to creating "sequential portfolios" from configurations discarded during the AC process to manage to obtain even better results.