Common chronic conditions are routinely treated following standardised procedures known as . For patients suffering from two or more chronic conditions, known as multimorbidity, several guidelines have to be applied simultaneously, which may lead to severe adverse effects when the combined recommendations and prescribed medications are inconsistent or incomplete. This paper presents an automated formal framework to detect, highlight and resolve conflicts in the treatments used for patients with multimorbidities focusing on medications. The presented extended framework has a front-end which takes guidelines captured in a standard modelling language and returns the visualisation of the detected conflicts as well as suggested alternative treatments. Internally, the guidelines are transformed into formal models capturing the possible unfoldings of the guidelines. The back-end takes the formal models associated with multiple guidelines and checks their correctness with a theorem prover, and inherent inconsistencies with a constraint solver. Key to our approach is the use of an optimising constraint solver which enables us to search for the best solution that resolves/minimises conflicts according to medication efficacy and the degree of severity in case of harmful combinations, also taking into account their temporal overlapping. The approach is illustrated throughout with a real medical example.

We compare different algorithms for computing eigenvalues and eigenvectors of a symmetric band matrix across a wide range of synthetic test problems. Of particular interest is a comparison of state-of-the-art tridiagonalization-based methods as implemented in Lapack or Plasma on the one hand, and the block divide-and-conquer (BD&C) algorithm as well as the block twisted factorization (BTF) method on the other hand. The BD&C algorithm does not require tridiagonalization of the original band matrix at all, and the current version of the BTF method tridiagonalizes the original band matrix only for computing the eigenvalues. Avoiding the tridiagonalization process sidesteps the cost of backtransformation of the eigenvectors. Beyond that, we discovered another disadvantage of the backtransformation process for band matrices: In several scenarios, a lot of gradual underflow is observed in the (optional) accumulation of the transformation matrix and in the (obligatory) backtransformation step. According to the IEEE 754 standard for floating-point arithmetic, this implies many operations with subnormal (denormalized) numbers, which causes severe slowdowns compared to the other algorithms without backtransformation of the eigenvectors. We illustrate that in these cases the performance of existing methods from Lapack and Plasma reaches a competitive level only if subnormal numbers are disabled (and thus the IEEE standard is violated). Overall, our performance studies illustrate that if the problem size is large enough relative to the bandwidth, BD&C tends to achieve the highest performance of all methods if the spectrum to be computed is clustered. For test problems with well separated eigenvalues, the BTF method tends to become the fastest algorithm with growing problem size.