[ca] El problema de la Satisfactibilitat (SAT) consisteix a decidir si existeix una assignació de valors de veritat que satisfaci una fórmula proposicional donada. SAT va ser el primer problema per al qual es va demostrar la seva NP-completitud, sent un dels problemes més estudiats en Ciències de la Computació. D'altra banda, MaxSAT i MinSAT són versions d'optimització de SAT en les quals l'objectiu és trobar una assignació que maximitzi o minimitzi el nombre de clàusules satisfetes, respectivament. Aquests problemes són importants perquè molts problemes pràctics poden codificar-se com a problemes SAT, MaxSAT o MinSAT, i resoldre's utilitzant un resolvedor SAT, MaxSAT o MinSAT. Mentre que SAT s'utilitza per resoldre problemes de decisió, MaxSAT i MinSAT s'utilitzen per resoldre problemes d'optimització. L'objectiu general d'aquesta tesi doctoral és avançar en l'estat de l'art en la resolució de problemes d'optimització computacionalment difícils via la seva reducció a MaxSAT i MinSAT. Per aconseguir aquest objectiu, hem investigat nous sistemes d'inferència per MaxSAT i MinSAT basats en tableaux semàntics, i definit codificacions adequades per a noves aplicacions MaxSAT. Quant als sistemes d'inferència, la tesi defineix un càlcul de tableaux complet per MaxSAT clausal, un càlcul de tableaux complet per MinSAT clausal i un càlcul de tableaux complet que permet resoldre tant MaxSAT com MinSAT. A més, la tesi proposa dos enfocaments diferents per a resoldre MaxSAT no clausal i MinSAT no clausal: en el primer enfocament, la tesi defineix transformacions de MaxSAT no clausal a MaxSAT clausal que preserven el cost. Aquestes transformacions s'estenen després per a definir transformacions de MinSAT no clausal a MinSAT clausal. En el segon enfocament, la tesi defineix un càlcul de tableaux per MaxSAT no clausal i demostra la seva consistència i completitud. També descriu com el càlcul de tableaux per MaxSAT no clausal es pot utilitzar per resoldre MinSAT no clausal. Pel que fa a les noves aplicacions de MaxSAT, la tesi defineix codificacions MaxSAT pel problema de composició d'equips en una aula, les avalua empíricament i demostra que aquest problema és NP-dur. Els coneixements adquirits són útils per resoldre altres problemes d'optimització mitjançant la seva reducció a MaxSAT. En particular, la tesi mostra com resoldre problemes de formació d'equips més complexos, utilitzant el model de composició d'equips sinèrgics com a cas d'estudi.

[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.