SAT-MICRO: petit mais costaud !

Le probleme SAT, qui consiste a determiner si une formule booleenne est satisfaisable, est un des problemes NP-complets les plus celebres et aussi un des plus etudies. Bases initialement sur la procedure DPLL, les SAT-solvers modernes ont connu des progres spectaculaires ces dix dernieres annees dans leurs performances, essentiellement grâce a deux optimisations: le retour en arriere non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une etude formelle du fonctionnement de ces techniques ainsi qu'une realisation en OCaml d'un SAT-solver, baptise SAT-MICRO, integrant ces optimisations ainsi qu'une mise en forme normale conjonctive paresseuse. Le fonctionnement de SAT-MICRO est decrit par un ensemble de regles d'inference et la taille de son code, 70 lignes au total, permet d'envisager sa certification complete.