Representations de formules SAT pour la resolution sequentielle

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.