资 源 简 介
Dans le cadre du projet de langage C, nous avons étudié le problème SAT et realisé un programme de résolution de celui-ci. À travers les questions qui nous étaient proposées, nous avons pu remettre en œuvre l"algorithme DPLL (Davis, Putnam, Logemann, Loveland) en employant une structure de données qui nous est propre. Une fois l"algorithme fonctionnel, nous nous sommes intéressés aux différentes optimisations possibles et en avons implémenté certaines. Pour nous assurer de l"efficacité de l"algorithme, nous avons réalisé différentes séries de tests.
