Stage: Synthèse de réseaux booléens par résolution de problèmes de satisfiabilité avec quantificateurs

# Stage: Synthèse de réseaux booléens par résolution de problèmes de satisfiabilité avec quantificateurs  **Encadrant**: Loïc Paulevé - https://loicpauleve.name - [loic.pauleve@labri.fr](mailto:loic.pauleve@labri.fr) **Lieu**: LaBRI, Université de Bordeaux **Mots clés**: SAT, logique, systèmes dynamiques ### Contexte et objectifs Un réseau d'automates booléens est constitué d'un ensemble de variables binaires et associe à chacune d'elle une règle logique pour calculer sa valeur en fonction des autres variables. Par exemple, le réseau $$\begin{align*} f_a(a,b) &= \lnot a \land \lnot b\\ f_b(a,b) &= a \lor b \end{align*}$$ définit deux variables, $a$ et $b$ et leur règle pour changer d'état. Associé à un *mode de mise à jour* (sémantique), il décrit un système dynamique avec les transitions possibles entre les configurations du réseau. Par exemple, le mode synchrone appliquera itérativement $f$ sur la configuration initiale, alors que le mode asynchrone considère toutes les combinaisons de mise à jour d'automates possibles. La synthèse de réseaux booléens consiste à trouver automatiquement une définition de $f$ dont l'interprétation dynamique vérifie un ensemble de propriétés voulues. Ces propriétés font généralement référence à l'existence ou absence de trajectoires (*reachability*), et sur les configurations limites du réseau (*attractors*). L'objectif du stage est d'étudier différents encodages du problème de synthèse de réseaux booléens, en particulier en tant que problèmes SAT et QBF, et l'efficacité de leur résolution. Les propriétés considérées nécessiteront entre 1 (SAT) et 3 niveaux de quantification (2-QBF et 3-QBF) de formules de logique propositionnelle. ### Liens - T Chatain et al., "Most Permissive Semantics of Boolean Networks", http://arxiv.org/abs/1808.10240 - S Chevalier et al., "Synthesis of Boolean Networks from Biological Dynamical Constraints using Answer-Set Programming", IEEE ICTAI 2019 https://hal.archives-ouvertes.fr/hal-02276921/file/ictai19.pdf - https://github.com/bnediction/bonesis