Felip Manyà

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.