SAT-MICRO: petit mais costaud ! - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2008

SAT-MICRO: petit mais costaud !

Abstract

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.
Fichier principal
Vignette du fichier
conchon.pdf (389.62 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00202831 , version 1 (08-01-2008)

Identifiers

  • HAL Id : inria-00202831 , version 1

Cite

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

Share

Gmail Facebook X LinkedIn More