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

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