Comme promis la maj du soir.

J'ai corrigé 2-3 trucs dans mes fonctions et je pense qu'elles ne contiennent (presque) plus de bugs. Pour tester : appeler dpll sur une formule, s'il renvoie true alors on trouve une affectation qui marche dans "paris", si false : insatisfiable

En fait, ça ne peut pas marcher pour l'instant puisqu'il y a d'abord la question suivante à résoudre :
au sujet des variables (leur nombre, où les stocker...) : après réflexion, je pense que ça simplifierait vraiment les choses de stocker leur nombre dans la formule et de ne pas utiliser le varset "vars" (et du coup, dans l'initializer, on initialise les occurences_pos/neg au cas où on ait des variables n'apparaissant dans aucune clause). Je me suis renseigné sur le format d'entrée DIMACS et il est bien précisé que pour n variables celles-ci doivent prendre leurs noms entre 1 et n. Je n'ai pas modifié l'objet formule pour l'instant, mais les fonctions find_single_polarite et next_pari présupposent actuellement que les variables sont entre 1 et n et que n est connu (càd un champ nb_vars dans formule + une fonction get_nb_vars)

Enfin, pour s'en souvenir, une liste de trucs à faire (bugs ou consignes pour le rendu) :
  - détection des tautologies / inclusions ???
  - pré-traitement de l'entrée : éliminer tautologies ?
  - corriger l'utilisation du parser/lexer dans le main pour que ça compile << déplacer la gestion des arguments passés en entrée dans un fichier à part ?
  - fonctions d'affichage en cours de route (imposé !)