Studying the behaviour of dynamic biological systems is made by model checking;
this method generates scenarios based on the constraints defined in a model.
A scenario or a trajectory (i.e. a sequence of states of biomolecules),
can be described with the help of propositional logic formulas.
A SAT solver allows us to analyse constraints from models with **several thousands of places and transitions**.
It is used to either give a satisfiability answer, or generate a set of initial activation states
for the boundaries (frontier places) of the system.
Cadbiom uses the free and open source CryptoMinisat solver which happens to be a winner
of the 2010 and 2015 SAT Race competitions [SAT-Race2015]_.
Cadbiom has benefited from a major refactoring over the years. Some particularly costly functions in calculation time
have been written in C. An architecture implementing multiprocessing technology has been integrated into
the command line module to take advantage of the computing power of modern computers and distributed
computing infrastructures.
Moreover, an increased computing capacity has been achieved thanks to last versions of CryptoMinisat.
We can thus compare the performance of the old Cadbiom versions with the new one in terms
of the number of solutions obtained per unit of time.
..
import pandas as pd
df = pd.DataFrame({"Years of development and versions":["2016\nalpha", "2017\nv0.1.7", "2019\nv0.2", "2020 1st quarter\n(dev branch)"], "Solutions per hour":[0.33, 48, 180, 633]})
ax = df.plot.bar(
x="Years of development and versions",
y="Solutions per hour",
# title="Improved performance over the development years (log scale for y axis)",