Commit e9e7a039 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain
Browse files

M7 again

parent c5a71dc0
%% Cell type:markdown id: tags:
# M7 Chemical SAT Solver
* Deciding the satisfiability of a Boolean formula in conjunctive normal form is NP-complete
* How can we program a chemical SAT solver ?
F. Fages, S. Soliman, Apr. 2020
%% Cell type:markdown id: tags:
# "Generate and Test" Algorithm with Stochastic CRN
* A stochastic CRN can be used to enumerate random Boolean values for a variable
%% Cell type:code id: tags:
```
parameter(k=1).
```
%% Cell type:code id: tags:
```
MA(k) for _/a => a. % reactions with inhibitors cannot fire in presence of the inhibitor, here a
```
%% Cell type:code id: tags:
```
MA(k) for a => _.
```
%% Cell type:code id: tags:
```
option(method:spn, stochastic_conversion:1).
```
%% Cell type:code id: tags:
```
numerical_simulation.
plot.
```
%% Cell type:markdown id: tags:
## Question 1) Write a random generator of Boolean values for a vector of 3 variables a, b, c
Write a stochastic CRN randomly sampling the Boolean values of a, b and c.
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 2) Write a CRN to find values satisfying the formula (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)
* Use an event to stop the simulation when the formula is satisfied
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
# Guided Search Algorithm with Stochastic CRN
## Question 3) Improve your CRN to decrease the probability of moves of the variables that belong to satisfied clauses
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 4) Determine the phase transition threshold in 3-SAT
## Question 4) Any idea to decide unsatisfiability?
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 5) Determine the phase transition threshold in 3-SAT
As seen in the class
* the density of a SAT instance is the ratio of the number of clauses divided by the number of variables
* a phase transition phenomenon is an asymptotic result showing the existence of a density threshold
* under the threshold the instances are almost surely satisfiable
* above the threshold the instances are almost surely unsatisfiable
* the hard instances are around the density threshold
Can we observe that phenomenon with our CRN? Why?
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
# Guided Search Algorithm by Continuous CRN
We can see the SAT solving problem as a (continous) global optimization problem and try to solve it by gradient descent.
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}$$
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.
$$E = \sum_{1\leq j\leq M}K_j^2$$
%% Cell type:markdown id: tags:
## Question 5) Write $K_j$
## Question 6) Write $K_j$
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.
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 id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 6) Obtain $dx_i/dt$
## Question 7) Obtain $dx_i/dt$
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 id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 7) Implement on the above example (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)
## Question 8) Implement on the above example (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)
Using the commands:
`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$)
Run a numerical simulation and plot the $x_i$ to see the result.
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 id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 8) Improving the search
## Question 9) Improving the search
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$$
These are new variables that will have an exponential increase proportional to $K_j$.
Add the 3 new variables and their ODEs with `add_ode`, change also the existing model accordingly.
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 id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 9) Complexity
## Question 10) Complexity
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 id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 10) Biochemical interpretation
## Question 11) Phase transition
Do you think one can observe the phase-transition phenomenon?
In other words are _hard instances_ the ones with an average clause density? why?
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 12) Biochemical interpretation
What variables are always positive? What do you think about the associated chemical reaction network? [use biocham commands to obtain it!]
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question 13) Genericity?
How generic is the method we use here for our continuous solver?
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
%% Cell type:code id: tags:
```
```
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment