SMT Solving for Vesicle Traffic Systems in Cells

TL;DR

This paper introduces SMT-based methods to analyze vesicle traffic networks in cells, enabling biologists to identify possible network configurations satisfying specific biophysical constraints.

Contribution

It presents novel SMT encodings for vesicle traffic properties and a tool that efficiently searches for networks meeting those biological constraints.

Findings

Successfully searches for biologically relevant network sizes

Demonstrates the effectiveness of SMT solvers in biological network analysis

Provides a new computational approach for studying cellular transport systems

Abstract

In biology, there are several questions that translate to combinatorial search. For example, vesicle traffic systems that move cargo within eukaryotic cells have been proposed to exhibit several graph properties such as three connectivity. These properties are consequences of underlying biophysical constraints. A natural question for biologists is: what are the possible networks for various combinations of those properties? In this paper, we present novel SMT based encodings of the properties over vesicle traffic systems and a tool that searches for the networks that satisfies the properties using SMT solvers. In our experiments, we show that our tool can search for networks of sizes that are considered to be relevant by biologists.