SAT-MICRO: petit mais costaud !

Sylvain Conchon 1 Johannes Kanig 1 Stéphane Lescuyer 1
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Le problème SAT, qui consiste à déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en OCaml d'un SAT-solver, baptisé SAT-MICRO, intégrant ces optimisations ainsi qu'une mise en forme normale conjonctive paresseuse. Le fonctionnement de SAT-MICRO est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.
Type de document :
Communication dans un congrès
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.91-106, 2008
Liste complète des métadonnées

Littérature citée [3 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00202831
Contributeur : Sandrine Blazy <>
Soumis le : mardi 8 janvier 2008 - 11:52:44
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:51:33

Fichier

conchon.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00202831, version 1

Collections

Citation

Sylvain Conchon, Johannes Kanig, Stéphane Lescuyer. SAT-MICRO: petit mais costaud !. JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.91-106, 2008. 〈inria-00202831〉

Partager

Métriques

Consultations de la notice

439

Téléchargements de fichiers

289