Statut : Actif
- Url pour s'y attacher : http://sat.isa.ru/pdsat/
- L’alliance Francophone : http://sat.isa.ru/pdsat/team_display.php?teamid=4
- Classement mondial de L'AF : http://fr.boincstats.com/stats/team_stats.php?pr=sat&st=0
- Temps de calcul et points de sauvegarde : http://wuprop.boinc-af.org/results.html
- Avancement des sous-projets : http://sat.isa.ru/pdsat/research_progress.php
- État du Serveur : http://at.isa.ru/pdsat/server_status.php
- Affiliation : Académie des sciences de Russie - Russie
Résumé :
Le projet vise à résoudre divers problèmes combinatoires. Il y a beaucoup de problèmes pratiques importants pour lesquels l'existence d'algorithmes (polynomiales) efficaces pour leurs résolutions n'a pas été prouvée. La plupart de ces problèmes sont Np-complets. Cela signifie qu'en se basant sur des hypothèses raisonnables (mais non prouvées), ces problèmes ne peuvent pas être résolus en temps polynomial. Cependant, de nombreux de leurs cas particuliers se présentent dans les applications pratiques: divers problèmes d'optimisation discrète (par exemple, la planification de la production) et les problèmes de vérification des dispositifs discrets (se présentant, par exemple, dans la conception de circuits et la démonstration de l’exactitude du programme). Par conséquent, il est très important de disposer de méthodes permettant leurs résolutions qui n'ont pas une complexité polynomiale, mais qui sont efficaces dans la pratique. De telles méthodes peuvent faire face aux nombreux cas particuliers des problèmes Np-complets de grandes dimensions. L'un des plus simple dans sa base, et donc le plus efficace en terme d'implémentations logicielles est l'approche SAT. Cette approche est basée sur la réductibilité du problème considéré comme original vers un problème SAT, qui est le problème de la satisfaisabilité de la forme normale conjonctive (CNF). Les problèmes SAT admettent une forme très naturelle de parallélisme, ce qui permet l'utilisation d'un environnement de calcul distribué. En réalité, la réductibilité vers SAT peut être menée de manière efficace (en fait, elle résulte de la célèbre forme du théorème de Cook-Levin). Pour plus de détails sur les problèmes SAT, voir ici.
La cryptanalyse ( déchiffrer un message ayant été chiffré sans posséder la clé de chiffrement) fournit une classe très intéressante de problèmes pouvant être résolus par une approche SAT. Il convient de noter que nous ne résolvons pas les problèmes de déchiffrement avec des données privées. Tous les tests à l'étude sont générés aléatoirement. À cet égard, notre travail est d'étudier la stabilité des systèmes de cryptage modernes. C'est pourquoi, dans un avenir proche, nous prévoyons de résoudre avec le projet SAT@home des problèmes de recherche de séquences d'initialisation pour A5/1 (algorithme de chiffrement) qui ne sont pas couverts actuellement.
En outre, nous prévoyons d'utiliser SAT@home pour étudier d'autres fonctions de cryptographie et de résoudre certains problèmes "extrêmement complexes" d'optimisation discrète, en particulier le problème d'affectation quadratique (QAP), et certains problèmes de bio-informatique (analyse de modèles discrets de réseaux de gènes).
Applications CPU :
Disponible pour Windows (32bits) et Linux (32 et 64bits).
*Des WUs 32bits seront envoyées aux machines 64bits sous Windows.