SAT@casa

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 16 de mayo de 2018; las comprobaciones requieren 5 ediciones .
SAT@Home
Plataforma BOINC
Tamaño de descarga de software 10 MB
Tamaño cargado de datos de trabajo 2 KB
Cantidad de datos de trabajo enviados 20 KB
Espacio en disco 10 MB
Cantidad de memoria utilizada 80 MB
interfaz gráfica de usuario No
Tiempo promedio de cálculo de tareas hasta 5 horas
plazo 10 días
Posibilidad de usar GPU No

SAT@home es un proyecto informático voluntario ruso en la plataforma BOINC , lanzado en septiembre de 2011 [1] . El objetivo científico del proyecto es resolver problemas discretos reduciéndolos al problema de satisfacibilidad de fórmulas booleanas (SAT, del inglés.  Satisfiability - factibility) en forma normal conjuntiva (CNF). La búsqueda de una solución al problema seleccionado se lleva a cabo utilizando uno de los conocidos solucionadores de SAT que implementa el algoritmo DPLL . El proyecto cuenta con el apoyo del Laboratorio de Análisis Discreto y Lógica Aplicada del Instituto de Dinámica de Sistemas y Teoría de Control de la Rama Siberiana de la Academia Rusa de Ciencias y el Centro de Computación Distribuida del Instituto de Problemas de Transmisión de Información . A partir del 19 de septiembre de 2014, participaron en el proyecto 18394 ordenadores de 7239 usuarios de 124 países, proporcionando un rendimiento de alrededor de 3,1 teraflops [ 2] . Cualquiera que tenga una computadora con acceso a Internet puede participar en el proyecto instalando en ella el programa BOINC .

Historia del proyecto

Los cálculos en el marco del proyecto comenzaron [3] en septiembre de 2011 con la solución del problema de criptoanálisis del generador A5/1 utilizado en las comunicaciones GSM . Según el fragmento conocido del flujo de claves, se requería determinar la secuencia de inicialización, es decir, el llenado inicial de los registros del generador . El propósito de los cálculos fue probar la aplicabilidad del enfoque SAT para resolver este problema en aquellos casos en los que es imposible encontrar una solución por otros métodos (por ejemplo, utilizando tablas de arcoíris ). Como resultado de los cálculos, en mayo de 2012 se resolvieron 10 problemas de prueba de criptoanálisis A5/1 [4] .

En junio de 2012 se lanzó un nuevo experimento cuyo objetivo fue la búsqueda de pares ortogonales de cuadrados latinos diagonales de orden 9. Para agosto de 2012 se habían encontrado 134 pares, lo que demostró la aplicabilidad de este enfoque al problema. A raíz de esto, se lanzó un experimento para buscar pares ortogonales de cuadrados latinos diagonales de orden 10. Como resultado de los cálculos, hasta el momento se han encontrado 13 pares de cuadrados latinos [4] , que no coinciden con los pares conocidos dados en el artículo [5] .

Logros científicos

año 2012 Año 2013

Al parecer, el proyecto dejó de existir en 2016.

Notas

  1. ↑ SAT@Home . Fecha de acceso: 26 de diciembre de 2012. Archivado desde el original el 21 de diciembre de 2012.
  2. ↑ Estadísticas detalladas de SAT@home . Consultado el 5 de septiembre de 2013. Archivado desde el original el 11 de agosto de 2013.
  3. ↑ Archivo de noticias de SAT@home (enlace descendente) . Fecha de acceso: 26 de diciembre de 2012. Archivado desde el original el 4 de enero de 2013. 
  4. ↑ 1 2 3 4 Soluciones SAT@home encontradas (enlace no disponible) . Fecha de acceso: 26 de diciembre de 2012. Archivado desde el original el 21 de diciembre de 2012. 
  5. ↑ Brown et al. Completamiento del Espectro de Cuadrados Latinos Diagonales Ortogonales. Apuntes de clase de matemáticas puras y aplicadas. 1992 vol. 139. Págs. 43–49.

Enlaces