Abstract
Elementary flux modes (EFMs) are commonly accepted tools for metabolic network analysis under steady state conditions. They can be defined as the smallest sub-networks enabling the metabolic system to operate in steady state with all irreversible reactions proceeding in the appropriate direction. However, when networks are complex, the number of EFMs quickly leads to a combinatorial explosion, preventing from drawing even simple conclusions from their analysis. Since the concept of EFMs analysis was introduced in 1994, there has been an important and ongoing effort to develop more efficient algorithms. However, these methods share a common bottleneck: they enumerate all the EFMs which make the computation impossible when the metabolic network is large and only few works try to search only EFMs with specific properties. As we will show in this paper, enumerating all the EFMs is not necessary in many cases and it is possible to directly query the network instead with an appropriate tool. For ensuring a good query time, we will rely on a state of the art SAT solver, working on a propositional encoding of EFMs, and enriched with a simple SMT-like solver ensuring EFMs consistency with stoichiometric constraints. We illustrate our new framework by providing experimental evidences of almost immediate answer times on a non trivial metabolic network.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Audemard, G., Lagniez, J., Simon, L.: Just-in-time compilation of knowledge bases. In: 23rd International Joint Conference on Artificial Intelligence(IJCAI 2013), pp. 447–453 (August 2013)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: IJCAI (2009)
Ballerstein, K., von Kamp, A., Klamt, S., Haus, U.: Minimal cut sets in a metabolic network are elementary modes in a dual network. Bioinformatics 28(3), 381–387 (2012)
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere et al (eds.) [8], ch. 26, vol. 185, pp. 825–885 (February 2009)
Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient mus extraction. AI Communications 25(2), 97–116 (2012)
Biere, A.: Bounded Model Checking. In: Biere, et al. (eds.) [8] ch. 14, vol. 185, pp. 455–481 (2009)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds (1999)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009)
Bradley, A.R.: IC3 and beyond: Incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4–4. Springer, Heidelberg (2012)
Darwiche, A., Marquis, P.: A knowledge compilation map. J. of AI Research, 229–264 (2002)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. JACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM 7, 201–215 (1960)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. SAT, pp. 502–518. Springer, Heidelberg (2004)
Gagneur, J., Klamt, S.: Computation of elementary modes : a unifying framework and the new binary approach. BMC Bioinformatics 5(175) (2004)
Jevremovic, D., Trinh, C., Srienc, F., Sosa, C.P., Boley, D.: Parallelization of nullspace algorithm for the computation of metabolic pathways. Parallel Computing 37(6-7), 261–278 (2011)
Jol, S.J., Kümmel, A., Terzer, M., Stelling, J., Heinemann, M.: System-level insights into yeast metabolism by thermodynamic analysis of elementary flux modes. PLoS Computational Biology 8(3) (2012)
Jungreuthmayer, C., Ruckerbauer, D.E., Zanghellini, J.: Regefmtool: Speeding up elementary flux mode calculation using transcriptional regulatory rules in the form of three-state logic. Biosystems 113(1), 37–39 (2013)
Kaleta, C., De Figueiredo, L.F., Schuster, S.: Can the whole be less than the sum of its parts? pathway analysis in genome-scale metabolic networks using elementary flux patterns. Genome Research 19, 1872–1883 (2009)
Kautz, H., Selman, B.: Blackbox: A new approach to the application of theorem proving to problem solving. In: Working notes of the Workshop on Planning as Combinatorial Search, Held in Conjunction with AIPS 1998, pp. 58–60 (1998)
Klamt, S., Saez-Rodriguez, J., Gilles, E.: Structural and functional analysis of cellular networks with cellnetanalyzer. BMC Systems Biology 1(1), 2 (2007)
Klamt, S., Stelling, J.: Combinatorial complexity of pathway anaysis in metabolic networks. Mol. Bio. Rep. 29, 233–236 (2002)
Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: International Workshop on First-Order Theorem Proving (2009)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530–535 (2001)
Peres, S., Beurton-Aimar, M., Mazat, J.P.: Pathway classification of tca cycle. IEE Journal for Systems Biology 153(5), 369–371 (2006)
Peres, S., Vallée, F., Beurton-Aimar, M., Mazat, J.P.: Acom: a classification method for elementary flux modes based on motif finding. Biosystems 103(3), 410–419 (2011)
Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proc. SAT (2004)
Schuster, S., Dandekar, T., Fell, D.A.: Detection of elementary modes in biochemical networks : A promising tool for pathway analysis and metabolic engineering. Trends Biotechnol. 17, 53–60 (1999)
Schuster, S., Fell, D.A., Dandekar, T.: A general definition of metabolic pathways useful for systematic organization and analysis of complex metabolic networks. Nat. Biotechnol. 18, 326–332 (2000)
Schuster, S., Hilgetag, C.: On elementary flux modes in biochemical reaction systems at steady state. Journal of Biological Systems 2(2), 165–182 (1994)
Schwimmer, C., Lefebvre-Legendre, L., Rak, M., Devin, A., Slonimski, P., di Rago, J.P., Rigoulet, M.: Increasing mitochondrial substrate-level phosphorylation can rescue respiratory growth of an atp synthase-deficient yeast. J. Biol. Chem. 280(35), 30751–30759 (2005)
Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of ICCAD, pp. 220–227 (1996)
American Mathematical Society (ed.) Second DIMACS implementation challenge: cliques, coloring and satisfiability, vol. 26 (1996)
Soh, T., Inoue, K.: Identifying necessary reactions in metabolic pathways by minimal model generation. In: ECAI, pp. 277–282 (2010)
Soh, T., Inoue, K., Baba, T., Takada, T., Shiroishi, T.: Predicting gene knockout effects by minimal pathway enumeration. In: BIOTECHNO 2012 : The Fourth International Conference on Bioinformatics, Biocomputational Systems and Biotechnologies, pp. 11–19 (2012)
Stelling, J., Klamt, S., Bettenbrock, K., Schuster, S., Gilles, E.D.: Metabolic network structure determines key aspect of functionnality and regulation. Nature 420, 190–193 (2002)
Terzer, M., Stelling, J.: Large-scale computation of elementary flux modes with bit pattern trees. Bioinformatics 24(19), 2229–2235 (2008)
Tiwari, A., Talcott, C., Knapp, M., Lincoln, P., Laderoute, K.: Analyzing pathways using SAT-based approaches. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol. 4545, pp. 155–169. Springer, Heidelberg (2007)
von Kamp, A., Klamt, S.: Enumeration of smallest intervention strategies in genome-scale metabolic networks. PLoS Comput Biol 10(1), e1003378 (2014)
von Kamp, A., Schuster, S.: Metatool 5.0: Fast and flexible elementary modes analysis. Bioinformatics 22, 1930–1931 (2006)
Wieringa, S.: Incremental Satisfiability Solving and its Applications. PhD thesis, Aalto University (2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Peres, S., Morterol, M., Simon, L. (2014). SAT-Based Metabolics Pathways Analysis without Compilation. In: Mendes, P., Dada, J.O., Smallbone, K. (eds) Computational Methods in Systems Biology. CMSB 2014. Lecture Notes in Computer Science(), vol 8859. Springer, Cham. https://doi.org/10.1007/978-3-319-12982-2_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-12982-2_2
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12981-5
Online ISBN: 978-3-319-12982-2
eBook Packages: Computer ScienceComputer Science (R0)