Phylogenetic incongruence through the lens of Monadic Second Order logic

TL;DR

This paper demonstrates the potential of Monadic Second Order logic (MSOL) to efficiently analyze phylogenetic tree incongruence by providing fixed parameter tractability proofs for various measures, leveraging graph treewidth bounds.

Contribution

The paper introduces MSOL-based methods for proving fixed parameter tractability of phylogenetic incongruence measures, highlighting MSOL's potential in phylogenetics research.

Findings

MSOL can be used to prove fixed parameter tractability of incongruence measures.

Agreement forests imply bounded treewidth of display graphs.

New MSOL primitives tailored for phylogenetics are proposed.

Abstract

Within the field 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 fixed parameter tractable algorithms. In this article we use Monadic Second Order logic (MSOL) to give alternative, compact proofs of fixed parameter tractability for several well-known incongruency 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. A crucial component of this work is the observation that many of these 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. We give a variety of different MSOL formulations. Some are based on explicitly encoding agreement forests, while some only use them implicitly to generate the treewidth bound. Our formulations introduce a number of "phylogenetics MSOL primitives" which will hopefully be of use to other researchers.