Auteur Sujet: SAT@home  (Lu 14347 fois)

0 Membres et 1 Invité sur ce sujet

Aillas

  • Messages: 74
  • Boinc'eur Junior
  • **
  •   
SAT@home
« le: 10 octobre 2011 à 14:26 »


Infos Utiles :




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.

Citer
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

Citer
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.

Citer
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 04 Juin 2012 par cedricdd.
« Modifié: 03 février 2013 à 20:28 par LOCTET SetiOne »

ousermaatre

  • Gentil admin
  • Messages: 11504
  • Boinc'eur devant l'éternel
  • *******
  •   
Re : SAT@home
« Réponse #1 le: 10 octobre 2011 à 14:34 »
projet d'algorithmes ? section mathématiques ?

[AF>Libristes] Dudumomo

  • Messages: 5872
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #2 le: 10 octobre 2011 à 14:39 »
Projet issu de la meme academie des sciences que le projet Optima@home
http://www.isa.ru/

C'est dommage qu'ils divisent leurs ressources ainsi.
News & Tutorial on how to host your server: http://freedif.org

fzs600

  • Animateur fanatique
  • Messages: 5931
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #3 le: 10 octobre 2011 à 14:52 »
Aillas   :hello:

Merci pour l'info

« Modifié: 10 octobre 2011 à 22:52 par fzs600 »

Utilisateur GNU-LINUX. fzs600@hub.g3l.org

[AF>Libristes] nico8313

  • Messages: 7863
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #4 le: 10 octobre 2011 à 14:55 »
Poly n'a pas encore crée notre team !!! c'est un scandale !!!  :o :o

 :D

[AF>Libristes] nico8313

  • Messages: 7863
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #5 le: 10 octobre 2011 à 15:04 »

samuel debergh

  • Messages: 3574
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #6 le: 10 octobre 2011 à 16:10 »
inscrit j'ai des wu à mi parcours , je verrai bientot ce que ça donne en points.
« Modifié: 10 octobre 2011 à 17:57 par samuel debergh »

Jaehaerys Targaryen

  • CàA
  • Messages: 10388
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #7 le: 10 octobre 2011 à 19:40 »
Citer
PDSAT is a research project that uses Internet-connected computers to solve hard and practically important problems (discrete functions inversion problems, discrete optimization,   bioinformatics, etc) that can be effectively reduced to SAT. Currently in the project problems of inversion of some cryptographic functions used in keystream generators are being solved. All cryptographic algorithms under investigation are publicly available. Corresponding tasks are randomly generated and do not contain any confidential information. We also plan to publish obtained results. In the nearest future we are going to launch an experiment for solving Quadratic Assignment problem (hard optimization problem) within the project.

Projet sur la cryptographie ?

Poly n'a pas encore crée notre team !!! c'est un scandale !!!  :o :o

 :D
  :D :D
« Modifié: 10 octobre 2011 à 19:42 par Polynésia »


Twitter : devweborne // Chaine Youtube : https://www.youtube.com/channel/UCXcoCd-1UlHpYIYzNER0n1Q

ousermaatre

  • Gentil admin
  • Messages: 11504
  • Boinc'eur devant l'éternel
  • *******
  •   
Re : SAT@home
« Réponse #8 le: 10 octobre 2011 à 19:42 »
 :hello: Poly, j'ai mis un lien sur le SAT en premier post. 

Jaehaerys Targaryen

  • CàA
  • Messages: 10388
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #9 le: 10 octobre 2011 à 19:46 »
ouaip....  :??: :??: avec mes 2 neurones je comprends presque rien...


Twitter : devweborne // Chaine Youtube : https://www.youtube.com/channel/UCXcoCd-1UlHpYIYzNER0n1Q

[AF>Libristes>Jip]Augure

  • Méchant modo
  • Messages: 4701
  • Boinc'eur devant l'éternel
  • ******
  •   
Re : SAT@home
« Réponse #10 le: 10 octobre 2011 à 20:32 »
Projet issu de la meme academie des sciences que le projet Optima@home
http://www.isa.ru/

C'est dommage qu'ils divisent leurs ressources ainsi.

oui !

pour eux et pour nous (car si au final 500 projets existe => cool  :love: ! mais on sera jamais inscrit sur tous ! :/ ! )...
>>

[AF>Libristes] Dudumomo

  • Messages: 5872
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #11 le: 11 octobre 2011 à 01:52 »
Pour info, je leur ai envoye un mail pour leur demander pourquoi il ne faisait pas directement un projet tiroir vu qu'ils travaillent dans le meme departement.
 :coffeetime:
News & Tutorial on how to host your server: http://freedif.org

Infomat

  • Animateur fanatique
  • Messages: 5319
  • Boinc'eur devant l'éternel
  • *****
  •   
    • Site de Claude
Re : SAT@home
« Réponse #12 le: 11 octobre 2011 à 05:40 »
Inscris dessus et reçu des UT cpu alors que des gpu sont possibles... Mais j'en ai pas encore reçu  :??:


[6c/ 12t] Intel i7-980X @3.7  2xNVidia GTX 760  AMD 6970    Windows 7 Pro x64 ou Windows 10 Pro x64 ou Linux 
ELAF= Electrons Libres de l'AF http://forum.electronslibres.boinc-af.org/

fzs600

  • Animateur fanatique
  • Messages: 5931
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #13 le: 11 octobre 2011 à 07:23 »
Inscris dessus et reçu des UT cpu alors que des gpu sont possibles... Mais j'en ai pas encore reçu  :??:
Des UTs GPU ou ca   :??:
http://sat.isa.ru/pdsat/apps.php   :kookoo:


Deja 2 ut de faites
Citer
   10 Oct 2011 12:39:46 UTC    11 Oct 2011 1:40:01 UTC    Completed and validated    23,810.21    135.77    135.77
   10 Oct 2011 12:40:01 UTC    11 Oct 2011 1:35:57 UTC    Completed and validated    23,730.54    135.32    135.32


Utilisateur GNU-LINUX. fzs600@hub.g3l.org

samuel debergh

  • Messages: 3574
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #14 le: 11 octobre 2011 à 07:40 »

fzs600

  • Animateur fanatique
  • Messages: 5931
  • Boinc'eur devant l'éternel
  • *****
  •   

Utilisateur GNU-LINUX. fzs600@hub.g3l.org

samuel debergh

  • Messages: 3574
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #16 le: 11 octobre 2011 à 08:11 »
j'ai vu juste rapidement l'annonce^^

JeromeC

  • CàA
  • Messages: 23190
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #17 le: 11 octobre 2011 à 13:59 »
Citer
PDSAT is a research project that uses Internet-connected computers to solve hard and practically important problems (discrete functions inversion problems, discrete optimization,   bioinformatics, etc) that can be effectively reduced to SAT. Currently in the project problems of inversion of some cryptographic functions used in keystream generators are being solved. All cryptographic algorithms under investigation are publicly available. Corresponding tasks are randomly generated and do not contain any confidential information. We also plan to publish obtained results. In the nearest future we are going to launch an experiment for solving Quadratic Assignment problem (hard optimization problem) within the project.

PDSAT est un projet de recherche qui utilise des ordinateurs connectés à Internet pour résoudre des problèmes difficiles et "pratiquement important" (problèmes d'inversion de fonctions discrètes, optimisation discrète, la bioinformatique, etc) qui peuvent être effectivement réduits à des problèmes SAT. Actuellement des "problèmes" dans le projet de d'inversion de certaines fonctions cryptographiques utilisées dans les "générateurs de chiffrement" sont résolus. Tous les algorithmes de cryptographie à l'étude sont disponibles publiquement. Les tâches correspondantes sont générés aléatoirement et ne contiennent aucune information confidentielle. Nous prévoyons également de publier les résultats obtenus. Dans le proche avenir, nous allons lancer une expérimentation pour résoudre le problème d'affectation quadratique (problème d'optimisation difficile) au sein du projet.


Donc oui, encore de la cryptographie, mais pour décrypter, on dirait bien, non ?
Parce que c'était lui, parce que c'était moi.

RLDF

  • Messages: 4530
  • Boinc'eur devant l'éternel
  • *****
  •   
    • avatar ?
Re : SAT@home
« Réponse #18 le: 11 octobre 2011 à 14:47 »
PDSAT est un projet de recherche qui utilise des ordinateurs connectés à Internet pour résoudre des problèmes difficiles et "pratiquement important" (problèmes d'inversion de fonctions discrètes, optimisation discrète, la bioinformatique, etc) qui peuvent être effectivement réduits à des problèmes SAT. Actuellement des "problèmes" dans le projet de d'inversion de certaines fonctions cryptographiques utilisées dans les "générateurs de chiffrement" sont résolus. Tous les algorithmes de cryptographie à l'étude sont disponibles publiquement. Les tâches correspondantes sont générés aléatoirement et ne contiennent aucune information confidentielle. Nous prévoyons également de publier les résultats obtenus. Dans le proche avenir, nous allons lancer une expérimentation pour résoudre le problème d'affectation quadratique (problème d'optimisation difficile) au sein du projet.


Donc oui, encore de la cryptographie, mais pour décrypter, on dirait bien, non ?
oops, tu as bien fait de traduire, je pensais que c'était un bouquet de chaines TV par satellite pour la communauté gay  :lol:

ousermaatre

  • Gentil admin
  • Messages: 11504
  • Boinc'eur devant l'éternel
  • *******
  •   
Re : SAT@home
« Réponse #19 le: 11 octobre 2011 à 16:27 »
 :giligili:

mcroger

  • Méchant modo
  • Messages: 6071
  • Boinc'eur devant l'éternel
  • ******
  •   
Re : SAT@home
« Réponse #20 le: 11 octobre 2011 à 20:25 »
 :hap:

al@ON

  • Messages: 11703
  • Boinc'eur devant l'éternel
  • *****
  •   
    • MySpace al@ON
Re : SAT@home
« Réponse #21 le: 12 octobre 2011 à 00:03 »
 :lol:

[AF>Libristes] nico8313

  • Messages: 7863
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #22 le: 12 octobre 2011 à 00:08 »
 :ptdr: :ptdr: :ptdr: :ptdr: :ptdr:

Infomat

  • Animateur fanatique
  • Messages: 5319
  • Boinc'eur devant l'éternel
  • *****
  •   
    • Site de Claude
Re : SAT@home
« Réponse #23 le: 12 octobre 2011 à 03:29 »
Si ils demandent dans les options si on veut utiliser une CG, c'est qu'il devrait y avoir des UT pour elles, non ???


[6c/ 12t] Intel i7-980X @3.7  2xNVidia GTX 760  AMD 6970    Windows 7 Pro x64 ou Windows 10 Pro x64 ou Linux 
ELAF= Electrons Libres de l'AF http://forum.electronslibres.boinc-af.org/

cedricdd

  • Messages: 1389
  • Boinc'eur devant l'éternel
  • *****
  •   
Re : SAT@home
« Réponse #24 le: 12 octobre 2011 à 03:43 »
ou qu'ils ont configurés ça n'importe comment  :lol:
Kill all my demons, and my angels might die too.