Phylogenetic incongruence through the lens of Monadic Second Order logic

Within the eld of phylogenetics there is growing interest in measures for summarising the dissimilarity, or incongruence, of two or more phylogenetic trees. Many of these measures are NP-hard to compute and this has stimulated a considerable volume of research into xed parameter tractable algorithms. In this article we use Monadic Second Order logic (MSOL) to give alternative, compact proofs of xed parameter tractability 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 phylogenetics, 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 xed 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 xed 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 incongruence measures analysed in this article.