Abstract
Phylogenetic analysis is a widely used technique, for example in biology and biomedical sciences. The construction of phylogenies can be computationally hard. A commonly used solution for construction of phylogenies is to start from a set of biological species and relations among those species. This work addresses the case where the relations among species are specified as quartet topologies. Moreover, the problem to be solved consists of computing a phylogeny that satisfies the maximum number of quartet topologies. This is referred to as the Maximum Quartet Consistency (MQC) problem, and represents an NP-hard optimization problem. MQC has been solved both heuristically and exactly. Exact solutions for MQC include those based on Constraint Programming, Answer Set Programming, Pseudo-Boolean Optimization (PBO), and Satisfiability Modulo Theories (SMT). This paper provides a comprehensive overview of the use of PBO and SMT for solving MQC, and builds on recent work in this area. Moreover, the paper provides new insights on how to use SMT for solving optimization problems, by focusing on the concrete case of MQC. The solutions based on PBO and SMT were experimentally compared with other exact solutions. The results 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.