22 May 2014 Solving a discrete model of the lac operon using Z3
Author Affiliations +
A discrete model for the Lcac Operon is solved using the SMT-solver Z3. Traditionally the Lac Operon is formulated in a continuous math model. This model is a system of ordinary differential equations. Here, it was considerated as a discrete model, based on a Boolean red. The biological problem of Lac Operon is enunciated as a problem of Boolean satisfiability, and it is solved using an STM-solver named Z3. Z3 is a powerful solver that allows understanding the basic dynamic of the Lac Operon in an easier and more efficient way. The multi-stability of the Lac Operon can be easily computed with Z3. The code that solves the Boolean red can be written in Python language or SMT-Lib language. Both languages were used in local version of the program as online version of Z3. For future investigations it is proposed to solve the Boolean red of Lac Operon using others SMT-solvers as cvc4, alt-ergo, mathsat and yices.
© (2014) COPYRIGHT Society of Photo-Optical Instrumentation Engineers (SPIE). Downloading of the abstract is permitted for personal use only.
Natalia A. Gutierrez, Natalia A. Gutierrez, } "Solving a discrete model of the lac operon using Z3", Proc. SPIE 9118, Independent Component Analyses, Compressive Sampling, Wavelets, Neural Net, Biosystems, and Nanoengineering XII, 911814 (22 May 2014); doi: 10.1117/12.2049755; https://doi.org/10.1117/12.2049755

Back to Top