-
-
-
-
-
-
-
HomeSite map
SoC/Offres d'emplois/Stages/2009-2010/ALSOC 11 Print page

Parallélisation de la résolution de problèmes SAT

 

 

Introduction 

Les circuits intégrés deviennent de plus en plus complexes et réduits. Si des moyens et des outils puissants sont mis à la disposition des développeurs, l’usage d’outils de test automatique et de vérification reste marginal alors que les domaines d’application sont de plus en plus critiques (aérospatiale, télécom, nucléaire,…). 

Récemment des progrès significatifs ont été réalisés dans le domaine de la vérification de circuits en employant en particulier des techniques basées sur des « SAT Solvers » combinées avec l’approche dite « Bounded Model Checking ». 

Un problème SAT est le problème de déterminer si les variables d’une formule booléenne peuvent être assignées, de façon à évaluer la formule à vraie. Ce problème trouve son importance dans plusieurs domaines d’applications (model-checking, planification, intelligence artificielle….). Cependant il est connu pour être un problème NP–complet (en général) !  

Ainsi, le but principal du stage est d’étudier la possibilité de parallélisation d’algorithmes de résolution de problèmes SAT (en particulier le problème de comptage du nombre de solutions d’un problème SAT), comme heuristique permettant l’accélération de la résolution. Ensuite, il sera question d’intégrer le résultat de cette étude dans le logiciel VIS (un outil qui intègre la vérification, la simulation et la synthèse des systèmes matériels).  

Contexte 

Le stage se déroulera au LIP6, dans l’équipe ALSOC, du département SoC. Il s’intègre dans le cadre du projet FME3 (Enhancing the Evaluation of Error consequences using Formal Methods), dont l’objectif principal est l’évaluation de la robustesse des circuits intégrés. 

Le stage sera encadré par Souheib Baarir, maitre de conférences à l’université de Paris Ouest Nanterre la Défense, rattaché au LIP6 (équipe MoVe). 

Travail à réaliser 

  • Etat de l’art des techniques et outils existants.
  • Construction d’une série de programme de Référence.
  • Réalisation d’un prototype.

 

Pré-requis  

  • Connaissance de C, C++.
  • Des connaissances en (Bounded) Model Cheking seront très appréciées.

  

Références 

  1. V. Dahllof, P. Jonsson, M. Wahlstrom. Counting satisfying assignments in 2-SAT and 3-SAT.
  2. H. Jin, F. Somenzi. Prime clauses for fast enumeration of satisfying assignments to boolean circuits
  3. J. Roberto, Jr. Bayardo, J. D. Pehoushek. Counting Models Using Connected Components.
  4. Marc Thurley. SharpSAT - Counting Models with Advanced Component Caching and Implicit BCP.
  5. A. Biere, A. Cimatti, E. Clarke and Y. Zhu. Symbolic Model Checking without BDDs
  6. R. K. Brayton et all. VIS : A System for Verification and Synthesis.

LIP6 LIP6-SoC LIP6 CNRS UPMC