[en] The Satisfiability problem, or SAT, is the problem of deciding if there exists an assignment that satisfies a given propositional formula. SAT was the first problem proven to be NP-complete and is one of the most studied problems in Computer Science. On the other hand, MaxSAT and MinSAT are optimization versions of SAT where the goal is to find an assignment that maximizes or minimizes the number of satisfied clauses, respectively. All these problems are significant because many practical problems can be encoded as SAT, MaxSAT or MinSAT problems, and solved using a SAT, MaxSAT or MinSAT solver. While SAT is used to solve decision problems, MaxSAT and MinSAT are used to solve optimization problems. The general objective of this PhD thesis is to advance the state of the art in solving computationally difficult optimization problems by reducing them to MaxSAT and MinSAT. To achieve this objective, we have investigated new inference systems for MaxSAT and MinSAT based on semantic tableaux, and suitable encodings for new MaxSAT applications. Regarding inference systems, the thesis defines a complete tableau calculus for solving clausal MaxSAT, a complete tableau calculus for solving clausal MinSAT and a complete tableau calculus for solving both clausal MaxSAT and clausal MinSAT. Moreover, the thesis proposes two different approaches to solving non-clausal MaxSAT and non-clausal MinSAT: in the first approach, the thesis defines novel cost-preserving transformations from non-clausal MaxSAT to clausal MaxSAT. Such transformations are then extended to define cost-preserving transformations from non-clausal MinSAT to clausal MinSAT. In the second approach, the thesis defines a genuine tableau calculus for non-clausal MaxSAT and proves its soundness and completeness. It also describes how the tableau calculus for non-clausal MaxSAT can be used to solve non-clausal MinSAT. Regarding new MaxSAT applications, the thesis defines and empirically evaluates MaxSAT encodings for the team composition problem in a classroom and proves that this problem is NP-hard. The insights gained are useful for solving other challenging optimization problems via their reduction to MaxSAT. In particular, the thesis shows how to solve more complex team formation problems, using the synergistic team composition model as a case study.

[es] El problema de la Satisfacibilidad (SAT) consiste en decidir si existe una asignación de valores de verdad que satisfaga una fórmula proposicional dada. SAT fue el primer problema para el cual se demostró su NP-completitud, siendo uno de los problemas más estudiados en Ciencias de la Computación. Por otro lado, MaxSAT y MinSAT son versiones de optimización de SAT en las cuales el objetivo es encontrar una asignación que maximice o minimice el número de cláusulas satisfechas, respectivamente. Estos problemas son importantes porque muchos problemas prácticos pueden codificarse como problemas SAT, MaxSAT o MinSAT, y resolverse utilizando un resolvedor para SAT, MaxSAT o MinSAT. Mientras SAT se utiliza para resolver problemas de decisión, MaxSAT y MinSAT se utilizan para resolver problemas de optimización. El objetivo general de esta tesis doctoral es avanzar en el estado del arte en la resolución de problemas de optimización computacionalmente difíciles via su reducción a MaxSAT y MinSAT. Para lograr este objetivo, hemos estudiado nuevos sistemas de inferencia para MaxSAT y MinSAT basados en tableaux semánticos, y hemos definido codificaciones adecuadas para problemas que todavía no habían sido resueltos mediante su reducción a MaxSAT y MinSAT. En cuanto a los sistemas de inferencia, la tesis define un cálculo de tableaux completo para MaxSAT clausal, un cálculo de tableaux completo para MinSAT clausal y un cálculo de tableaux completo que permite resolver tanto MaxSAT como MinSAT. Además, la tesis propone dos enfoques diferentes para resolver MaxSAT no clausal y MinSAT no clausal: en el primer enfoque, la tesis define transformaciones de MaxSAT no clausal a MaxSAT clausal que preservan el coste. Además, define la extensión de estas transformaciones de MinSAT no clausal a MinSAT clausal. En el segundo enfoque, la tesis define un cálculo de tableaux para MaxSAT no clausal y demuestra su consistencia y completud. También describe cómo el cálculo de tableaux para MaxSAT no clausal puede utilizarse para resolver MinSAT no clausal. En cuanto a las nuevas aplicaciones de MaxSAT, la tesis define codificaciones MaxSAT para el problema de composición de equipos en un aula, las evalúa empíricamente y demuestra que este problema es NP-duro. Los conocimientos adquiridos son útiles para resolver otros problemas de optimización con tecnología MaxSAT. En particular, la tesis muestra cómo resolver problemas de formación de equipos más complejos, utilizando el modelo de composición de equipos sinérgicos como caso de estudio.