Analysis of some graph properties of the current model.
').
pathway(Object1,Object2):-
biocham_command,
type(Object1,object),
type(Object2,object),
doc('Gives one reaction pathway from \\argument{Object1} to \\argument{Object2} if one exists in the directed reaction graph of the current model (for more complex queries, see next section on Computation Tree Logic model-checking).'),
doc('Lists the molecular species that are neither a non-strict-catalyst reaction product nor the target of an influence rule in the curent model.Strict catalysts, i.e. catalysts with same stoichiometry in left-hand and right side of reactions, are allowed as inputs.'),
input_species(Molecules),
writeln(Molecules).
list_source_species:-
biocham_command,
doc('Lists the molecular species that are neither a reaction product nor the target of an influence rule in the curent model.'),
source_species(Molecules),
writeln(Molecules).
list_sink_species:-
biocham_command,
doc('Lists the molecular species that are neither a reactant nor a positive source of an influence rule in the curent model.'),
sink_species(Molecules),
writeln(Molecules).
%API
:-devdoc('Prolog lists of graph sources and sinks.').
"* Deciding the satisfiability of a Boolean formula in conjunctive normal form is NP-complete\n",
"* How can we program a chemical SAT solver ? \n",
"\n",
"F. Fages, S. Soliman, Apr. 2020"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# \"Generate and Test\" Algorithm with Stochastic CRN\n",
"\n",
"A stochastic CRN can be used to enumerate random Boolean values for a variable"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"parameter(k=1)."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"MA(k) for _/a => a. % reactions with inhibitors cannot fire in presence of the inhibitor, here a"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"MA(k) for a => _."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"option(method:spn, stochastic_conversion:1)."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"numerical_simulation.\n",
"plot."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 1) Write a random generator of Boolean values for a vector of 3 variables a, b, c\n",
"\n",
"Write a stochastic CRN randomly sampling the Boolean values of a, b and c."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 2) Write a CRN to find values satisfying the formula (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)\n",
"\n",
"Use an event to stop the simulation when the formula is satisfied"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Guided Search Algorithm with Stochastic CRN\n",
"## Question 3) Improve your CRN to decrease the probability of moves of the variables that belong to satisfied clauses"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 4) Any idea to decide unsatisfiability?"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 5) About the phase transition threshold in 3-SAT\n",
"\n",
"As seen in the class\n",
"* the density of a SAT instance is the ratio of the number of clauses divided by the number of variables\n",
"* a phase transition phenomenon is an asymptotic result showing the existence of a density threshold\n",
"* under the threshold the instances are almost surely satisfiable\n",
"* above the threshold the instances are almost surely unsatisfiable\n",
"* the hard instances are around the density threshold \n",
"\n",
"Can we observe that phenomenon with our CRN? Why?"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Guided Search Algorithm by Continuous CRN\n",
"\n",
"We can see the SAT solving problem as a (continous) global optimization problem and try to solve it by gradient descent.\n",
"\n",
"The idea is to find an energy function $E$ that is minimal when all clauses are satisfied, and then to simply enforce that $$\\frac{dx}{dt} = -\\frac{\\partial E}{\\partial x}$$\n",
"\n",
"For a SAT problem involving variables $x_i\\in [0, 1], 1\\leq i\\leq N$ and clauses $C_j, 1\\leq j\\leq M$ (with $C_{ji} = 1$ if $x_i$ appears positively in $C_j$, $C_{ji} = -1$ if $x_i$ appears negatively, and $0$ otherwise), we will define our energy function as a sum of squares of sub-energies for each clause.\n",
"\n",
"$$E = \\sum_{1\\leq j\\leq M}K_j^2$$\n",
"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 6) Write $K_j$\n",
"\n",
"Define (formally) $K_j$ as a function of the $C_{ji}$ and of the $x_i$, such that $K_j = 0$ iff clause $j$ is satisfied, and $K_j = 2^N$ if all $N$ variables appear in clause $j$ and are currently at the _wrong_ value.\n",
"\n",
"One might want to define $s_i\\in[-1, 1]$ as a function of $x_i\\in[0, 1]$ and then $K_j$ as a function of the $s_i$ for ease of writing."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 7) Obtain $dx_i/dt$\n",
"\n",
"Obtain the formal expression for $\\displaystyle\\frac{dx}{dt}$ (if you have used $s_i$ just note that $\\frac{\\partial E}{\\partial x}=\\frac{\\partial E}{\\partial x}\\frac{\\partial s}{\\partial x}$)."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 8) Implement on the above example (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)\n",
"\n",
"Using the commands:\n",
"`new_ode_system`, `init` (to set $x_1, x_2$ and $x_3$ initial state to 0.5), `ode_parameter` (to set the $c_ji$ corresponding to our 3 clauses), `ode_function` (for the $k_j$ and $s_i$) and `add_ode` (to add the above $dx_i/dt$)\n",
"\n",
"Run a numerical simulation and plot the $x_i$ to see the result.\n",
"Experiment with different initial states, and variants of the problem (changing only the $c_{ji}$), what do you observe? [please leave all results and remarks *in* the notebook!]"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Question 9) Improving the search\n",
"\n",
"To avoid getting stuck in some local minima, we can add *Lagrange multipliers* $a_j, 1\\leq j\\leq M$ so that the energy becomes $$E = \\sum_{1\\leq j\\leq M}a_j K_j^2$$\n",
"These are new variables that will have an exponential increase proportional to $K_j$.\n",
"\n",
"Add the 3 new variables and their ODEs with `add_ode`, change also the existing model accordingly.\n",
"Do you notice any difference? What can you say about the steadiness and stability of the initial state with all $x_i$ equal to 0.5?"
