Skip to content

Research at St Andrews

An integrated approach to a combinatorial optimisation problem

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We take inspiration from a problem from the healthcare domain, where patients with several chronic conditions follow different guidelines designed for the individual conditions, and where the aim is to find the best treatment plan for a patient that avoids adverse drug reactions, respects patient’s preferences and prioritises drug efficacy. Each chronic condition guideline can be abstractly described by a directed graph, where each node indicates a treatment step (e.g., a choice in medications or resources) and has a certain duration. The search for the best treatment path is seen as a combinatorial optimisation problem and we show how to select a path across the graphs constrained by a notion of resource compatibility. This notion takes into account interactions between any finite number of resources, and makes it possible to express non-monotonic interactions. Our formalisation also introduces a discrete temporal metric, so as to consider only simultaneous nodes in the optimisation process. We express the formal problem as an SMT problem and provide a correctness proof of the SMT code by exploiting the interplay between SMT solvers and the proof assistant Isabelle/HOL. The problem we consider combines aspects of optimal graph execution and resource allocation, showing how an SMT solver can be an alternative to other approaches which are well-researched in the corresponding domains.


Original languageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings
EditorsWolfgang Ahrendt, Silvia Lizeth Tapia Tarifa
Place of PublicationCham
Number of pages19
ISBN (Electronic)9783030349684
ISBN (Print)9783030349677
Publication statusPublished - 2019
Event15th International Conference on integrated Formal Methods (iFM 2019) -, Bergen, Norway
Duration: 2 Dec 20196 Dec 2019
Conference number: 15

Publication series

NameLecture Notes in Computer Science (Programming and Software Engineering)
ISSN (Print)0302-9743


Conference15th International Conference on integrated Formal Methods (iFM 2019)
Abbreviated titleiFM 2019

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. A framework for automated conflict detection and resolution in medical guidelines

    Bowles, J., Caminati, M. B., Cha, S. & Mendoza, J., 1 Aug 2019, In : Science of Computer Programming. 182, p. 42-63 22 p.

    Research output: Contribution to journalArticle

  2. Balancing prescriptions with constraint solvers

    Bowles, J. K. F. & Caminati, M. B., 2019, Automated Reasoning for Systems Biology and Medicine. Liò, P. & Zuliani, P. (eds.). Cham: Springer, p. 243-267 25 p. (Computational Biology; vol. 30).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  3. Formalization and Automation of Quality Assurance Processes in Radiation Oncology

    Munbodh, R., Zaveri, H., Caminati, M. & Bowles, J., 31 Jul 2018, In : Medical physics. 45, 6, p. E274-E274 1 p.

    Research output: Contribution to journalAbstract

  4. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S., 7 Feb 2018, 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 261446208