SAT-MICRO: petit mais costaud !

Sylvain Conchon 1 Johannes Kanig 1 Stéphane Lescuyer 1
1 PROVAL - Proof of Programs
CNRS : UMR, UP11 - Université Paris-Sud - Paris 11, INRIA Saclay - Ile de France
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.
Document type :
Conference papers
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.91-106, 2008


https://hal.inria.fr/inria-00202831
Contributor : Sandrine Blazy <>
Submitted on : Tuesday, January 8, 2008 - 11:52:44 AM
Last modification on : Wednesday, August 13, 2008 - 3:20:10 PM

File

conchon.pdf
fileSource_public_author

Identifiers

  • 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>

Export

Share

Metrics

Consultation de
la notice

158

Téléchargement du document

96