{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# M7 Chemical SAT Solver\n", "\n", "* 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?" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Question 10) Complexity\n", "\n", "The authors of the paper observe on random SAT instances that the $x_i$ trajectories have a polynomial length, however they do **not** conclude that the algorithm is polynomial. What have you observed that might not remain polynomial?" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Question 11) Phase transition\n", "\n", "Do you think one can observe the phase-transition phenomenon?\n", "In other words are _hard instances_ the ones with an average clause density? why?" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Question 12) Biochemical interpretation\n", "\n", "What variables are always positive? What do you think about the associated chemical reaction network? [use biocham commands to obtain it!]" ] }, { "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 13) Genericity?\n", "\n", "How generic is the method we use here for our continuous solver?" ] }, { "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": [] } ], "metadata": { "kernelspec": { "display_name": "Biocham", "language": "", "name": "biocham" }, "language_info": { "codemirror_mode": "biocham", "file_extension": ".bc", "mimetype": "text/plain", "name": "biocham", "pygments_lexer": "prolog" } }, "nbformat": 4, "nbformat_minor": 4 }