Authors: Bhattacharya Arnab, Kuppusamy Lakshmanan, Shukla Ankit, Srivas Mandayam, Thattai Mukund
The inside of a living cell is split into several distinct locations called organelles. Small transporters called vesicles move cargo between these organelles, just as trucks move cargo between warehouses in a logistics network. We are interested in the global mathematical features of the resulting network, where each organelle is considered as a node, and each vesicle transport route is considered as a directed edge. The whole structure can be represented as graph. We have shown that the connectedness of a vesicle graph is an informative feature. Two - connectedness is necessary and sufficient for mass balance. Three - connectedness is sufficient (but not necessary) for a system driven by molecular recognition. Four - connectedness is necessary and sufficient for the famous Rothman-Schekman-Sudhof model of vesicle traffic. We have used boolean satisfiability, SAT as a framework via a model-checking tool (CBMC) to verify these properties and shown further connections between molecular rules and graph-theoretic properties. Scalability of SAT solvers and model checkers that use has always been an issue, we have shown by exploiting structure of formulas it is possible to scale the SAT model checkers to reasonably complex biological systems. . . .