Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

M7_chemical_SAT_solver.ipynb 11.4 KB
Newer Older
1
2
3
4
5
6
7
8
{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# M7 Chemical SAT Solver\n",
    "\n",
FAGES Francois's avatar
FAGES Francois committed
9
10
    "* Deciding the satisfiability of a Boolean formula in conjunctive normal form is NP-complete\n",
    "* How can we program a chemical SAT solver ? \n",
11
    "\n",
FAGES Francois's avatar
FAGES Francois committed
12
    "F. Fages, S. Soliman, Apr. 2020"
13
14
   ]
  },
FAGES Francois's avatar
M7sat    
FAGES Francois committed
15
16
17
18
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
FAGES Francois's avatar
FAGES Francois committed
19
    "# \"Generate and Test\" Algorithm with Stochastic CRN\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
20
21
    "\n",
    "A stochastic CRN can be used to enumerate random Boolean values for a variable"
22
23
24
25
   ]
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
26
   "execution_count": null,
27
28
29
   "metadata": {},
   "outputs": [],
   "source": [
FAGES Francois's avatar
FAGES Francois committed
30
    "parameter(k=1)."
31
32
33
34
   ]
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
35
   "execution_count": null,
36
37
38
   "metadata": {},
   "outputs": [],
   "source": [
FAGES Francois's avatar
FAGES Francois committed
39
    "MA(k) for _/a => a. % reactions with inhibitors cannot fire in presence of the inhibitor, here a"
40
41
42
43
   ]
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
44
   "execution_count": null,
45
46
47
   "metadata": {},
   "outputs": [],
   "source": [
FAGES Francois's avatar
FAGES Francois committed
48
    "MA(k) for a => _."
49
50
51
52
   ]
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
53
   "execution_count": null,
54
55
56
   "metadata": {},
   "outputs": [],
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
57
    "option(method:spn, stochastic_conversion:1)."
58
59
   ]
  },
FAGES Francois's avatar
M7sat    
FAGES Francois committed
60
61
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
62
   "execution_count": null,
FAGES Francois's avatar
M7sat    
FAGES Francois committed
63
   "metadata": {},
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
64
   "outputs": [],
65
66
67
68
69
70
   "source": [
    "numerical_simulation.\n",
    "plot."
   ]
  },
  {
FAGES Francois's avatar
FAGES Francois committed
71
   "cell_type": "markdown",
72
   "metadata": {},
FAGES Francois's avatar
M7sat    
FAGES Francois committed
73
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
74
75
76
    "## 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."
FAGES Francois's avatar
M7sat    
FAGES Francois committed
77
   ]
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
FAGES Francois's avatar
FAGES Francois committed
93
94
95
96
97
98
99
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
100
  {
FAGES Francois's avatar
M7sat    
FAGES Francois committed
101
   "cell_type": "markdown",
102
   "metadata": {},
FAGES Francois's avatar
M7sat    
FAGES Francois committed
103
   "source": [
FAGES Francois's avatar
FAGES Francois committed
104
    "## Question 2) Write a CRN to find values satisfying the formula (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
105
106
    "\n",
    "Use an event to stop the simulation when the formula is satisfied"
FAGES Francois's avatar
M7sat    
FAGES Francois committed
107
   ]
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
  },
  {
   "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": []
  },
  {
FAGES Francois's avatar
M7sat    
FAGES Francois committed
131
   "cell_type": "markdown",
132
   "metadata": {},
FAGES Francois's avatar
M7sat    
FAGES Francois committed
133
   "source": [
FAGES Francois's avatar
FAGES Francois committed
134
135
    "# 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"
FAGES Francois's avatar
M7sat    
FAGES Francois committed
136
   ]
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
  },
  {
   "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": []
  },
FAGES Francois's avatar
M7sat    
FAGES Francois committed
159
160
161
162
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
    "## 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": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
180
181
182
183
184
185
186
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
187
188
189
190
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
191
    "## Question 5) About the phase transition threshold in 3-SAT\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
192
193
    "\n",
    "As seen in the class\n",
FAGES Francois's avatar
FAGES Francois committed
194
195
196
197
    "* 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",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
198
199
200
    "* the hard instances are around the density threshold \n",
    "\n",
    "Can we observe that phenomenon with our CRN? Why?"
FAGES Francois's avatar
FAGES Francois committed
201
202
203
204
205
206
207
208
209
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
210
211
212
213
214
215
216
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
217
218
219
220
221
222
223
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
FAGES Francois's avatar
FAGES Francois committed
224
225
226
227
228
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Guided Search Algorithm by Continuous CRN\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
229
230
231
232
233
234
235
    "\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",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
236
    "$$E = \\sum_{1\\leq j\\leq M}K_j^2$$\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
237
238
239
240
241
242
243
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
244
    "## Question 6) Write $K_j$\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
245
    "\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
246
    "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",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
247
    "\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
248
    "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."
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
265
266
267
268
269
270
271
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
272
273
274
275
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
276
    "## Question 7) Obtain $dx_i/dt$\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
    "\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": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
295
296
297
298
299
300
301
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
302
303
304
305
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
306
    "## Question 8) Implement on the above example (x⋁¬y)⋀(y⋁¬z)⋀(z⋁¬x)\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
307
308
309
310
311
    "\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",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
312
    "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!]"
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
313
314
315
316
   ]
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
317
   "execution_count": null,
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
318
   "metadata": {},
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
319
320
   "outputs": [],
   "source": []
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
321
322
323
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
324
   "execution_count": null,
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
325
   "metadata": {},
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
326
327
   "outputs": [],
   "source": []
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
328
329
330
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
331
   "execution_count": null,
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
332
   "metadata": {},
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
333
   "outputs": [],
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
334
335
336
337
338
339
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
340
    "## Question 9) Improving the search\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
341
    "\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
342
    "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",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
343
344
    "These are new variables that will have an exponential increase proportional to $K_j$.\n",
    "\n",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
345
    "Add the 3 new variables and their ODEs with `add_ode`, change also the existing model accordingly.\n",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
346
    "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?"
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
347
348
   ]
  },
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
367
    "## Question 10) Complexity\n",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
368
369
    "\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?"
370
371
372
373
374
375
376
377
378
379
380
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
381
   "execution_count": null,
382
383
   "metadata": {},
   "outputs": [],
SOLIMAN Sylvain's avatar
prep M7    
SOLIMAN Sylvain committed
384
   "source": []
385
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
386
387
388
389
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
    "## 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",
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
    "\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": []
  },
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
  {
   "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": []
  },
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
  {
   "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
}