DPLL SAT求解器

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.

csatsolver-badsi-chapon-ferlet
genclauses.py
benchall.sh
fsio.c
fsio.h
bench.sh
solver.c
mem.c
solver.h
matrice.txt
jnh1-sat.txt
mem.h
matrice.c
jnh301-sat.txt
csatsolver.c
jnh2-unsat.txt
convall.sh
gen3satset.py
jnh3-unsat.txt
jnh7-sat.txt
matrice.h
Makefile
clauses.txt
dimacsconv.py
README