Contribution à l'implémentation d'un algorithme de résolution d'équations booléennes

Équipe

Calcul Formel

Responsables

Objectifs du stage

  • Participer à une implémentation ultra-efficace d'un algorithme nouveau
  • Inclure le code dans des librairies open-source

Mots-clefs

calcul scientifique haute performance, parallélisation, équations booléennes, générateur de code, assembleur x86, instructions multimédia.

Contexte Scientifique

Ce projet tourne autours d'un algorithme nouveau [1] pour résoudre des systèmes d'équations booléennes. Dans SAT, le plus connu des problèmes NP-complets, on trouve des équations avec des ET, des OU, des NON et des variables. Le type d'équations auxquelles on s'intéresse ici contient des variables, des constantes, des ET et des XOR. On peut voir ces équations commes des polynômes en plusieurs variables, mais dont les variables valent soit zéro soit un. Le problème associé est lui aussi NP-complet. La résolution de ce type d'équation est plus difficile que SAT, car la méthode de "backtracking" efficace utilisée pour SAT ne peut pas s'appliquer.

En dehors de cas particuliers, la méthode la plus efficace pour résoudre ce genre de systèmes d'équations est la recherche exhaustive. Elle est facile à paralléliser, et son temps d'éxecution est très prévisible, puisqu'il est de l'ordre de 2^n opérations s'il y a n variables. L'algorithme donné dans [1] est une reformulation intelligente de la recherche exhaustive qui économise des calculs, et est particulièrement efficace, puisqu'il est possible de traiter presque 3 solutions possibles par cycle CPU sur du matériel récent. Ce code est le plus rapide du monde, de très, très, très loin, pour résoudre ce type d'équations. L'algorithme lui-même n'est pas particulièrement compliqué (il s'agit principalement de faire des XOR...). Cependant, pour obtenir ce niveau de performance, une implémentation extrêmement efficace est nécessaire.

L'algorithme de [1] a été implémenté une première fois par ses auteurs sur CPU et sur GPU, et a démontré ses performances. Cette première implémentation, efficace, était cependant de qualité "recherche", et pas de qualité "production". Il n'était pas possible de la distribuer, et quasiment personne d'autre que ses auteurs ne pouvaient s'en servir.

Un premier effort a été accompli l'été 2012 pour repartir de zéro, et recommencer à écrire le code sur des bases saines. Cela a soulevé de nombreux problèmes, tant théoriques que pratiques. Une nouvelle implémentation, plus claire, plus simple, existe, mais elle n'atteint pas encore le niveau de performances de l'ancienne. Cependant, elle est suffisament "propre" et bien pensée pour pouvoir être inclue dans un logiciel de calcul open-source, SAGE. D'ores-et-déjà, il est possible d'utiliser la nouvelle implémentation dans SAGE pour faire des calculs (http://trac.sagemath.org/sage_trac/ticket/13162). Cependant, toutes les fonctionnnalités ne sont pas disponible. Par exemple, alors que la parallélisation serait facile, le nouveau code n'est pas encore multi-thread.

Une des particuliarité de ce code est que la boucle principale est très courte, mais qu'elle doit être très rapide. Pour cela, elle est écrite directement en assembleur. De nombreuses "ruses" sont utilisées pour utiliser le CPU au maximum de ses capacités. Ce code assembleur est lui-même généré automatiquement lors de la compilation de la librairie. Faire fonctionner tout ça est donc non-trivial. Il y a aussi une version "purement en C" de la librairie, ce qui lui permet de fonctionner sur d'autres CPU que des x86. Le code actuel en assembleur est écrit pour les CPUs 64-bits uniquement.

Description du travail à effectuer

L'objectif principal du stage consiste à faire avancer l'implémentation actuelle. Cela peut être accompli de bien des manières : améliorer l'interface avec SAGE, paralléliser le code, l'améliorer (nous avons en tête un moyen de le rendre 50% plus rapide), écrire une petite documentation, une petite démonstration pour les utilisateurs de SAGE, écrire une version pour d'autres CPUs (ARM par exemple, SPARC, x86 32 bits, etc.). Si le travail pratique avance bien, on pourra envisager la rédaction d'un article scientifique sur le sujet.

Les problèmes à résoudre, de diverses natures, et surtout imprévus, ne manqueront pas.

Remarques

Ce stage est plutôt destiné à des étudiants qui sont à l’aise avec la programmation en général, mais en C en particulier. Des rudiments sur l’architecture des ordinateurs et des CPUs seraient souhaitable. Une expérience de programmation en assembleur serait un plus.

Références

[1] Charles Bouillaguet, Hsieh-Chung Chen, Chen-Mou Cheng, Tung Chou, Ruben Niede- rhagen, Adi Shamir, and Bo-Yin Yang. Fast exhaustive search for polynomial systems in GF(2). In Stefan Mangard and François-Xavier Standaert, editors, CHES, volume 6225 of Lecture Notes in Computer Science, pages 203–218. Springer, 2010.