(http://sat.isa.ru/pdsat/img/logo.png) (http://sat.isa.ru/pdsat/)
Infos Utiles :
- Statut : Projet terminer
- Url pour s'y attacher : http://sat.isa.ru/pdsat/
- L’alliance Francophone : http://sat.isa.ru/pdsat/team_display.php?teamid=4
- Articles sur le site de L'AF : http://boinc-af.org/projets-mathematiques/1391-sat-home.html (http://boinc-af.org/projets-mathematiques/1391-sat-home.html)
- 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 (http://www.isa.ru/index.php?lang=en) - 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 (http://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT).
La cryptanalyse (http://fr.wikipedia.org/wiki/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 (http://fr.wikipedia.org/wiki/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 (http://en.wikipedia.org/wiki/Quadratic_assignment_problem) (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.
Malheureusement il n'y a pas de librairie MAC OS pour DC-API (cette API (interface de programmation) est utilisée à la place de la version standard de BOINC). J'ai demandé aux développeurs de DC-API de faire une telle version, je l'attends pour le moment.
Dernière Info :
Le 04/06/2012
New version of application. New experiment
- Experiment aimed at solving A5/1 crytanalysis problems successfully ended May 5, 2012 (it took 6 months).
- New experiment has started. The goal is to find pairs of orthogonal latin squares of order 9 and 10
- Version 1.19 was released.
Nouvelle version de l'application. Nouvelle expérience.
- L'expérience visant à des problèmes de cryptanalyse avec A5/1 s'est terminée avec succès le 5 Mai 2012 (il aura fallu 6 mois).
- Une nouvelle expérience a commencée. Le but est de trouver des paires de carrés latins orthogonaux d'ordre 9 et 10
- La version 1.19 est maintenant disponible.
mise à jour par fzs600 le 22 avril 2020