Phylogenetic incongruence through the lens of monadic second order logic

Abstract

Within the field of phylogenetics there is growing interest in measures for summarising the dissimilarity, or incongruence, of two or more phylo- genetic trees. Many of these measures are NP-hard to compute and this has stimulated a considerable volume of research into fixxed parameter tractable algorithms. In this article we use Monadic Second Order logic (MSOL) to give alternative, compact proofs of fixed parameter tractabil- ity for several well-known incongruence measures. In doing so we wish to demonstrate the considerable potential of MSOL - machinery still largely unknown outside the algorithmic graph theory community - within phylo- genetics, introducing a number of \phylogenetics MSOL primitives'' which will hopefully be of use to other researchers. A crucial component of this work is the observation that many incongruence measures, when bounded, imply the existence of an agreement forest of bounded size, which in turn implies that an auxiliary graph structure, the display graph, has bounded treewidth. It is this bound on treewidth that makes the machinery of MSOL available for proving fixed parameter tractability. Due to the fact that all our formulations are of constant length, and are articulated in the restricted variant of MSOL known as MSO1, we actually obtain the stronger result that all these incongruence measures are fixed parameter tractable purely in the treewidth (in fact, if an appropriate decomposition is given: the cliquewidth) of the display graph. To highlight the potential importance of this, we re-analyse a well-known dataset and show that the treewidth of the display graph grows more slowly than the main incon- gruence measures analysed in this article1.