António José dos Reis Morgado
Combinatorial Optimization problems occur in different fields of science, including Artificial Intelligence, BioInformatics, Electronic Design Automation, Operations Research, Applied Formal Methods, among others. For example in BioInformatics, and in particular in the field of Phylogenetic analysis, the problem of computing an optimal phylogeny that satisfies the maximum number of a given set quartet topologies is the problem called the Maximum Quartet Consistency (MQC) problem, and represents an NP-hard optimization problem. In the field of Operations Research, optimizing the arrangement of a set of two-dimensional rectangles in an area with fixed width and variable height, such that the area occupied is minimal, is referred to as the Two-Dimensional Strip Packing problem (2SPP). 2SPP is a NP-hard optimization problem. Propositional Satisfiability (SAT) is a well-known NP-complete problem. Despite SAT not being an optimization problem, the ability of current state of the art SAT solvers to handle large search spaces has inspired the creation of extensions of the SAT problem which optimize some cost function. For example, Pseudo-Boolean Optimization (PBO), Maximum Satisfiability (Max SAT) or more recently Satisfiability Modulo Theories (SMT). Solutions to MQC and 2SPP include both heuristic and exact approaches. This thesis provides a comprehensive overview of the use SAT technology for solving both MQC and 2SPP, and builds on recent work in this areas. Moreover, the thesis provides new insights on how to use SMT for solving optimization problems, by focusing on the concrete cases of MQC and 2SPP. The solutions based on iterative SAT, PBO, and SMT were experimentally compared with other existing exact solutions. The results for MQC show that for instances with small percentage of quartet errors, the models based on SMT can be competitive, whereas for instances with higher number of quartet errors the PBO models are more efficient. On the other hand for 2SPP, the results show that solutions based on iteration of SAT instances are more effective.