Please use this identifier to cite or link to this item: http://univ-bejaia.dz/dspace/123456789/9590
Title: Representations de formules SAT pour la resolution sequentielle
Authors: Boudjerida, Fatima
Habbas, Zineb; Promotrice
Keywords: SAT : Resolution sequentielle : CNF : OBDD : DNNF
Issue Date: 2007
Publisher: Université de Béjaia
Abstract: La simplicité du formalisme de la logique propositionnelle a considérablement contribué aux succès courants de la résolution des problèmes SAT. D'une part, la simplicité du formalisme facilite l’implémentation de solveurs efficaces par des structures de données simples. D'autre part, plusieurs problèmes NP-complet ont des encodages linéaires de petite taille comme la forme normale de négation décomposable (DNNF), qui est fortement approprié pour des objectifs pratiques. Dans ce présent travail, nous avons analysé les formalismes les plus connu dans le cadre de la résolution séquentielle. Dans ces formalismes, les solveurs a pour but de résoudre les différents types de problèmes théoriques et industriels réputés dans la communauté SAT dans un temps polynomial. Nous avons étudié les trois formalismes: CNF, OBDD et DNNF. La première est le plus ancien et le plus utilisé dans la littérature comme Rel-SAT, Grasp, SATO, Chaff, BerkMin, Siege, Minisat,….mais la dernière DNNF est plus efficace. Pour faire face à ce formalisme nous avons proposé une résolution basée sur un formalisme hybride (CNF et DNNF). Les résultats obtenus montrent l'efficacité de la solution proposée à compiler les instances des problèmes SAT, encodés en CNF, au d-DNNF et à calculer les solutions de ces instances.
Description: Option : Réseaux et Systèmes Distribués
URI: http://univ-bejaia.dz/dspace/123456789/9590
Appears in Collections:Mémoires de Magister

Files in This Item:
File Description SizeFormat 
Representations de formules SAT pour la resolution sequentielle.pdf2.17 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.