sign in
english version rss feed

inria-00202831, version 1

SAT-MICRO: petit mais costaud !

Sylvain Conchon 1, Johannes Kanig 1, Stéphane Lescuyer 1

JFLA (Journées Francophones des Langages Applicatifs) (2008) 91-106

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.

  • Domain : Computer Science/Programming Languages
 
  • inria-00202831, version 1
  • oai:hal.inria.fr:inria-00202831
  • From: 
  • Submitted on: Tuesday, 8 January 2008 11:52:44
  • Updated on: Wednesday, 13 August 2008 15:20:10
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...