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

More questions…

parent 0b389437
%% 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
%% 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:markdown id: tags:
## Question ) Any idea to decide unsatisfiability ? statistical test question ?
%% 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
* 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
%% Cell type:code id: tags:
```
```
%% Cell type:markdown id: tags:
## Question ) Evaluation on 2-SAT and Horn-SAT ?
%% 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$
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$
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)
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
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?
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
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
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:
```
```
......
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